![]() |
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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smfmul 45501* | 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 45502* | 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 45503* | 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 45504* | 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 45505* | 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 45506 | 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 45507* | 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 45508 | 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 45509* | The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π β SAlg) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) β β’ (π β (π₯ β π΄ β¦ -π΅) β (SMblFnβπ)) | ||
Theorem | smffmptf 45510 | 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 45511* | 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 45512* | 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 45483 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ β²π₯πΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β SAlg) & β’ (π β πΉ:πβΆ(SMblFnβπ)) & β’ π· = {π₯ β βͺ π β π β© π β (β€β₯βπ)dom (πΉβπ) β£ (π β π β¦ ((πΉβπ)βπ₯)) β dom β } & β’ πΊ = (π₯ β π· β¦ ( β β(π β π β¦ ((πΉβπ)βπ₯)))) β β’ (π β πΊ β (SMblFnβπ)) | ||
Theorem | smfpimcclem 45513* | Lemma for smfpimcc 45514 given the choice function πΆ. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ π β π & β’ (π β π β π) & β’ ((π β§ π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β (πΆβπ¦) β π¦) & β’ π» = (π β π β¦ (πΆβ{π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) | ||
Theorem | smfpimcc 45514* | 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 45515* | 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 45516* | 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 45517* | 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 45518* | 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 45519* | 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 45520* | 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 45521* | 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 45522* | 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 45523* | 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 45524* | 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 45525* | 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 45526* | If π» converges, the lim sup of πΉ is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β πΎ β π) β β’ (π β dom (π»βπΎ) β dom (πΉβπΎ)) | ||
Theorem | smflimsuplem2 45527* | 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 45528* | 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 45529* | 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 45530* | π» 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 45531* | 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 45532* | 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 45533* | 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 45534* | 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 45535* | 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 45536* | 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 45537* | 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 45538* | 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 45539 | 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 45540 | 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 45541 | 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 45542 | 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 45543* | 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 45544 | 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 45545* | 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 45546* | 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 45547 | 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 45548* | 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 45549* | 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 45550* | 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 45551* | 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 45552* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 45524. 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 45553* | The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 45524. 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 45554* | 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 45555* | 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 45556* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = (ββ((ββπ΄) Β· π΅))) | ||
Theorem | sigarim 45557* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) β β) | ||
Theorem | sigarac 45558* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = -(π΅πΊπ΄)) | ||
Theorem | sigaraf 45559* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ)πΊπ΅) = ((π΄πΊπ΅) + (πΆπΊπ΅))) | ||
Theorem | sigarmf 45560* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊπ΅) = ((π΄πΊπ΅) β (πΆπΊπ΅))) | ||
Theorem | sigaras 45561* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ + πΆ)) = ((π΄πΊπ΅) + (π΄πΊπΆ))) | ||
Theorem | sigarms 45562* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ β πΆ)) = ((π΄πΊπ΅) β (π΄πΊπΆ))) | ||
Theorem | sigarls 45563* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ Β· πΆ)) = ((π΄πΊπ΅) Β· πΆ)) | ||
Theorem | sigarid 45564* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ (π΄ β β β (π΄πΊπ΄) = 0) | ||
Theorem | sigarexp 45565* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊ(π΅ β πΆ)) = (((π΄πΊπ΅) β (π΄πΊπΆ)) β (πΆπΊπ΅))) | ||
Theorem | sigarperm 45566* | 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 45567* | 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 45568* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β)) β β’ (π β (π΄πΊπ΅) β β) | ||
Theorem | sigariz 45569* | 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 45570* | 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 45571* | 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 45572* | Subtracting (double) area of π΄π·πΆ from π΄π΅πΆ yields the (double) area of π·π΅πΆ. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ ((π΄ β π·)πΊ(π΅ β π·)) = 0)) β β’ (π β (((π΅ β πΆ)πΊ(π΄ β πΆ)) β ((π· β πΆ)πΊ(π΄ β πΆ))) = ((π΅ β πΆ)πΊ(π· β πΆ))) | ||
Theorem | cevathlem1 45573 | 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 45574* | 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 45575* |
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 45574 three times and then using cevathlem1 45573 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 45570. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (πΉ β β β§ π· β β β§ πΈ β β)) & β’ (π β π β β) & β’ (π β (((π΄ β π)πΊ(π· β π)) = 0 β§ ((π΅ β π)πΊ(πΈ β π)) = 0 β§ ((πΆ β π)πΊ(πΉ β π)) = 0)) & β’ (π β (((π΄ β πΉ)πΊ(π΅ β πΉ)) = 0 β§ ((π΅ β π·)πΊ(πΆ β π·)) = 0 β§ ((πΆ β πΈ)πΊ(π΄ β πΈ)) = 0)) & β’ (π β (((π΄ β π)πΊ(π΅ β π)) β 0 β§ ((π΅ β π)πΊ(πΆ β π)) β 0 β§ ((πΆ β π)πΊ(π΄ β π)) β 0)) β β’ (π β (((π΄ β πΉ) Β· (πΆ β πΈ)) Β· (π΅ β π·)) = (((πΉ β π΅) Β· (πΈ β π΄)) Β· (π· β πΆ))) | ||
Theorem | simpcntrab 45576 | 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 45577 | Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11322. (New usage is discouraged.) |
β’ Β¬ π΄ < π΄ | ||
Theorem | et-equeucl 45578 | Alternative proof that equality is left-Euclidean, using ax7 2019 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024.) |
β’ (π₯ = π§ β (π¦ = π§ β π₯ = π¦)) | ||
Theorem | et-sqrtnegnre 45579 | The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.) |
β’ ((π΄ β β β§ π΄ < 0) β Β¬ (ββπ΄) β β) | ||
Theorem | natlocalincr 45580* | 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 45581* | 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 45582 | Extend class notation to include the set of strictly increasing sequences. |
class UpWord π | ||
Definition | df-upword 45583* | 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 45584 | Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ β β UpWord π | ||
Theorem | upwordisword 45585 | Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ (π΄ β UpWord π β π΄ β Word π) | ||
Theorem | singoutnword 45586 | Singleton with character out of range π is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β V β β’ (Β¬ π΄ β π β Β¬ β¨βπ΄ββ© β Word π) | ||
Theorem | singoutnupword 45587 | 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 45588 | Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β π β β’ β¨βπ΄ββ© β UpWord π | ||
Theorem | upwordsseti 45589 | Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π β V β β’ UpWord π β V | ||
Theorem | tworepnotupword 45590 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ π΄ β V β β’ Β¬ (β¨βπ΄ββ© ++ β¨βπ΄ββ©) β UpWord π | ||
Theorem | upwrdfi 45591* | 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 45592 | 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.) |
β’ ((Β¬ π β Β¬ π) β ((Β¬ π β π) β π)) | ||
Theorem | ax3h 45593 | Recover ax-3 8 from hirstL-ax3 45592. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((Β¬ π β Β¬ π) β (π β π)) | ||
Theorem | aibandbiaiffaiffb 45594 | A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β π) β§ (π β π)) β (π β π)) | ||
Theorem | aibandbiaiaiffb 45595 | A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.) |
β’ (((π β π) β§ (π β π)) β (π β π)) | ||
Theorem | notatnand 45596 | Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ Β¬ π β β’ Β¬ (π β§ π) | ||
Theorem | aistia 45597 | Given a is equivalent to β€, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β€) β β’ π | ||
Theorem | aisfina 45598 | Given a is equivalent to β₯, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β₯) β β’ Β¬ π | ||
Theorem | bothtbothsame 45599 | Given both a, b are equivalent to β€, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ (π β β€) & β’ (π β β€) β β’ (π β π) | ||
Theorem | bothfbothsame 45600 | Given both a, b are equivalent to β₯, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ (π β β₯) & β’ (π β β₯) β β’ (π β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |