Home | Metamath
Proof Explorer Theorem List (p. 411 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smfmullem4 41001* | 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 ↾t | ||
Theorem | smfmul 41002* | 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 41003* | 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 41004* | 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 SMblFn | ||
Theorem | smfpimbor1lem1 41005* | 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 ↾t | ||
Theorem | smfpimbor1lem2 41006* | 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 SalGen ↾t ↾t | ||
Theorem | smfpimbor1 41007 | 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 SalGen ↾t | ||
Theorem | smf2id 41008* | Twice the identity function is Borel sigma-measurable (just an example, to test previous general theorems). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
SalGen SMblFn | ||
Theorem | smfco 41009 | 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 SalGen SMblFn SMblFn | ||
Theorem | smfneg 41010* | The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
SAlg SMblFn SMblFn | ||
Theorem | smffmpt 41011* | 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 41012* | 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 less distinct variable restrictions than smflim and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
SAlg SMblFn SMblFn | ||
Theorem | smfpimcclem 41013* | Lemma for smfpimcc 41014 given the choice function . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Theorem | smfpimcc 41014* | 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 SalGen | ||
Theorem | issmfle2d 41015* | 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 41016* | 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 indexes . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
SAlg SMblFn SMblFn | ||
Theorem | smfsuplem1 41017* | 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 ↾t | ||
Theorem | smfsuplem2 41018* | 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 ↾t | ||
Theorem | smfsuplem3 41019* | 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 SMblFn | ||
Theorem | smfsup 41020* | 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 SMblFn | ||
Theorem | smfsupmpt 41021* | 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 SMblFn | ||
Theorem | smfsupxr 41022* | 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 SMblFn | ||
Theorem | smfinflem 41023* | 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 SMblFn | ||
Theorem | smfinf 41024* | 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 SMblFn | ||
Theorem | smfinfmpt 41025* | 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 SMblFn | ||
Theorem | smflimsuplem1 41026* | If converges, the of is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Theorem | smflimsuplem2 41027* | 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 | ||
Theorem | smflimsuplem3 41028* | The limit of the functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
SAlg SMblFn SMblFn | ||
Theorem | smflimsuplem4 41029* | If converges, the of is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
SAlg SMblFn | ||
Theorem | smflimsuplem5 41030* | converges to the superior limit of . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
SAlg SMblFn | ||
Theorem | smflimsuplem6 41031* | 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 | ||
Theorem | smflimsuplem7 41032* | 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 | ||
Theorem | smflimsuplem8 41033* | 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 SMblFn | ||
Theorem | smflimsup 41034* | 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 SMblFn | ||
Theorem | smflimsupmpt 41035* | 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 indexes . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
SAlg SMblFn SMblFn | ||
Theorem | smfliminflem 41036* | 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 liminf liminf SMblFn | ||
Theorem | smfliminf 41037* | 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 liminf liminf SMblFn | ||
Theorem | smfliminfmpt 41038* | 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 indexes . (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
SAlg SMblFn liminf liminf SMblFn | ||
Theorem | sigarval 41039* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarim 41040* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarac 41041* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigaraf 41042* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarmf 41043* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigaras 41044* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarms 41045* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarls 41046* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarid 41047* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
Theorem | sigarexp 41048* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
Theorem | sigarperm 41049* | 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 41050* | If signed area between vectors and is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
Theorem | sigarimcd 41051* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
Theorem | sigariz 41052* | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
Theorem | sigarcol 41053* | 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.) |
Theorem | sharhght 41054* | 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.) |
Theorem | sigaradd 41055* | Subtracting (double) area of from yields the (double) area of . (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
Theorem | cevathlem1 41056 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
Theorem | cevathlem2 41057* | Ceva's theorem second lemma. Relate (doubled) areas of triangles and with of segments and . (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
Theorem | cevath 41058* |
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 41057 three times and then using cevathlem1 41056 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 41053. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
Theorem | hirstL-ax3 41059 | 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 41060 | Recovery of ax-3 8 from hirstL-ax3 41059. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | aibandbiaiffaiffb 41061 | 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 41062 | 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 41063 | 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 41064 | Given a is equivalent to , there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
Theorem | aisfina 41065 | Given a is equivalent to , there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.) |
Theorem | bothtbothsame 41066 | 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 41067 | 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 41068 | 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 41069 | 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 41070 | Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1465 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
Theorem | aiffnbandciffatnotciffb 41071 | 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 41072 | 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 41073 | Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.) |
Theorem | aibnbaif 41074 | Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.) |
Theorem | aiffbtbat 41075 | 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 41076 | 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 41077 | 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 41078 | Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.) |
Theorem | atbiffatnnb 41079 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.) |
Theorem | bisaiaisb 41080 | Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
Theorem | atbiffatnnbalt 41081 | If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.) |
Theorem | abnotbtaxb 41082 | Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
Theorem | abnotataxb 41083 | Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.) |
Theorem | conimpf 41084 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.) |
Theorem | conimpfalt 41085 | Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.) |
Theorem | aistbisfiaxb 41086 | Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
Theorem | aisfbistiaxb 41087 | Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.) |
Theorem | aifftbifffaibif 41088 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
Theorem | aifftbifffaibifff 41089 | Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
Theorem | atnaiana 41090 | Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
Theorem | ainaiaandna 41091 | Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
Theorem | abcdta 41092 | Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
Theorem | abcdtb 41093 | Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
Theorem | abcdtc 41094 | Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
Theorem | abcdtd 41095 | Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.) |
Theorem | abciffcbatnabciffncba 41096 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
Theorem | abciffcbatnabciffncbai 41097 | Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.) |
Theorem | nabctnabc 41098 | not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.) |
Theorem | jabtaib 41099 | For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.) |
Theorem | onenotinotbothi 41100 | From one negated implication it is not the case its non negated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |