![]() |
Metamath
Proof Explorer Theorem List (p. 372 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wl-sb8motv 37101* |
Substitution of variable in universal quantifier. Closed form of
sb8mo 2589 without ax-13 2365, but requiring π₯ and π¦ being
disjoint.
This theorem relates to wl-mo3t 37096, since replacing π with [π¦ / π₯]π in the latter yields subexpressions like [π₯ / π¦][π¦ / π₯]π, which can be reduced to π via sbft 2256 and sbco 2500. So β*π₯π β β*π¦[π¦ / π₯]π is provable from wl-mo3t 37096 in a simple fashion. From an educational standpoint, one would assume wl-mo3t 37096 to be more fundamental, as it hints how the "at most one" objects on both sides of the biconditional correlate (they are the same), if they exist at all, and then prove this theorem from it. (Contributed by Wolf Lammen, 3-May-2025.) |
β’ (βπ₯β²π¦π β (β*π₯π β β*π¦[π¦ / π₯]π)) | ||
Theorem | wl-issetft 37102 | A closed form of issetf 3478. The proof here is a modification of a subproof in vtoclgft 3531, where it could be used to shorten the proof. (Contributed by Wolf Lammen, 25-Jan-2025.) |
β’ (β²π₯π΄ β (π΄ β V β βπ₯ π₯ = π΄)) | ||
Theorem | wl-axc11rc11 37103 |
Proving axc11r 2359 from axc11 2423. The hypotheses are two instances of
axc11 2423 used in the proof here. Some systems
introduce axc11 2423 as an
axiom, see for example System S2 in
https://us.metamath.org/downloads/finiteaxiom.pdf 2423.
By contrast, this database sees the variant axc11r 2359, directly derived from ax-12 2166, as foundational. Later axc11 2423 is proven somewhat trickily, requiring ax-10 2129 and ax-13 2365, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.) |
β’ (βπ¦ π¦ = π₯ β (βπ¦ π¦ = π₯ β βπ₯ π¦ = π₯)) & β’ (βπ₯ π₯ = π¦ β (βπ₯π β βπ¦π)) β β’ (βπ¦ π¦ = π₯ β (βπ₯π β βπ¦π)) | ||
Axiom | ax-wl-11v 37104* | Version of ax-11 2146 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2146. It will later be converted into a theorem directly based on ax-11 2146. (Contributed by Wolf Lammen, 28-Jun-2019.) |
β’ (βπ₯βπ¦π β βπ¦βπ₯π) | ||
Theorem | wl-ax11-lem1 37105 | A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ (βπ₯ π₯ = π¦ β (βπ₯ π₯ = π§ β βπ¦ π¦ = π§)) | ||
Theorem | wl-ax11-lem2 37106* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ ((βπ’ π’ = π¦ β§ Β¬ βπ₯ π₯ = π¦) β βπ₯ π’ = π¦) | ||
Theorem | wl-ax11-lem3 37107* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ (Β¬ βπ₯ π₯ = π¦ β β²π₯βπ’ π’ = π¦) | ||
Theorem | wl-ax11-lem4 37108* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ β²π₯(βπ’ π’ = π¦ β§ Β¬ βπ₯ π₯ = π¦) | ||
Theorem | wl-ax11-lem5 37109 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ (βπ’ π’ = π¦ β (βπ’[π’ / π¦]π β βπ¦π)) | ||
Theorem | wl-ax11-lem6 37110* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ ((βπ’ π’ = π¦ β§ Β¬ βπ₯ π₯ = π¦) β (βπ’βπ₯[π’ / π¦]π β βπ₯βπ¦π)) | ||
Theorem | wl-ax11-lem7 37111 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ (βπ₯(Β¬ βπ₯ π₯ = π¦ β§ π) β (Β¬ βπ₯ π₯ = π¦ β§ βπ₯π)) | ||
Theorem | wl-ax11-lem8 37112* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ ((βπ’ π’ = π¦ β§ Β¬ βπ₯ π₯ = π¦) β (βπ’βπ₯[π’ / π¦]π β βπ¦βπ₯π)) | ||
Theorem | wl-ax11-lem9 37113 | The easy part when π₯ coincides with π¦. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ (βπ₯ π₯ = π¦ β (βπ¦βπ₯π β βπ₯βπ¦π)) | ||
Theorem | wl-ax11-lem10 37114* | We now have prepared everything. The unwanted variable π’ is just in one place left. pm2.61 191 can be used in conjunction with wl-ax11-lem9 37113 to eliminate the second antecedent. Missing is something along the lines of ax-6 1963, so we could remove the first antecedent. But the Metamath axioms cannot accomplish this. Such a rule must reside one abstraction level higher than all others: It says that a distinctor implies a distinct variable condition on its contained setvar. This is only needed if such conditions are required, as ax-11v does. The result of this study is for me, that you cannot introduce a setvar capturing this condition, and hope to eliminate it later. (Contributed by Wolf Lammen, 30-Jun-2019.) |
β’ (βπ¦ π¦ = π’ β (Β¬ βπ₯ π₯ = π¦ β (βπ¦βπ₯π β βπ₯βπ¦π))) | ||
Theorem | wl-clabv 37115* |
Variant of df-clab 2703, where the element π₯ is required to be
disjoint from the class it is taken from. This restriction meets
similar ones found in other definitions and axioms like ax-ext 2696,
df-clel 2802 and df-cleq 2717. π₯ β π΄ with π΄ depending on π₯ can
be the source of side effects, that you rather want to be aware of. So
here we eliminate one possible way of letting this slip in instead.
An expression π₯ β π΄ with π₯, π΄ not disjoint, is now only introduced either via ax-8 2100, ax-9 2108, or df-clel 2802. Theorem cleljust 2107 shows that a possible choice does not matter. The original df-clab 2703 can be rederived, see wl-dfclab 37116. In an implementation this theorem is the only user of df-clab. (Contributed by NM, 26-May-1993.) Element and class are disjoint. (Revised by Wolf Lammen, 31-May-2023.) |
β’ (π₯ β {π¦ β£ π} β [π₯ / π¦]π) | ||
Theorem | wl-dfclab 37116 | Rederive df-clab 2703 from wl-clabv 37115. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.) |
β’ (π₯ β {π¦ β£ π} β [π₯ / π¦]π) | ||
Theorem | wl-clabtv 37117* | Using class abstraction in a context, requiring π₯ and π disjoint, but based on fewer axioms than wl-clabt 37118. (Contributed by Wolf Lammen, 29-May-2023.) |
β’ (π β {π₯ β£ π} = {π₯ β£ (π β π)}) | ||
Theorem | wl-clabt 37118 | Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 37117. (Contributed by Wolf Lammen, 29-May-2023.) |
β’ β²π₯π β β’ (π β {π₯ β£ π} = {π₯ β£ (π β π)}) | ||
Theorem | rabiun 37119* | Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.) |
β’ {π₯ β βͺ π¦ β π΄ π΅ β£ π} = βͺ π¦ β π΄ {π₯ β π΅ β£ π} | ||
Theorem | iundif1 37120* | Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.) |
β’ βͺ π₯ β π΄ (π΅ β πΆ) = (βͺ π₯ β π΄ π΅ β πΆ) | ||
Theorem | imadifss 37121 | The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ ((πΉ β π΄) β (πΉ β π΅)) β (πΉ β (π΄ β π΅)) | ||
Theorem | cureq 37122 | Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ (π΄ = π΅ β curry π΄ = curry π΅) | ||
Theorem | unceq 37123 | Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ (π΄ = π΅ β uncurry π΄ = uncurry π΅) | ||
Theorem | curf 37124 | Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ ((πΉ:(π΄ Γ π΅)βΆπΆ β§ π΅ β (π β {β }) β§ πΆ β π) β curry πΉ:π΄βΆ(πΆ βm π΅)) | ||
Theorem | uncf 37125 | Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ (πΉ:π΄βΆ(πΆ βm π΅) β uncurry πΉ:(π΄ Γ π΅)βΆπΆ) | ||
Theorem | curfv 37126 | Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ (((πΉ Fn (π Γ π) β§ π΄ β π β§ π΅ β π) β§ π β π) β ((curry πΉβπ΄)βπ΅) = (π΄πΉπ΅)) | ||
Theorem | uncov 37127 | Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄uncurry πΉπ΅) = ((πΉβπ΄)βπ΅)) | ||
Theorem | curunc 37128 | Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ ((πΉ:π΄βΆ(πΆ βm π΅) β§ π΅ β β ) β curry uncurry πΉ = πΉ) | ||
Theorem | unccur 37129 | Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.) |
β’ ((πΉ:(π΄ Γ π΅)βΆπΆ β§ π΅ β (π β {β }) β§ πΆ β π) β uncurry curry πΉ = πΉ) | ||
Theorem | phpreu 37130* | Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ ((π΄ β Fin β§ π΄ β π΅) β (βπ₯ β π΄ βπ¦ β π΅ π₯ = πΆ β βπ₯ β π΄ β!π¦ β π΅ π₯ = πΆ)) | ||
Theorem | finixpnum 37131* | A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.) |
β’ ((π΄ β Fin β§ βπ₯ β π΄ π΅ β dom card) β Xπ₯ β π΄ π΅ β dom card) | ||
Theorem | fin2solem 37132* | Lemma for fin2so 37133. (Contributed by Brendan Leahy, 29-Jun-2019.) |
β’ ((π Or π₯ β§ (π¦ β π₯ β§ π§ β π₯)) β (π¦π π§ β {π€ β π₯ β£ π€π π¦} [β] {π€ β π₯ β£ π€π π§})) | ||
Theorem | fin2so 37133 | Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.) |
β’ ((π΄ β FinII β§ π Or π΄) β π΄ β Fin) | ||
Theorem | ltflcei 37134 | Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
β’ ((π΄ β β β§ π΅ β β) β ((ββπ΄) < π΅ β π΄ < -(ββ-π΅))) | ||
Theorem | leceifl 37135 | Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
β’ ((π΄ β β β§ π΅ β β) β (-(ββ-π΄) β€ π΅ β π΄ β€ (ββπ΅))) | ||
Theorem | sin2h 37136 | Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.) |
β’ (π΄ β (0[,](2 Β· Ο)) β (sinβ(π΄ / 2)) = (ββ((1 β (cosβπ΄)) / 2))) | ||
Theorem | cos2h 37137 | Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.) |
β’ (π΄ β (-Ο[,]Ο) β (cosβ(π΄ / 2)) = (ββ((1 + (cosβπ΄)) / 2))) | ||
Theorem | tan2h 37138 | Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.) |
β’ (π΄ β (0[,)Ο) β (tanβ(π΄ / 2)) = (ββ((1 β (cosβπ΄)) / (1 + (cosβπ΄))))) | ||
Theorem | lindsadd 37139 | In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023.) |
β’ ((π β LVec β§ πΉ β (LIndSβπ) β§ π β ((Baseβπ) β ((LSpanβπ)βπΉ))) β (πΉ βͺ {π}) β (LIndSβπ)) | ||
Theorem | lindsdom 37140 | A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ ((π β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π freeLMod πΌ))) β π βΌ πΌ) | ||
Theorem | lindsenlbs 37141 | A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ (((π β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π freeLMod πΌ))) β§ π β πΌ) β π β (LBasisβ(π freeLMod πΌ))) | ||
Theorem | matunitlindflem1 37142 | One direction of matunitlindf 37144. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ (((π β Field β§ π:(πΌ Γ πΌ)βΆ(Baseβπ )) β§ πΌ β (Fin β {β })) β (Β¬ curry π LIndF (π freeLMod πΌ) β ((πΌ maDet π )βπ) = (0gβπ ))) | ||
Theorem | matunitlindflem2 37143 | One direction of matunitlindf 37144. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ ((((π β Field β§ π β (Baseβ(πΌ Mat π ))) β§ πΌ β β ) β§ curry π LIndF (π freeLMod πΌ)) β ((πΌ maDet π )βπ) β (Unitβπ )) | ||
Theorem | matunitlindf 37144 | A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.) |
β’ ((π β Field β§ π β (Baseβ(πΌ Mat π ))) β (π β (Unitβ(πΌ Mat π )) β curry π LIndF (π freeLMod πΌ))) | ||
Theorem | ptrest 37145* | Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆTop) & β’ ((π β§ π β π΄) β π β π) β β’ (π β ((βtβπΉ) βΎt Xπ β π΄ π) = (βtβ(π β π΄ β¦ ((πΉβπ) βΎt π)))) | ||
Theorem | ptrecube 37146* | Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.) |
β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ ((π β π β§ π β π) β βπ β β+ Xπ β (1...π)((πβπ)(ballβπ·)π) β π) | ||
Theorem | poimirlem1 37147* | Lemma for poimir 37179- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))) & β’ (π β π:(1...π)βΆβ€) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ (π β π β (1...(π β 1))) β β’ (π β Β¬ β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) | ||
Theorem | poimirlem2 37148* | Lemma for poimir 37179- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))) & β’ (π β π:(1...π)βΆβ€) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ (π β π β (1...(π β 1))) & β’ (π β π β ((0...π) β {π})) β β’ (π β β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) | ||
Theorem | poimirlem3 37149* | Lemma for poimir 37179 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π β β0) & β’ (π β π < π) & β’ (π β π:(1...π)βΆ(0..^πΎ)) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) β β’ (π β (βπ β (0...π)βπ β (0...π)π = β¦((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β (β¨(π βͺ {β¨(π + 1), 0β©}), (π βͺ {β¨(π + 1), (π + 1)β©})β© β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β§ (βπ β (0...π)βπ β (0...π)π = β¦(((π βͺ {β¨(π + 1), 0β©}) βf + ((((π βͺ {β¨(π + 1), (π + 1)β©}) β (1...π)) Γ {1}) βͺ (((π βͺ {β¨(π + 1), (π + 1)β©}) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((π βͺ {β¨(π + 1), 0β©})β(π + 1)) = 0 β§ ((π βͺ {β¨(π + 1), (π + 1)β©})β(π + 1)) = (π + 1))))) | ||
Theorem | poimirlem4 37150* | Lemma for poimir 37179 connecting the admissible faces on the back face of the (π + 1)-cube to admissible simplices in the π-cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β π β β0) & β’ (π β π < π) β β’ (π β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} β {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))}) | ||
Theorem | poimirlem5 37151* | Lemma for poimir 37179 to establish that, for the simplices defined by a walk along the edges of an π-cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β π β π) & β’ (π β 0 < (2nd βπ)) β β’ (π β (πΉβ0) = (1st β(1st βπ))) | ||
Theorem | poimirlem6 37152* | Lemma for poimir 37179 establishing, for a face of a simplex defined by a walk along the edges of an π-cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β π β π) & β’ (π β (2nd βπ) β (1...(π β 1))) & β’ (π β π β (1...((2nd βπ) β 1))) β β’ (π β (β©π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) = ((2nd β(1st βπ))βπ)) | ||
Theorem | poimirlem7 37153* | Lemma for poimir 37179, similar to poimirlem6 37152, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β π β π) & β’ (π β (2nd βπ) β (1...(π β 1))) & β’ (π β π β ((((2nd βπ) + 1) + 1)...π)) β β’ (π β (β©π β (1...π)((πΉβ(π β 2))βπ) β ((πΉβ(π β 1))βπ)) = ((2nd β(1st βπ))βπ)) | ||
Theorem | poimirlem8 37154* | Lemma for poimir 37179, establishing that away from the opposite vertex the walks in poimirlem9 37155 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β π β π) & β’ (π β (2nd βπ) β (1...(π β 1))) & β’ (π β π β π) β β’ (π β ((2nd β(1st βπ)) βΎ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)})) = ((2nd β(1st βπ)) βΎ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))) | ||
Theorem | poimirlem9 37155* | Lemma for poimir 37179, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β π β π) & β’ (π β (2nd βπ) β (1...(π β 1))) & β’ (π β π β π) & β’ (π β (2nd β(1st βπ)) β (2nd β(1st βπ))) β β’ (π β (2nd β(1st βπ)) = ((2nd β(1st βπ)) β ({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))))) | ||
Theorem | poimirlem10 37156* | Lemma for poimir 37179 establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ (π β (2nd βπ) = 0) β β’ (π β ((πΉβ(π β 1)) βf β ((1...π) Γ {1})) = (1st β(1st βπ))) | ||
Theorem | poimirlem11 37157* | Lemma for poimir 37179 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ (π β (2nd βπ) = 0) & β’ (π β π β π) & β’ (π β (2nd βπ) = 0) & β’ (π β π β (1...π)) β β’ (π β ((2nd β(1st βπ)) β (1...π)) β ((2nd β(1st βπ)) β (1...π))) | ||
Theorem | poimirlem12 37158* | Lemma for poimir 37179 connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ (π β (2nd βπ) = π) & β’ (π β π β π) & β’ (π β (2nd βπ) = π) & β’ (π β π β (0...(π β 1))) β β’ (π β ((2nd β(1st βπ)) β (1...π)) β ((2nd β(1st βπ)) β (1...π))) | ||
Theorem | poimirlem13 37159* | Lemma for poimir 37179- for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) β β’ (π β β*π§ β π (2nd βπ§) = 0) | ||
Theorem | poimirlem14 37160* | Lemma for poimir 37179- for at most one simplex associated with a shared face is the opposite vertex last on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) β β’ (π β β*π§ β π (2nd βπ§) = π) | ||
Theorem | poimirlem15 37161* | Lemma for poimir 37179, that the face in poimirlem22 37168 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ (π β (2nd βπ) β (1...(π β 1))) β β’ (π β β¨β¨(1st β(1st βπ)), ((2nd β(1st βπ)) β ({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))))β©, (2nd βπ)β© β π) | ||
Theorem | poimirlem16 37162* | Lemma for poimir 37179 establishing the vertices of the simplex of poimirlem17 37163. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) & β’ (π β (2nd βπ) = 0) β β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ ((π β (1...π) β¦ (((1st β(1st βπ))βπ) + if(π = ((2nd β(1st βπ))β1), 1, 0))) βf + (((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))))) | ||
Theorem | poimirlem17 37163* | Lemma for poimir 37179 establishing existence for poimirlem18 37164. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) & β’ (π β (2nd βπ) = 0) β β’ (π β βπ§ β π π§ β π) | ||
Theorem | poimirlem18 37164* | Lemma for poimir 37179 stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) & β’ (π β (2nd βπ) = 0) β β’ (π β β!π§ β π π§ β π) | ||
Theorem | poimirlem19 37165* | Lemma for poimir 37179 establishing the vertices of the simplex in poimirlem20 37166. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ (π β (2nd βπ) = π) β β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ ((π β (1...π) β¦ (((1st β(1st βπ))βπ) β if(π = ((2nd β(1st βπ))βπ), 1, 0))) βf + (((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = 1, π, (π β 1)))) β (1...(π¦ + 1))) Γ {1}) βͺ ((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = 1, π, (π β 1)))) β (((π¦ + 1) + 1)...π)) Γ {0}))))) | ||
Theorem | poimirlem20 37166* | Lemma for poimir 37179 establishing existence for poimirlem21 37167. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ (π β (2nd βπ) = π) β β’ (π β βπ§ β π π§ β π) | ||
Theorem | poimirlem21 37167* | Lemma for poimir 37179 stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ (π β (2nd βπ) = π) β β’ (π β β!π§ β π π§ β π) | ||
Theorem | poimirlem22 37168* | Lemma for poimir 37179, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) β β’ (π β β!π§ β π π§ β π) | ||
Theorem | poimirlem23 37169* | Lemma for poimir 37179, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π β π:(1...π)βΆ(0..^πΎ)) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ (π β π β (0...π)) β β’ (π β (βπ β ran (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))(πβπ) β 0 β Β¬ (π = π β§ ((πβπ) = 0 β§ (πβπ) = π)))) | ||
Theorem | poimirlem24 37170* | Lemma for poimir 37179, two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ (π β π:(1...π)βΆ(0..^πΎ)) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ (π β π β (0...π)) β β’ (π β (βπ₯ β (((0...πΎ) βm (1...π)) βm (0...(π β 1)))(π₯ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) β§ ((0...(π β 1)) β ran (π β ran π₯ β¦ π΅) β§ βπ β ran π₯(πβπ) β 0)) β (βπ β (0...(π β 1))βπ β ((0...π) β {π})π = β¦β¨π, πβ© / π β¦πΆ β§ Β¬ (π = π β§ ((πβπ) = 0 β§ (πβπ) = π))))) | ||
Theorem | poimirlem25 37171* | Lemma for poimir 37179 stating that for a given simplex such that no vertex maps to π, the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ (π β π:(1...π)βΆ(0..^πΎ)) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ ((π β§ π β (0...π)) β π β β¦β¨π, πβ© / π β¦πΆ) β β’ (π β 2 β₯ (β―β{π¦ β (0...π) β£ βπ β (0...(π β 1))βπ β ((0...π) β {π¦})π = β¦β¨π, πβ© / π β¦πΆ})) | ||
Theorem | poimirlem26 37172* | Lemma for poimir 37179 showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) β β’ (π β 2 β₯ ((β―β{π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ βπ β (0...(π β 1))βπ β ((0...π) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦πΆ}) β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ}))) | ||
Theorem | poimirlem27 37173* | Lemma for poimir 37179 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ)) β π΅ β (π β 1)) β β’ (π β 2 β₯ ((β―β{π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ βπ β (0...(π β 1))βπ β ((0...π) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦πΆ}) β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (βπ β (0...(π β 1))βπ β (0...(π β 1))π = πΆ β§ ((1st βπ )βπ) = 0 β§ ((2nd βπ )βπ) = π)}))) | ||
Theorem | poimirlem28 37174* | Lemma for poimir 37179, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ)) β π΅ β (π β 1)) & β’ (π β πΎ β β) β β’ (π β βπ β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})βπ β (0...π)βπ β (0...π)π = πΆ) | ||
Theorem | poimirlem29 37175* | Lemma for poimir 37179 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ π = ((πΉβ(((1st β(πΊβπ)) βf + ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf / ((1...π) Γ {π})))βπ) & β’ (π β πΊ:ββΆ((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) & β’ ((π β§ π β β) β ran (1st β(πΊβπ)) β (0..^π)) & β’ ((π β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0ππ) β β’ (π β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ (β Γ β)))(1 / π)) β βπ β (1...π)βπ£ β (π βΎt πΌ)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) | ||
Theorem | poimirlem30 37176* | Lemma for poimir 37179 combining poimirlem29 37175 with bwth 23327. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ π = ((πΉβ(((1st β(πΊβπ)) βf + ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf / ((1...π) Γ {π})))βπ) & β’ (π β πΊ:ββΆ((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) & β’ ((π β§ π β β) β ran (1st β(πΊβπ)) β (0..^π)) & β’ ((π β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0ππ) β β’ (π β βπ β πΌ βπ β (1...π)βπ£ β (π βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) | ||
Theorem | poimirlem31 37177* | Lemma for poimir 37179, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 37176 and poimirlem28 37174. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) & β’ π = ((1st β(πΊβπ)) βf + ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) & β’ (π β πΊ:ββΆ((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) & β’ ((π β§ π β β) β ran (1st β(πΊβπ)) β (0..^π)) & β’ ((π β§ (π β β β§ π β (0...π))) β βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < )) β β’ ((π β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0π((πΉβ(π βf / ((1...π) Γ {π})))βπ)) | ||
Theorem | poimirlem32 37178* | Lemma for poimir 37179, combining poimirlem28 37174, poimirlem30 37176, and poimirlem31 37177 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ ((πΉβπ§)βπ)) β β’ (π β βπ β πΌ βπ β (1...π)βπ£ β (π βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) | ||
Theorem | poimir 37179* | Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ ((πΉβπ§)βπ)) β β’ (π β βπ β πΌ (πΉβπ) = ((1...π) Γ {0})) | ||
Theorem | broucube 37180* | Brouwer - or as Kulpa calls it, "Bohl-Brouwer" - fixed point theorem for the unit cube. Theorem on [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn (π βΎt πΌ))) β β’ (π β βπ β πΌ π = (πΉβπ)) | ||
Theorem | heicant 37181 | Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.) (Proof shortened by AV, 27-Sep-2020.) |
β’ (π β πΆ β (βMetβπ)) & β’ (π β π· β (βMetβπ)) & β’ (π β (MetOpenβπΆ) β Comp) & β’ (π β π β β ) & β’ (π β π β β ) β β’ (π β ((metUnifβπΆ) Cnu(metUnifβπ·)) = ((MetOpenβπΆ) Cn (MetOpenβπ·))) | ||
Theorem | opnmbllem0 37182* | Lemma for ismblfin 37187; could also be used to shorten proof of opnmbllem 25543. (Contributed by Brendan Leahy, 13-Jul-2018.) |
β’ (π΄ β (topGenβran (,)) β βͺ ([,] β {π§ β ran (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β£ ([,]βπ§) β π΄}) = π΄) | ||
Theorem | mblfinlem1 37183* | Lemma for ismblfin 37187, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in π΄. (Contributed by Brendan Leahy, 13-Jul-2018.) |
β’ ((π΄ β (topGenβran (,)) β§ π΄ β β ) β βπ π:ββ1-1-ontoβ{π β {π β ran (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β£ ([,]βπ) β π΄} β£ βπ β {π β ran (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β£ ([,]βπ) β π΄} (([,]βπ) β ([,]βπ) β π = π)}) | ||
Theorem | mblfinlem2 37184* | Lemma for ismblfin 37187, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different definition of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
β’ ((π΄ β (topGenβran (,)) β§ π β β β§ π < (vol*βπ΄)) β βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π < (vol*βπ ))) | ||
Theorem | mblfinlem3 37185* | The difference between two sets measurable by the criterion in ismblfin 37187 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
β’ (((π΄ β β β§ (vol*βπ΄) β β) β§ (π΅ β β β§ (vol*βπ΅) β β) β§ ((vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ) β§ (vol*βπ΅) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΅ β§ π¦ = (volβπ))}, β, < ))) β sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β (π΄ β π΅) β§ π¦ = (volβπ))}, β, < ) = (vol*β(π΄ β π΅))) | ||
Theorem | mblfinlem4 37186* | Backward direction of ismblfin 37187. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
β’ (((π΄ β β β§ (vol*βπ΄) β β) β§ π΄ β dom vol) β (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) | ||
Theorem | ismblfin 37187* | Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.) |
β’ ((π΄ β β β§ (vol*βπ΄) β β) β (π΄ β dom vol β (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ))) | ||
Theorem | ovoliunnfl 37188* | ovoliun 25447 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.) |
β’ ((π Fn β β§ βπ β β ((πβπ) β β β§ (vol*β(πβπ)) β β)) β (vol*ββͺ π β β (πβπ)) β€ sup(ran seq1( + , (π β β β¦ (vol*β(πβπ)))), β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | ex-ovoliunnfl 37189* | Demonstration of ovoliunnfl 37188. (Contributed by Brendan Leahy, 21-Nov-2017.) |
β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | voliunnfl 37190* | voliun 25496 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.) |
β’ π = seq1( + , πΊ) & β’ πΊ = (π β β β¦ (volβ(πβπ))) & β’ ((βπ β β ((πβπ) β dom vol β§ (volβ(πβπ)) β β) β§ Disj π β β (πβπ)) β (volββͺ π β β (πβπ)) = sup(ran π, β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | volsupnfl 37191* | volsup 25498 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.) |
β’ ((π:ββΆdom vol β§ βπ β β (πβπ) β (πβ(π + 1))) β (volββͺ ran π) = sup((vol β ran π), β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | mbfresfi 37192* | Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π β Fin) & β’ (π β βπ β π (πΉ βΎ π ) β MblFn) & β’ (π β βͺ π = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfposadd 37193* | If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018.) |
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) β MblFn) | ||
Theorem | cnambfre 37194 | A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol β§ (vol*β(π΄ β ((β‘(((topGenβran (,)) βΎt π΄) CnP (topGenβran (,))) β E ) β {πΉ}))) = 0) β πΉ β MblFn) | ||
Theorem | dvtanlem 37195 | Lemma for dvtan 37196- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) (Proof shortened by OpenAI, 3-Jul-2020.) |
β’ (β‘cos β (β β {0})) β (TopOpenββfld) | ||
Theorem | dvtan 37196 | Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.) |
β’ (β D tan) = (π₯ β dom tan β¦ ((cosβπ₯)β-2)) | ||
Theorem | itg2addnclem 37197* | An alternate expression for the β«2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(βπ¦ β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π¦))) βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) = sup(πΏ, β*, < )) | ||
Theorem | itg2addnclem2 37198* | Lemma for itg2addnc 37200. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) β β’ (((π β§ β β dom β«1) β§ π£ β β+) β (π₯ β β β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β dom β«1) | ||
Theorem | itg2addnclem3 37199* | Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 37200. (Contributed by Brendan Leahy, 11-Mar-2018.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΊ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΊ) β β) β β’ (π β (ββ β dom β«1(βπ¦ β β+ (π§ β β β¦ if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)) β βπ‘βπ’(βπ β dom β«1βπ β dom β«1((βπ β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)))) | ||
Theorem | itg2addnc 37200 | Alternate proof of itg2add 25702 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 25651, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 10453, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΊ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΊ) β β) β β’ (π β (β«2β(πΉ βf + πΊ)) = ((β«2βπΉ) + (β«2βπΊ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |