Home | Metamath
Proof Explorer Theorem List (p. 449 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smfpimcclem 44801* | Lemma for smfpimcc 44802 given the choice function πΆ. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ π β π & β’ (π β π β π) & β’ ((π β§ π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β (πΆβπ¦) β π¦) & β’ π» = (π β π β¦ (πΆβ{π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) | ||
Theorem | smfpimcc 44802* | 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 44803* | 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 44804* | 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 44805* | 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 44806* | 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 44807* | 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 44808* | 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 44809* | 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 44810* | 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 44811* | 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 44812* | 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 44813* | 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 44814* | If π» converges, the lim sup of πΉ is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ πΈ = (π β π β¦ {π₯ β β© π β (β€β₯βπ)dom (πΉβπ) β£ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ) β β}) & β’ π» = (π β π β¦ (π₯ β (πΈβπ) β¦ sup(ran (π β (β€β₯βπ) β¦ ((πΉβπ)βπ₯)), β*, < ))) & β’ (π β πΎ β π) β β’ (π β dom (π»βπΎ) β dom (πΉβπΎ)) | ||
Theorem | smflimsuplem2 44815* | 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 44816* | 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 44817* | 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 44818* | π» 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 44819* | 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 44820* | 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 44821* | 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 44822* | 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 44823* | 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 44824* | 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 44825* | 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 44826* | 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 44827 | 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 44828 | 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 44829 | 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 44830 | 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 44831* | 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 44832 | 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 44833* | 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 44834* | 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 44835 | 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 44836* | 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 44837* | 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 44838* | 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 44839* | 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 | sigarval 44840* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = (ββ((ββπ΄) Β· π΅))) | ||
Theorem | sigarim 44841* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) β β) | ||
Theorem | sigarac 44842* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β) β (π΄πΊπ΅) = -(π΅πΊπ΄)) | ||
Theorem | sigaraf 44843* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + πΆ)πΊπ΅) = ((π΄πΊπ΅) + (πΆπΊπ΅))) | ||
Theorem | sigarmf 44844* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊπ΅) = ((π΄πΊπ΅) β (πΆπΊπ΅))) | ||
Theorem | sigaras 44845* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ + πΆ)) = ((π΄πΊπ΅) + (π΄πΊπΆ))) | ||
Theorem | sigarms 44846* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ β πΆ)) = ((π΄πΊπ΅) β (π΄πΊπΆ))) | ||
Theorem | sigarls 44847* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΄πΊ(π΅ Β· πΆ)) = ((π΄πΊπ΅) Β· πΆ)) | ||
Theorem | sigarid 44848* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ (π΄ β β β (π΄πΊπ΄) = 0) | ||
Theorem | sigarexp 44849* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ β πΆ)πΊ(π΅ β πΆ)) = (((π΄πΊπ΅) β (π΄πΊπΆ)) β (πΆπΊπ΅))) | ||
Theorem | sigarperm 44850* | 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 44851* | 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 44852* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β)) β β’ (π β (π΄πΊπ΅) β β) | ||
Theorem | sigariz 44853* | 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 44854* | 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 44855* | 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 44856* | Subtracting (double) area of π΄π·πΆ from π΄π΅πΆ yields the (double) area of π·π΅πΆ. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (π· β β β§ ((π΄ β π·)πΊ(π΅ β π·)) = 0)) β β’ (π β (((π΅ β πΆ)πΊ(π΄ β πΆ)) β ((π· β πΆ)πΊ(π΄ β πΆ))) = ((π΅ β πΆ)πΊ(π· β πΆ))) | ||
Theorem | cevathlem1 44857 | 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 44858* | 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 44859* |
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 44858 three times and then using cevathlem1 44857 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 44854. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
β’ πΊ = (π₯ β β, π¦ β β β¦ (ββ((ββπ₯) Β· π¦))) & β’ (π β (π΄ β β β§ π΅ β β β§ πΆ β β)) & β’ (π β (πΉ β β β§ π· β β β§ πΈ β β)) & β’ (π β π β β) & β’ (π β (((π΄ β π)πΊ(π· β π)) = 0 β§ ((π΅ β π)πΊ(πΈ β π)) = 0 β§ ((πΆ β π)πΊ(πΉ β π)) = 0)) & β’ (π β (((π΄ β πΉ)πΊ(π΅ β πΉ)) = 0 β§ ((π΅ β π·)πΊ(πΆ β π·)) = 0 β§ ((πΆ β πΈ)πΊ(π΄ β πΈ)) = 0)) & β’ (π β (((π΄ β π)πΊ(π΅ β π)) β 0 β§ ((π΅ β π)πΊ(πΆ β π)) β 0 β§ ((πΆ β π)πΊ(π΄ β π)) β 0)) β β’ (π β (((π΄ β πΉ) Β· (πΆ β πΈ)) Β· (π΅ β π·)) = (((πΉ β π΅) Β· (πΈ β π΄)) Β· (π· β πΆ))) | ||
Theorem | simpcntrab 44860 | 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 44861 | Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11197. (New usage is discouraged.) |
β’ Β¬ π΄ < π΄ | ||
Theorem | et-equeucl 44862 | 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 44863 | The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.) |
β’ ((π΄ β β β§ π΄ < 0) β Β¬ (ββπ΄) β β) | ||
Theorem | natlocalincr 44864* | 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 44865* | 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 44866 | Extend class notation to include the set of strictly increasing sequences. |
class UpWordπ | ||
Definition | df-upword 44867* | 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 44868 | Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ β β UpWordπ | ||
Theorem | upwordisword 44869 | Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.) |
β’ (π΄ β UpWordπ β π΄ β Word π) | ||
Theorem | singoutnword 44870 | Singleton with character out of range π is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β V β β’ (Β¬ π΄ β π β Β¬ β¨βπ΄ββ© β Word π) | ||
Theorem | singoutnupword 44871 | 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 44872 | Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π΄ β π β β’ β¨βπ΄ββ© β UpWordπ | ||
Theorem | upwordsseti 44873 | Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) |
β’ π β V β β’ UpWordπ β V | ||
Theorem | tworepnotupword 44874 | Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.) |
β’ π΄ β V β β’ Β¬ (β¨βπ΄ββ© ++ β¨βπ΄ββ©) β UpWordπ | ||
Theorem | upwrdfi 44875* | 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 44876 | 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 44877 | Recover ax-3 8 from hirstL-ax3 44876. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((Β¬ π β Β¬ π) β (π β π)) | ||
Theorem | aibandbiaiffaiffb 44878 | 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 44879 | 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 44880 | 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 44881 | Given a is equivalent to β€, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β€) β β’ π | ||
Theorem | aisfina 44882 | Given a is equivalent to β₯, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β β₯) β β’ Β¬ π | ||
Theorem | bothtbothsame 44883 | 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 44884 | 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 | aiffbbtat 44885 | Given a is equivalent to b, b is equivalent to β€ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ (π β π) & β’ (π β β€) β β’ (π β β€) | ||
Theorem | aisbbisfaisf 44886 | Given a is equivalent to b, b is equivalent to β₯ there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
β’ (π β π) & β’ (π β β₯) β β’ (π β β₯) | ||
Theorem | axorbtnotaiffb 44887 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1510 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
β’ (π β» π) β β’ Β¬ (π β π) | ||
Theorem | aiffnbandciffatnotciffb 44888 | Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
β’ (π β Β¬ π) & β’ (π β π) β β’ Β¬ (π β π) | ||
Theorem | axorbciffatcxorb 44889 | Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016.) |
β’ (π β» π) & β’ (π β π) β β’ (π β» π) | ||
Theorem | aibnbna 44890 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
β’ (π β π) & β’ Β¬ π β β’ Β¬ π | ||
Theorem | aibnbaif 44891 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
β’ (π β π) & β’ Β¬ π β β’ (π β β₯) | ||
Theorem | aiffbtbat 44892 | Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ (π β π) & β’ (β€ β π) β β’ (π β β€) | ||
Theorem | astbstanbst 44893 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ (π β β€) & β’ (π β β€) β β’ ((π β§ π) β β€) | ||
Theorem | aistbistaandb 44894 | Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.) |
β’ (π β β€) & β’ (π β β€) β β’ (π β§ π) | ||
Theorem | aisbnaxb 44895 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
β’ (π β π) β β’ Β¬ (π β» π) | ||
Theorem | atbiffatnnb 44896 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
β’ ((π β π) β (π β Β¬ Β¬ π)) | ||
Theorem | bisaiaisb 44897 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ ((π β π) β (π β π)) | ||
Theorem | atbiffatnnbalt 44898 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
β’ ((π β π) β (π β Β¬ Β¬ π)) | ||
Theorem | abnotbtaxb 44899 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ π & β’ Β¬ π β β’ (π β» π) | ||
Theorem | abnotataxb 44900 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
β’ Β¬ π & β’ π β β’ (π β» π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |