Skip to content

Commit

Permalink
Add new pre-image theorems (metamath#4487)
Browse files Browse the repository at this point in the history 
* Remove unnecessary $d condition from theorems on sigma-measurable functions

* Add new pre-image theorems

- Reduced  constraints by replacing them with 'effectively not free' hypotheses.
- Improves theorem usability and simplifies certain dependencies.
  • Loading branch information
@glacode
glacode authored Dec 21, 2024
1 parent 2cbfae9 commit 86d9e3a
Showing 1 changed file with 86 additions and 29 deletions.
115 changes: 86 additions & 29 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -750157,18 +750157,30 @@ its dimensional volume (the product of its length in each dimension,
UNUTBCUOUPTUQ $.
$}

${
pimltpnff.1 $e |- F/ x ph $.
pimltpnff.2 $e |- F/_ x A $.
pimltpnff.3 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
$( Given a real-valued function, the preimage of an open interval,
unbounded below, with upper bound ` +oo ` , is the whole domain.
(Contributed by Glauco Siliprandi, 20-Dec-2024.) $)
pimltpnff $p |- ( ph -> { x e. A | B < +oo } = A ) $=
( cpnf clt wbr crab wss ssrab2f a1i cv wcel wral wa simpr sylibr cr ltpnf
syl jca rabid ex ralrimi nfrab1 dfss3f eqssd ) ADHIJZBCKZCULCLAUKBCFMNABO
ZULPZBCQCULLAUNBCEAUMCPZUNAUORZUOUKRUNUPUOUKAUOSUPDUAPUKGDUBUCUDUKBCUETUF
UGBCULFUKBCUHUITUJ $.
$}

${
$d A x $.
pimltpnf.1 $e |- F/ x ph $.
pimltpnf.2 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
$( Given a real-valued function, the preimage of an open interval,
unbounded below, with upper bound ` +oo ` , is the whole domain.
(Contributed by Glauco Siliprandi, 26-Jun-2021.) $)
(Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco
Siliprandi, 20-Dec-2024.) $)
pimltpnf $p |- ( ph -> { x e. A | B < +oo } = A ) $=
( cpnf clt wbr crab wss ssrab2 a1i cv wcel wral wa simpr cr sylibr syl ex
ltpnf jca rabid ralrimi nfcv nfrab1 dfss3f eqssd ) ADGHIZBCJZCULCKAUKBCLM
ABNZULOZBCPCULKAUNBCEAUMCOZUNAUOQZUOUKQUNUPUOUKAUORUPDSOUKFDUCUAUDUKBCUET
UBUFBCULBCUGUKBCUHUITUJ $.
( nfcv pimltpnff ) ABCDEBCGFH $.
$}

${
Expand Down Expand Up @@ -750581,17 +750593,30 @@ its dimensional volume (the product of its length in each dimension,
CFLWJWNXJXPYCHUNAXQXIYCIPWKWLTTVNYCWRBCWOSWPWQ $.
$}

${
pimgtmnff.1 $e |- F/ x ph $.
pimgtmnff.2 $e |- F/_ x A $.
pimgtmnff.3 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
$( Given a real-valued function, the preimage of an open interval,
unbounded above, with lower bound ` -oo ` , is the whole domain.
(Contributed by Glauco Siliprandi, 20-Dec-2024.) $)
pimgtmnff $p |- ( ph -> { x e. A | -oo < B } = A ) $=
( cmnf clt wbr crab wss ssrab2f a1i cv wcel wral wa simpr sylibr cr mnflt
syl jca rabid ex ralrimi nfrab1 dfss3f eqssd ) AHDIJZBCKZCULCLAUKBCFMNABO
ZULPZBCQCULLAUNBCEAUMCPZUNAUORZUOUKRUNUPUOUKAUOSUPDUAPUKGDUBUCUDUKBCUETUF
UGBCULFUKBCUHUITUJ $.
$}

${
$d A x $.
pimgtmnf.1 $e |- F/ x ph $.
pimgtmnf.2 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
$( Given a real-valued function, the preimage of an open interval,
unbounded above, with lower bound ` -oo ` , is the whole domain.
(Contributed by Glauco Siliprandi, 26-Jun-2021.) $)
(Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco
Siliprandi, 20-Dec-2024.) $)
pimgtmnf $p |- ( ph -> { x e. A | -oo < B } = A ) $=
( cmnf clt wbr crab cv cmpt cfv wcel wa cr eqidd fvmpt2d eqcomd breq2d
rabbida nfmpt1 eqid fmptdf pimgtmnf2 eqtrd ) AGDHIZBCJGBKZBCDLZMZHIZBCJCA
UGUKBCEAUHCNOZDUJGHULUJDABCDUIPAUIQFRSTUAABCUIBCDUBABCDPUIEFUIUCUDUEUF $.
( nfcv pimgtmnff ) ABCDEBCGFH $.
$}

${
Expand Down Expand Up @@ -751349,6 +751374,29 @@ its dimensional volume (the product of its length in each dimension,
VNAVIVOVJVPAVHBVCCVMUNAVCCDRVMUOUPVATUQURUSABVCDEFHVCUTVBT $.
$}

${
$d A y $. $d B y $. $d R x y $.
smfpimltxrmptf.x $e |- F/ x ph $.
smfpimltxrmptf.1 $e |- F/_ x A $.
smfpimltxrmptf.s $e |- ( ph -> S e. SAlg ) $.
smfpimltxrmptf.b $e |- ( ( ph /\ x e. A ) -> B e. V ) $.
smfpimltxrmptf.f $e |- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) $.
smfpimltxrmptf.r $e |- ( ph -> R e. RR* ) $.
$( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
an open interval unbounded below is in the subspace sigma-algebra
induced by its domain. (Contributed by Glauco Siliprandi,
20-Dec-2024.) $)
smfpimltxrmptf $p |- ( ph -> { x e. A | B < R } e. ( S |`t A ) ) $=
( vy clt wbr crab wcel wceq nfcv crest co cv cmpt cfv cdm nfmpt1 nfdm nfv
nffv nfbr fveq2 breq1d cbvrabw a1i smfpimltxr eqeltrd dmmptdf2 rabeqf syl
eqid wa simpr fvmpt2f syl2anc rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d
mpbird ) ADEOPZBCQZFCUAUBZRBUCZBCDUDZUEZEOPZBVQUFZQZFVTUAUBZRAWANUCZVQUEZ
EOPZNVTQZWBWAWFSAVSWEBNVTBVQBCDUGZUHZNVTTVSNUIBWDEOBWCVQWGBWCTUJBOTBETUKV
PWCSVRWDEOVPWCVQULUMUNUOANEVTFVQNVQTJLVTVAMUPUQAVNWAVOWBAWAVSBCQZVNVNAVTC
SWAWISABVQCDGHIVQVAKURZVSBVTCWHIUSUTAVSVMBCHAVPCRZVBZVRDEOWLWKDGRVRDSAWKV
CKBCDGIVDVEUMVFAVNVGVHACVTFUAAVTCWJVIVJVKVL $.
$}

${
$d A x y $. $d B y $. $d R x y $.
smfpimltxrmpt.x $e |- F/ x ph $.
Expand All @@ -751358,17 +751406,10 @@ its dimensional volume (the product of its length in each dimension,
smfpimltxrmpt.r $e |- ( ph -> R e. RR* ) $.
$( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
an open interval unbounded below is in the subspace sigma-algebra
induced by its domain. (Contributed by Glauco Siliprandi,
26-Jun-2021.) $)
induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
(Revised by Glauco Siliprandi, 20-Dec-2024.) $)
smfpimltxrmpt $p |- ( ph -> { x e. A | B < R } e. ( S |`t A ) ) $=
( vy clt wbr crab crest wcel wceq nfcv co cv cmpt cfv cdm nfmpt1 nfdm nfv
nffv nfbr fveq2 breq1d cbvrabw a1i eqid smfpimltxr eqeltrd dmmptdf rabeqf
syl wa fvmpt2d rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d mpbird ) ADENO
ZBCPZFCQUAZRBUBZBCDUCZUDZENOZBVNUEZPZFVQQUAZRAVRMUBZVNUDZENOZMVQPZVSVRWCS
AVPWBBMVQBVNBCDUFZUGZMVQTVPMUHBWAENBVTVNWDBVTTUIBNTBETUJVMVTSVOWAENVMVTVN
UKULUMUNAMEVQFVNMVNTIKVQUOLUPUQAVKVRVLVSAVRVPBCPZVKVKAVQCSVRWFSABVNCDGHVN
UOZJURZVPBVQCWEBCTUSUTAVPVJBCHAVMCRVAVODENABCDVNGVNVNSAWGUNJVBULVCAVKVDVE
ACVQFQAVQCWHVFVGVHVI $.
( nfcv smfpimltxrmptf ) ABCDEFGHBCMIJKLN $.
$}

${
Expand Down Expand Up @@ -752255,6 +752296,29 @@ convergence can be decidedly irregular (Remark 121G of [Fremlin1]
EEUOUAUBBUCTULDLMUKDLUNABUDCUKDUQTULDUKUEUFUGUKULUHUI $.
$}

${
$d A y $. $d B y $. $d L x y $.
smfpimgtxrmptf.x $e |- F/ x ph $.
smfpimgtxrmptf.1 $e |- F/_ x A $.
smfpimgtxrmptf.s $e |- ( ph -> S e. SAlg ) $.
smfpimgtxrmptf.b $e |- ( ( ph /\ x e. A ) -> B e. V ) $.
smfpimgtxrmptf.f $e |- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) $.
smfpimgtxrmptf.l $e |- ( ph -> L e. RR* ) $.
$( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
an open interval unbounded above is in the subspace sigma-algebra
induced by its domain. (Contributed by Glauco Siliprandi,
20-Dec-2024.) $)
smfpimgtxrmptf $p |- ( ph -> { x e. A | L < B } e. ( S |`t A ) ) $=
( vy clt wbr crab wcel wceq nfcv crest co cv cmpt cfv cdm nfmpt1 nfdm nfv
nffv nfbr fveq2 breq2d cbvrabw a1i smfpimgtxr eqeltrd dmmptdf2 rabeqf syl
eqid wa simpr fvmpt2f syl2anc rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d
mpbird ) AFDOPZBCQZECUAUBZRFBUCZBCDUDZUEZOPZBVQUFZQZEVTUAUBZRAWAFNUCZVQUE
ZOPZNVTQZWBWAWFSAVSWEBNVTBVQBCDUGZUHZNVTTVSNUIBFWDOBFTBOTBWCVQWGBWCTUJUKV
PWCSVRWDFOVPWCVQULUMUNUOANFVTEVQNVQTJLVTVAMUPUQAVNWAVOWBAWAVSBCQZVNVNAVTC
SWAWISABVQCDGHIVQVAKURZVSBVTCWHIUSUTAVSVMBCHAVPCRZVBZVRDFOWLWKDGRVRDSAWKV
CKBCDGIVDVEUMVFAVNVGVHACVTEUAAVTCWJVIVJVKVL $.
$}

${
$d A x y $. $d B y $. $d L x y $.
smfpimgtxrmpt.x $e |- F/ x ph $.
Expand All @@ -752264,17 +752328,10 @@ convergence can be decidedly irregular (Remark 121G of [Fremlin1]
smfpimgtxrmpt.l $e |- ( ph -> L e. RR* ) $.
$( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
an open interval unbounded above is in the subspace sigma-algebra
induced by its domain. (Contributed by Glauco Siliprandi,
26-Jun-2021.) $)
induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
(Revised by Glauco Siliprandi, 20-Dec-2024.) $)
smfpimgtxrmpt $p |- ( ph -> { x e. A | L < B } e. ( S |`t A ) ) $=
( vy clt wbr crab crest wcel wceq nfcv co cv cmpt cfv cdm nfmpt1 nfdm nfv
nffv nfbr fveq2 breq2d cbvrabw a1i eqid smfpimgtxr eqeltrd dmmptdf rabeqf
syl wa fvmpt2d rabbida eqidd 3eqtrrd eqcomd oveq2d eleq12d mpbird ) AFDNO
ZBCPZECQUAZRFBUBZBCDUCZUDZNOZBVNUEZPZEVQQUAZRAVRFMUBZVNUDZNOZMVQPZVSVRWCS
AVPWBBMVQBVNBCDUFZUGZMVQTVPMUHBFWANBFTBNTBVTVNWDBVTTUIUJVMVTSVOWAFNVMVTVN
UKULUMUNAMFVQEVNMVNTIKVQUOLUPUQAVKVRVLVSAVRVPBCPZVKVKAVQCSVRWFSABVNCDGHVN
UOZJURZVPBVQCWEBCTUSUTAVPVJBCHAVMCRVAVODFNABCDVNGVNVNSAWGUNJVBULVCAVKVDVE
ACVQEQAVQCWHVFVGVHVI $.
( nfcv smfpimgtxrmptf ) ABCDEFGHBCMIJKLN $.
$}

${
Expand Down

0 comments on commit 86d9e3a

Please sign in to comment.