From 86d9e3af022e82683d5f2c87c5d48aab1998deda Mon Sep 17 00:00:00 2001 From: glacode Date: Sat, 21 Dec 2024 10:29:17 +0100 Subject: [PATCH] Add new pre-image theorems (#4487) * 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. --- set.mm | 115 ++++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 86 insertions(+), 29 deletions(-) diff --git a/set.mm b/set.mm index aab2382ed3..4577dcbf8b 100644 --- a/set.mm +++ b/set.mm @@ -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 $. $} ${ @@ -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 $. $} ${ @@ -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 $. @@ -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 $. $} ${ @@ -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 $. @@ -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 $. $} ${