![]() |
Metamath
Proof Explorer Theorem List (p. 456 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smfpimgtxrmpt 45501* | 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.) (Revised by Glauco Siliprandi, 20-Dec-2024.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΏ β β*) β β’ (π β {π₯ β π΄ β£ πΏ < π΅} β (π βΎt π΄)) | ||
Theorem | smfpimioompt 45502* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΏ β β*) & β’ (π β π β β*) β β’ (π β {π₯ β π΄ β£ π΅ β (πΏ(,)π )} β (π βΎt π΄)) | ||
Theorem | smfpimioo 45503 | Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (π΄(,)π΅)) β (π βΎt π·)) | ||
Theorem | smfresal 45504* | Given a sigma-measurable function, the subsets of β whose preimage is in the sigma-algebra induced by the function's domain, form a sigma-algebra. First part of the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ π = {π β π« β β£ (β‘πΉ β π) β (π βΎt π·)} β β’ (π β π β SAlg) | ||
Theorem | smfrec 45505* | The reciprocal of a sigma-measurable functions is sigma-measurable. First part of Proposition 121E (e) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ πΆ = {π₯ β π΄ β£ π΅ β 0} β β’ (π β (π₯ β πΆ β¦ (1 / π΅)) β (SMblFnβπ)) | ||
Theorem | smfres 45506 | The restriction of sigma-measurable function is sigma-measurable. Proposition 121E (h) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ (π β π΄ β π) β β’ (π β (πΉ βΎ π΄) β (SMblFnβπ)) | ||
Theorem | smfmullem1 45507 | The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π Β· π) < π΄) & β’ π = ((π΄ β (π Β· π)) / (1 + ((absβπ) + (absβπ)))) & β’ π = if(1 β€ π, 1, π) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ (π β π» β (π(,)π )) & β’ (π β πΌ β (π(,)π)) β β’ (π β (π» Β· πΌ) < π΄) | ||
Theorem | smfmullem2 45508* | The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ πΎ = {π β (β βm (0...3)) β£ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π΄} & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π Β· π) < π΄) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ (π β π β ((π β π)(,)π)) & β’ (π β π β (π(,)(π + π))) & β’ π = ((π΄ β (π Β· π)) / (1 + ((absβπ) + (absβπ)))) & β’ π = if(1 β€ π, 1, π) β β’ (π β βπ β πΎ (π β ((πβ0)(,)(πβ1)) β§ π β ((πβ2)(,)(πβ3)))) | ||
Theorem | smfmullem3 45509* | The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β β) & β’ πΎ = {π β (β βm (0...3)) β£ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π } & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π Β· π) < π ) & β’ π = ((π β (π Β· π)) / (1 + ((absβπ) + (absβπ)))) & β’ π = if(1 β€ π, 1, π) β β’ (π β βπ β πΎ (π β ((πβ0)(,)(πβ1)) β§ π β ((πβ2)(,)(πβ3)))) | ||
Theorem | smfmullem4 45510* | The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) & β’ (π β π β β) & β’ πΎ = {π β (β βm (0...3)) β£ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π } & β’ πΈ = (π β πΎ β¦ {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) β β’ (π β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π } β (π βΎt (π΄ β© πΆ))) | ||
Theorem | smfmul 45511* | The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) β β’ (π β (π₯ β (π΄ β© πΆ) β¦ (π΅ Β· π·)) β (SMblFnβπ)) | ||
Theorem | smfmulc1 45512* | A sigma-measurable function multiplied by a constant is sigma-measurable. Proposition 121E (c) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β (SMblFnβπ)) | ||
Theorem | smfdiv 45513* | The fraction of two sigma-measurable functions is measurable. Proposition 121E (e) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β π) & β’ ((π β§ π₯ β πΆ) β π· β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) & β’ πΈ = {π₯ β πΆ β£ π· β 0} β β’ (π β (π₯ β (π΄ β© πΈ) β¦ (π΅ / π·)) β (SMblFnβπ)) | ||
Theorem | smfpimbor1lem1 45514* | Every open set belongs to π. This is the second step in the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ π½ = (topGenβran (,)) & β’ (π β πΊ β π½) & β’ π = {π β π« β β£ (β‘πΉ β π) β (π βΎt π·)} β β’ (π β πΊ β π) | ||
Theorem | smfpimbor1lem2 45515* | Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β πΈ β π΅) & β’ π = (β‘πΉ β πΈ) & β’ π = {π β π« β β£ (β‘πΉ β π) β (π βΎt π·)} β β’ (π β π β (π βΎt π·)) | ||
Theorem | smfpimbor1 45516 | Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β πΈ β π΅) & β’ π = (β‘πΉ β πΈ) β β’ (π β π β (π βΎt π·)) | ||
Theorem | smf2id 45517* | Twice the identity function is Borel sigma-measurable (just an example, to test previous general theorems). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π΄ β β) β β’ (π β (π₯ β π΄ β¦ (2 Β· π₯)) β (SMblFnβπ΅)) | ||
Theorem | smfco 45518 | The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π» β (SMblFnβπ΅)) β β’ (π β (π» β πΉ) β (SMblFnβπ)) | ||
Theorem | smfneg 45519* | The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) β β’ (π β (π₯ β π΄ β¦ -π΅) β (SMblFnβπ)) | ||
Theorem | smffmptf 45520 | A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) β β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) | ||
Theorem | smffmpt 45521* | A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) β β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) | ||
Theorem | smflim2 45522* | The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). TODO: this has fewer distinct variable conditions than smflim 45493 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfpimcclem 45523* | Lemma for smfpimcc 45524 given the choice function πΆ. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ π β π & β’ (π β π β π) & β’ ((π β§ π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β (πΆβπ¦) β π¦) & β’ π» = (π β π β¦ (πΆβ{π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) | ||
Theorem | smfpimcc 45524* | Given a countable set of sigma-measurable functions, and a Borel set π΄ there exists a choice function β that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of π΄. This is a generalization of the observation at the beginning of the proof of Proposition 121F of [Fremlin1] p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) & β’ (π β π΄ β π΅) β β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) | ||
Theorem | issmfle2d 45525* | A sufficient condition for "πΉ being a measurable function w.r.t. to the sigma-algebra π". (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β SAlg) & β’ (π β π· β βͺ π) & β’ (π β πΉ:π·βΆβ) & β’ ((π β§ π β β) β (β‘πΉ β (-β(,]π)) β (π βΎt π·)) β β’ (π β πΉ β (SMblFnβπ)) | ||
Theorem | smflimmpt 45526* | The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). π΄ can contain π as a free variable, in other words it can be thought as an indexed collection π΄(π). π΅ can be thought as a collection with two indices π΅(π, π₯). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΄ β π) & β’ ((π β§ π β π β§ π₯ β π΄) β π΅ β π) & β’ (π β π β SAlg) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)π΄ β£ (π β π β¦ π΅) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ π΅))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfsuplem1 45527* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) & β’ (π β π΄ β β) & β’ (π β π»:πβΆπ) & β’ ((π β§ π β π) β (β‘(πΉβπ) β (-β(,]π΄)) = ((π»βπ) β© dom (πΉβπ))) β β’ (π β (β‘πΊ β (-β(,]π΄)) β (π βΎt π·)) | ||
Theorem | smfsuplem2 45528* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) & β’ (π β π΄ β β) β β’ (π β (β‘πΊ β (-β(,]π΄)) β (π βΎt π·)) | ||
Theorem | smfsuplem3 45529* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfsup 45530* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfsupmpt 45531* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²π₯π & β’ β²π¦π & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ ((π β§ π β π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ π· = {π₯ β β© π β π π΄ β£ βπ¦ β β βπ β π π΅ β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ π΅), β, < )) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfsupxr 45532* | The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < ) β β} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β*, < )) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfinflem 45533* | The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} & β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfinf 45534* | The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} & β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfinfmpt 45535* | The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²π₯π & β’ β²π¦π & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ ((π β§ π β π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ π· = {π₯ β β© π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅} & β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ π΅), β, < )) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smflimsuplem1 45536* | If π» converges, the lim sup of πΉ is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β πΎ β π) β β’ (π β dom (π»βπΎ) β dom (πΉβπΎ)) | ||
Theorem | smflimsuplem2 45537* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β π β π) & β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ))) β β) & β’ (π β π β β© π β (β€β₯βπ)dom (πΉβπ)) β β’ (π β π β dom (π»βπ)) | ||
Theorem | smflimsuplem3 45538* | The limit of the (π»βπ) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) β β’ (π β (π₯ β {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (π»βπ) β£ (π β π β¦ ((π»βπ)βπ₯)) β dom β } β¦ ( β β(π β π β¦ ((π»βπ)βπ₯)))) β (SMblFnβπ)) | ||
Theorem | smflimsuplem4 45539* | If π» converges, the lim sup of πΉ is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β π β π) & β’ (π β π₯ β β© π β (β€β₯βπ)dom (π»βπ)) & β’ (π β (π β π β¦ ((π»βπ)βπ₯)) β dom β ) β β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ₯))) β β) | ||
Theorem | smflimsuplem5 45540* | π» converges to the superior limit of πΉ. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ))) β β) & β’ (π β π β π) & β’ (π β π β β© π β (β€β₯βπ)dom (πΉβπ)) β β’ (π β (π β (β€β₯βπ) β¦ ((π»βπ)βπ)) β (lim supβ(π β (β€β₯βπ) β¦ ((πΉβπ)βπ)))) | ||
Theorem | smflimsuplem6 45541* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β (lim supβ(π β π β¦ ((πΉβπ)βπ))) β β) & β’ (π β π β π) & β’ (π β π β β© π β (β€β₯βπ)dom (πΉβπ)) β β’ (π β (π β π β¦ ((π»βπ)βπ)) β dom β ) | ||
Theorem | smflimsuplem7 45542* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ ((πΉβπ)βπ₯))) β β} & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) β β’ (π β π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (π»βπ) β£ (π β π β¦ ((π»βπ)βπ₯)) β dom β }) | ||
Theorem | smflimsuplem8 45543* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ ((πΉβπ)βπ₯))) β β} & β’ πΊ = (π₯ β π· β¦ (lim supβ(π β π β¦ ((πΉβπ)βπ₯)))) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smflimsup 45544* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (lim supβ(π β π β¦ ((πΉβπ)βπ₯))) β β} & β’ πΊ = (π₯ β π· β¦ (lim supβ(π β π β¦ ((πΉβπ)βπ₯)))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smflimsupmpt 45545* | The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . π΄ can contain π as a free variable, in other words it can be thought of as an indexed collection π΄(π). π΅ can be thought of as a collection with two indices π΅(π, π₯). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ ((π β§ π β π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)π΄ β£ (lim supβ(π β π β¦ π΅)) β β} & β’ πΊ = (π₯ β π· β¦ (lim supβ(π β π β¦ π΅))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfliminflem 45546* | The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} & β’ πΊ = (π₯ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ₯)))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfliminf 45547* | The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (lim infβ(π β π β¦ ((πΉβπ)βπ₯))) β β} & β’ πΊ = (π₯ β π· β¦ (lim infβ(π β π β¦ ((πΉβπ)βπ₯)))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfliminfmpt 45548* | The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . π΄ can contain π as a free variable, in other words it can be thought of as an indexed collection π΄(π). π΅ can be thought of as a collection with two indices π΅(π, π₯). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ ((π β§ π β π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)π΄ β£ (lim infβ(π β π β¦ π΅)) β β} & β’ πΊ = (π₯ β π· β¦ (lim infβ(π β π β¦ π΅))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | adddmmbl 45549 | If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β dom (π₯ β (π΄ β© π΅) β¦ (πΆ + π·)) β π) | ||
Theorem | adddmmbl2 45550 | If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
β’ β²π₯πΉ & β’ β²π₯πΊ & β’ (π β π β SAlg) & β’ (π β dom πΉ β π) & β’ (π β dom πΊ β π) & β’ π» = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) + (πΊβπ₯))) β β’ (π β dom π» β π) | ||
Theorem | muldmmbl 45551 | If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β dom (π₯ β (π΄ β© π΅) β¦ (πΆ Β· π·)) β π) | ||
Theorem | muldmmbl2 45552 | If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.) |
β’ β²π₯πΉ & β’ β²π₯πΊ & β’ (π β π β SAlg) & β’ (π β dom πΉ β π) & β’ (π β dom πΊ β π) & β’ π» = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯))) β β’ (π β dom π» β π) | ||
Theorem | smfdmmblpimne 45553* | If a measurable function w.r.t. to a sigma-algebra has domain in the sigma-algebra, the set of elements that are not mapped to a given real, is in the sigma-algebra (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) & β’ (π β πΆ β β) & β’ π· = {π₯ β π΄ β£ π΅ β πΆ} β β’ (π β π· β π) | ||
Theorem | smfdivdmmbl 45554 | If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator (it is needed only for the function at the denominator). (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯π΅ & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ ((π β§ π₯ β π΅) β π· β π) & β’ (π β (π₯ β π΅ β¦ π·) β (SMblFnβπ)) & β’ πΈ = {π₯ β π΅ β£ π· β 0} β β’ (π β (π΄ β© πΈ) β π) | ||
Theorem | smfpimne 45555* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value in the extended reals is in the subspace of sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ & β’ (π β π΄ β β*) β β’ (π β {π₯ β π· β£ (πΉβπ₯) β π΄} β (π βΎt π·)) | ||
Theorem | smfpimne2 45556* | Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value is in the subspace sigma-algebra induced by its domain. Notice that π΄ is not assumed to be an extended real. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯πΉ & β’ (π β π β SAlg) & β’ (π β πΉ β (SMblFnβπ)) & β’ π· = dom πΉ β β’ (π β {π₯ β π· β£ (πΉβπ₯) β π΄} β (π βΎt π·)) | ||
Theorem | smfdivdmmbl2 45557 | If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator. It is required only for the function at the denominator. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
β’ β²π₯π & β’ β²π₯πΉ & β’ β²π₯πΊ & β’ (π β π β SAlg) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΊ β (SMblFnβπ)) & β’ (π β π΄ β π) & β’ (π β dom πΊ β π) & β’ π· = {π₯ β dom πΊ β£ (πΊβπ₯) β 0} & β’ π» = (π₯ β (dom πΉ β© π·) β¦ ((πΉβπ₯) / (πΊβπ₯))) β β’ (π β dom π» β π) | ||
Theorem | fsupdm 45558* | The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ*) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < π})) β β’ (π β π· = βͺ π β β β© π β π ((π»βπ)βπ)) | ||
Theorem | fsupdm2 45559* | The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ*) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < π})) β β’ (π β dom πΊ = βͺ π β β β© π β π ((π»βπ)βπ)) | ||
Theorem | smfsupdmmbllem 45560* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ ((π β§ π β π) β dom (πΉβπ) β π) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ ((πΉβπ)βπ₯) < π})) & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β dom πΊ β π) | ||
Theorem | smfsupdmmbl 45561* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ ((π β§ π β π) β dom (πΉβπ) β π) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π ((πΉβπ)βπ₯) β€ π¦} & β’ πΊ = (π₯ β π· β¦ sup(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β dom πΊ β π) | ||
Theorem | finfdm 45562* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 45534. Note that this definition of the inf function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fifth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ*) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)})) β β’ (π β π· = βͺ π β β β© π β π ((π»βπ)βπ)) | ||
Theorem | finfdm2 45563* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 45534. Note that this definition of the inf function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fifth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ ((π β§ π β π) β (πΉβπ):dom (πΉβπ)βΆβ*) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} & β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)})) β β’ (π β dom πΊ = βͺ π β β β© π β π ((π»βπ)βπ)) | ||
Theorem | smfinfdmmbllem 45564* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their infimum function has the domain in the sigma-algebra. This is the fifth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²ππ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ ((π β§ π β π) β dom (πΉβπ) β π) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} & β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) & β’ π» = (π β π β¦ (π β β β¦ {π₯ β dom (πΉβπ) β£ -π < ((πΉβπ)βπ₯)})) β β’ (π β dom πΊ β π) | ||
Theorem | smfinfdmmbl 45565* | If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their infimum function has the domain in the sigma-algebra. This is the fifth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 1-Feb-2025.) |
β’ β²ππ & β’ β²π₯π & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ ((π β§ π β π) β dom (πΉβπ) β π) & β’ π· = {π₯ β β© π β π dom (πΉβπ) β£ βπ¦ β β βπ β π π¦ β€ ((πΉβπ)βπ₯)} & β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ ((πΉβπ)βπ₯)), β, < )) β β’ (π β dom πΊ β π) | ||
Theorem | sigarval 45566* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = (ββ((ββπ΄) Β· π΅))) | ||
Theorem | sigarim 45567* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) β β) | ||
Theorem | sigarac 45568* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = -(π΅πΊπ΄)) | ||
Theorem | sigaraf 45569* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ)πΊπ΅) = ((π΄πΊπ΅) + (πΆπΊπ΅))) | ||
Theorem | sigarmf 45570* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊπ΅) = ((π΄πΊπ΅) β (πΆπΊπ΅))) | ||
Theorem | sigaras 45571* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ + πΆ)) = ((π΄πΊπ΅) + (π΄πΊπΆ))) | ||
Theorem | sigarms 45572* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ β πΆ)) = ((π΄πΊπ΅) β (π΄πΊπΆ))) | ||
Theorem | sigarls 45573* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ Β· πΆ)) = ((π΄πΊπ΅) Β· πΆ)) | ||
Theorem | sigarid 45574* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ (π΄ β β β (π΄πΊπ΄) = 0) | ||
Theorem | sigarexp 45575* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊ(π΅ β πΆ)) = (((π΄πΊπ΅) β (π΄πΊπΆ)) β (πΆπΊπ΅))) | ||
Theorem | sigarperm 45576* | Signed area (π΄ β πΆ)πΊ(π΅ β πΆ) acts as a double area of a triangle π΄π΅πΆ. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊ(π΅ β πΆ)) = ((π΅ β π΄)πΊ(πΆ β π΄))) | ||
Theorem | sigardiv 45577* | If signed area between vectors π΅ β π΄ and πΆ β π΄ is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β Β¬ πΆ = π΄) & β’ (π β ((π΅ β π΄)πΊ(πΆ β π΄)) = 0) β β’ (π β ((π΅ β π΄) / (πΆ β π΄)) β β) | ||
Theorem | sigarimcd 45578* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β)) β β’ (π β (π΄πΊπ΅) β β) | ||
Theorem | sigariz 45579* | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β)) & β’ (π β (π΄πΊπ΅) = 0) β β’ (π β (π΅πΊπ΄) = 0) | ||
Theorem | sigarcol 45580* | Given three points π΄, π΅ and πΆ such that Β¬ π΄ = π΅, the point πΆ lies on the line going through π΄ and π΅ iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β Β¬ π΄ = π΅) β β’ (π β (((π΄ β πΆ)πΊ(π΅ β πΆ)) = 0 β βπ‘ β β πΆ = (π΅ + (π‘ Β· (π΄ β π΅))))) | ||
Theorem | sharhght 45581* | Let π΄π΅πΆ be a triangle, and let π· lie on the line π΄π΅. Then (doubled) areas of triangles π΄π·πΆ and πΆπ·π΅ relate as lengths of corresponding bases π΄π· and π·π΅. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ ((π΄ β π·)πΊ(π΅ β π·)) = 0)) β β’ (π β (((πΆ β π΄)πΊ(π· β π΄)) Β· (π΅ β π·)) = (((πΆ β π΅)πΊ(π· β π΅)) Β· (π΄ β π·))) | ||
Theorem | sigaradd 45582* | Subtracting (double) area of π΄π·πΆ from π΄π΅πΆ yields the (double) area of π·π΅πΆ. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ ((π΄ β π·)πΊ(π΅ β π·)) = 0)) β β’ (π β (((π΅ β πΆ)πΊ(π΄ β πΆ)) β ((π· β πΆ)πΊ(π΄ β πΆ))) = ((π΅ β πΆ)πΊ(π· β πΆ))) | ||
Theorem | cevathlem1 45583 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ πΈ β β β§ πΉ β β)) & β’ (π β (πΊ β β β§ π» β β β§ πΎ β β)) & β’ (π β (π΄ β 0 β§ πΈ β 0 β§ πΆ β 0)) & β’ (π β ((π΄ Β· π΅) = (πΆ Β· π·) β§ (πΈ Β· πΉ) = (π΄ Β· πΊ) β§ (πΆ Β· π») = (πΈ Β· πΎ))) β β’ (π β ((π΅ Β· πΉ) Β· π») = ((π· Β· πΊ) Β· πΎ)) | ||
Theorem | cevathlem2 45584* | Ceva's theorem second lemma. Relate (doubled) areas of triangles πΆπ΄π and π΄π΅π with of segments π΅π· and π·πΆ. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (πΉ β β β§ π· β β β§ πΈ β β)) & β’ (π β π β β) & β’ (π β (((π΄ β π)πΊ(π· β π)) = 0 β§ ((π΅ β π)πΊ(πΈ β π)) = 0 β§ ((πΆ β π)πΊ(πΉ β π)) = 0)) & β’ (π β (((π΄ β πΉ)πΊ(π΅ β πΉ)) = 0 β§ ((π΅ β π·)πΊ(πΆ β π·)) = 0 β§ ((πΆ β πΈ)πΊ(π΄ β πΈ)) = 0)) & β’ (π β (((π΄ β π)πΊ(π΅ β π)) β 0 β§ ((π΅ β π)πΊ(πΆ β π)) β 0 β§ ((πΆ β π)πΊ(π΄ β π)) β 0)) β β’ (π β (((πΆ β π)πΊ(π΄ β π)) Β· (π΅ β π·)) = (((π΄ β π)πΊ(π΅ β π)) Β· (π· β πΆ))) | ||
Theorem | cevath 45585* |
Ceva's theorem. Let π΄π΅πΆ be a triangle and let points πΉ,
π· and πΈ lie on sides π΄π΅, π΅πΆ, πΆπ΄
correspondingly. Suppose that cevians π΄π·, π΅πΈ and πΆπΉ
intersect at one point π. Then triangle's sides are
partitioned
into segments and their lengths satisfy a certain identity. Here we
obtain a bit stronger version by using complex numbers themselves
instead of their absolute values.
The proof goes by applying cevathlem2 45584 three times and then using cevathlem1 45583 to multiply obtained identities and prove the theorem. In the theorem statement we are using function πΊ as a collinearity indicator. For justification of that use, see sigarcol 45580. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (πΉ β β β§ π· β β β§ πΈ β β)) & β’ (π β π β β) & β’ (π β (((π΄ β π)πΊ(π· β π)) = 0 β§ ((π΅ β π)πΊ(πΈ β π)) = 0 β§ ((πΆ β π)πΊ(πΉ β π)) = 0)) & β’ (π β (((π΄ β πΉ)πΊ(π΅ β πΉ)) = 0 β§ ((π΅ β π·)πΊ(πΆ β π·)) = 0 β§ ((πΆ β πΈ)πΊ(π΄ β πΈ)) = 0)) & β’ (π β (((π΄ β π)πΊ(π΅ β π)) β 0 β§ ((π΅ β π)πΊ(πΆ β π)) β 0 β§ ((πΆ β π)πΊ(π΄ β π)) β 0)) β β’ (π β (((π΄ β πΉ) Β· (πΆ β πΈ)) Β· (π΅ β π·)) = (((πΉ β π΅) Β· (πΈ β π΄)) Β· (π· β πΆ))) | ||
Theorem | simpcntrab 45586 | The center of a simple group is trivial or the group is abelian. (Contributed by SS, 3-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntrβπΊ) & β’ (π β πΊ β SimpGrp) β β’ (π β (π = { 0 } β¨ πΊ β Abel)) | ||
Theorem | et-ltneverrefl 45587 | Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11323. (New usage is discouraged.) |
β’ Β¬ π΄ < π΄ | ||
Theorem | et-equeucl 45588 | Alternative proof that equality is left-Euclidean, using ax7 2020 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024.) |
β’ (π₯ = π§ β (π¦ = π§ β π₯ = π¦)) | ||
Theorem | et-sqrtnegnre 45589 | The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.) |
β’ ((π΄ β β β§ π΄ < 0) β Β¬ (ββπ΄) β β) | ||
Theorem | natlocalincr 45590* | Global monotonicity on half-open range implies local monotonicity. Inference form. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ βπ β (0..^π)βπ‘ β (1..^(π + 1))(π < π‘ β (π΅βπ) < (π΅βπ‘)) β β’ βπ β (0..^π)(π΅βπ) < (π΅β(π + 1)) | ||
Theorem | natglobalincr 45591* | Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024.) |
β’ βπ β (0..^π)(π΅βπ) < (π΅β(π + 1)) & β’ π β β€ β β’ βπ β (0..^π)βπ‘ β ((π + 1)...π)(π΅βπ) < (π΅βπ‘) | ||
Syntax | cupword 45592 | Extend class notation to include the set of strictly increasing sequences. |
class UpWord π | ||
Definition | df-upword 45593* | Strictly increasing sequence is a sequence, adjacent elements of which increase. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ UpWord π = {π€ β£ (π€ β Word π β§ βπ β (0..^((β―βπ€) β 1))(π€βπ) < (π€β(π + 1)))} | ||
Theorem | upwordnul 45594 | Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ β β UpWord π | ||
Theorem | upwordisword 45595 | Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ (π΄ β UpWord π β π΄ β Word π) | ||
Theorem | singoutnword 45596 | Singleton with character out of range π is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β V β β’ (Β¬ π΄ β π β Β¬ β¨βπ΄ββ© β Word π) | ||
Theorem | singoutnupword 45597 | Singleton with character out of range π is not an increasing sequence for that range. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ π΄ β V β β’ (Β¬ π΄ β π β Β¬ β¨βπ΄ββ© β UpWord π) | ||
Theorem | upwordsing 45598 | Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β π β β’ β¨βπ΄ββ© β UpWord π | ||
Theorem | upwordsseti 45599 | Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π β V β β’ UpWord π β V | ||
Theorem | tworepnotupword 45600 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ π΄ β V β β’ Β¬ (β¨βπ΄ββ© ++ β¨βπ΄ββ©) β UpWord π |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |