![]() |
Metamath
Proof Explorer Theorem List (p. 459 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smfpimioo 45801 | 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 45802* | 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 45803* | 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 45804 | 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 45805 | 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 45806* | 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 45807* | 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 45808* | 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 45809* | 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 45810* | 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 45811* | 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 45812* | 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 45813* | 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 45814 | 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 45815* | 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 45816 | 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 45817* | The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) β β’ (π β (π₯ β π΄ β¦ -π΅) β (SMblFnβπ)) | ||
Theorem | smffmptf 45818 | 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 45819* | 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 45820* | 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 45791 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfpimcclem 45821* | Lemma for smfpimcc 45822 given the choice function πΆ. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ π β π & β’ (π β π β π) & β’ ((π β§ π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β (πΆβπ¦) β π¦) & β’ π» = (π β π β¦ (πΆβ{π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) | ||
Theorem | smfpimcc 45822* | 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 45823* | 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 45824* | 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 45825* | 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 45826* | 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 45827* | 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 45828* | 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 45829* | 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 45830* | 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 45831* | 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 45832* | 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 45833* | 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 45834* | If π» converges, the lim sup of πΉ is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β πΎ β π) β β’ (π β dom (π»βπΎ) β dom (πΉβπΎ)) | ||
Theorem | smflimsuplem2 45835* | 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 45836* | 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 45837* | 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 45838* | π» 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 45839* | 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 45840* | 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 45841* | 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 45842* | 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 45843* | 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 45844* | 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 45845* | 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 45846* | 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 45847 | 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 45848 | 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 45849 | 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 45850 | 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 45851* | 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 45852 | 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 45853* | 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 45854* | 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 45855 | 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 45856* | 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 45857* | 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 45858* | 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 45859* | 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 45860* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 45832. 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 45861* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 45832. 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 45862* | 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 45863* | 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 45864* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = (ββ((ββπ΄) Β· π΅))) | ||
Theorem | sigarim 45865* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) β β) | ||
Theorem | sigarac 45866* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = -(π΅πΊπ΄)) | ||
Theorem | sigaraf 45867* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ)πΊπ΅) = ((π΄πΊπ΅) + (πΆπΊπ΅))) | ||
Theorem | sigarmf 45868* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊπ΅) = ((π΄πΊπ΅) β (πΆπΊπ΅))) | ||
Theorem | sigaras 45869* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ + πΆ)) = ((π΄πΊπ΅) + (π΄πΊπΆ))) | ||
Theorem | sigarms 45870* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ β πΆ)) = ((π΄πΊπ΅) β (π΄πΊπΆ))) | ||
Theorem | sigarls 45871* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ Β· πΆ)) = ((π΄πΊπ΅) Β· πΆ)) | ||
Theorem | sigarid 45872* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ (π΄ β β β (π΄πΊπ΄) = 0) | ||
Theorem | sigarexp 45873* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊ(π΅ β πΆ)) = (((π΄πΊπ΅) β (π΄πΊπΆ)) β (πΆπΊπ΅))) | ||
Theorem | sigarperm 45874* | 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 45875* | 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 45876* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β)) β β’ (π β (π΄πΊπ΅) β β) | ||
Theorem | sigariz 45877* | 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 45878* | 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 45879* | 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 45880* | Subtracting (double) area of π΄π·πΆ from π΄π΅πΆ yields the (double) area of π·π΅πΆ. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ ((π΄ β π·)πΊ(π΅ β π·)) = 0)) β β’ (π β (((π΅ β πΆ)πΊ(π΄ β πΆ)) β ((π· β πΆ)πΊ(π΄ β πΆ))) = ((π΅ β πΆ)πΊ(π· β πΆ))) | ||
Theorem | cevathlem1 45881 | 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 45882* | 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 45883* |
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 45882 three times and then using cevathlem1 45881 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 45878. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (πΉ β β β§ π· β β β§ πΈ β β)) & β’ (π β π β β) & β’ (π β (((π΄ β π)πΊ(π· β π)) = 0 β§ ((π΅ β π)πΊ(πΈ β π)) = 0 β§ ((πΆ β π)πΊ(πΉ β π)) = 0)) & β’ (π β (((π΄ β πΉ)πΊ(π΅ β πΉ)) = 0 β§ ((π΅ β π·)πΊ(πΆ β π·)) = 0 β§ ((πΆ β πΈ)πΊ(π΄ β πΈ)) = 0)) & β’ (π β (((π΄ β π)πΊ(π΅ β π)) β 0 β§ ((π΅ β π)πΊ(πΆ β π)) β 0 β§ ((πΆ β π)πΊ(π΄ β π)) β 0)) β β’ (π β (((π΄ β πΉ) Β· (πΆ β πΈ)) Β· (π΅ β π·)) = (((πΉ β π΅) Β· (πΈ β π΄)) Β· (π· β πΆ))) | ||
Theorem | simpcntrab 45884 | 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 45885 | Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11327. (New usage is discouraged.) |
β’ Β¬ π΄ < π΄ | ||
Theorem | et-equeucl 45886 | Alternative proof that equality is left-Euclidean, using ax7 2017 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024.) |
β’ (π₯ = π§ β (π¦ = π§ β π₯ = π¦)) | ||
Theorem | et-sqrtnegnre 45887 | The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.) |
β’ ((π΄ β β β§ π΄ < 0) β Β¬ (ββπ΄) β β) | ||
Theorem | natlocalincr 45888* | 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 45889* | 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 45890 | Extend class notation to include the set of strictly increasing sequences. |
class UpWord π | ||
Definition | df-upword 45891* | 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 45892 | Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ β β UpWord π | ||
Theorem | upwordisword 45893 | Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ (π΄ β UpWord π β π΄ β Word π) | ||
Theorem | singoutnword 45894 | Singleton with character out of range π is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β V β β’ (Β¬ π΄ β π β Β¬ β¨βπ΄ββ© β Word π) | ||
Theorem | singoutnupword 45895 | 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 45896 | Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β π β β’ β¨βπ΄ββ© β UpWord π | ||
Theorem | upwordsseti 45897 | Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π β V β β’ UpWord π β V | ||
Theorem | tworepnotupword 45898 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ π΄ β V β β’ Β¬ (β¨βπ΄ββ© ++ β¨βπ΄ββ©) β UpWord π | ||
Theorem | upwrdfi 45899* | There is a finite number of strictly increasing sequences of a given length over finite alphabet. Trivially holds for invalid lengths where there're zero matching sequences. (Contributed by Ender Ting, 5-Jan-2024.) |
β’ (π β Fin β {π β UpWord π β£ (β―βπ) = π} β Fin) | ||
Theorem | hirstL-ax3 45900 | The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.) |
β’ ((Β¬ π β Β¬ π) β ((Β¬ π β π) β π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |