![]() |
Metamath
Proof Explorer Theorem List (p. 322 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrpxdivcld 32101 | Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β β+) β β’ (π β (π΄ /π π΅) β (0[,]+β)) | ||
Theorem | wrdfd 32102 | A word is a zero-based sequence with a recoverable upper limit, deduction version. (Contributed by Thierry Arnoux, 22-Dec-2021.) |
β’ (π β π = (β―βπ)) & β’ (π β π β Word π) β β’ (π β π:(0..^π)βΆπ) | ||
Theorem | wrdres 32103 | Condition for the restriction of a word to be a word itself. (Contributed by Thierry Arnoux, 5-Oct-2018.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β (π βΎ (0..^π)) β Word π) | ||
Theorem | wrdsplex 32104* | Existence of a split of a word at a given index. (Contributed by Thierry Arnoux, 11-Oct-2018.) (Proof shortened by AV, 3-Nov-2022.) |
β’ ((π β Word π β§ π β (0...(β―βπ))) β βπ£ β Word ππ = ((π βΎ (0..^π)) ++ π£)) | ||
Theorem | pfx1s2 32105 | The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (β¨βπ΄π΅ββ© prefix 1) = β¨βπ΄ββ©) | ||
Theorem | pfxrn2 32106 | The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14635. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ran (π prefix πΏ) β ran π) | ||
Theorem | pfxrn3 32107 | Express the range of a prefix of a word. Stronger version of pfxrn2 32106. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ran (π prefix πΏ) = (π β (0..^πΏ))) | ||
Theorem | pfxf1 32108 | Condition for a prefix to be injective. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
β’ (π β π β Word π) & β’ (π β π:dom πβ1-1βπ) & β’ (π β πΏ β (0...(β―βπ))) β β’ (π β (π prefix πΏ):dom (π prefix πΏ)β1-1βπ) | ||
Theorem | s1f1 32109 | Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023.) |
β’ (π β πΌ β π·) β β’ (π β β¨βπΌββ©:dom β¨βπΌββ©β1-1βπ·) | ||
Theorem | s2rn 32110 | Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ (π β πΌ β π·) & β’ (π β π½ β π·) β β’ (π β ran β¨βπΌπ½ββ© = {πΌ, π½}) | ||
Theorem | s2f1 32111 | Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) β β’ (π β β¨βπΌπ½ββ©:dom β¨βπΌπ½ββ©β1-1βπ·) | ||
Theorem | s3rn 32112 | Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) β β’ (π β ran β¨βπΌπ½πΎββ© = {πΌ, π½, πΎ}) | ||
Theorem | s3f1 32113 | Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β β¨βπΌπ½πΎββ©:dom β¨βπΌπ½πΎββ©β1-1βπ·) | ||
Theorem | s3clhash 32114 | Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.) |
β’ β¨βπΌπ½πΎββ© β (β‘β― β {3}) | ||
Theorem | ccatf1 32115 | Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023.) |
β’ (π β π β π) & β’ (π β π΄ β Word π) & β’ (π β π΅ β Word π) & β’ (π β π΄:dom π΄β1-1βπ) & β’ (π β π΅:dom π΅β1-1βπ) & β’ (π β (ran π΄ β© ran π΅) = β ) β β’ (π β (π΄ ++ π΅):dom (π΄ ++ π΅)β1-1βπ) | ||
Theorem | pfxlsw2ccat 32116 | Reconstruct a word from its prefix and its last two symbols. (Contributed by Thierry Arnoux, 26-Sep-2023.) |
β’ π = (β―βπ) β β’ ((π β Word π β§ 2 β€ π) β π = ((π prefix (π β 2)) ++ β¨β(πβ(π β 2))(πβ(π β 1))ββ©)) | ||
Theorem | wrdt2ind 32117* | Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ ++ β¨βππββ©) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ ((π¦ β Word π΅ β§ π β π΅ β§ π β π΅) β (π β π)) β β’ ((π΄ β Word π΅ β§ 2 β₯ (β―βπ΄)) β π) | ||
Theorem | swrdrn2 32118 | The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14602. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
β’ ((π β Word π β§ π β (0...π) β§ π β (0...(β―βπ))) β ran (π substr β¨π, πβ©) β ran π) | ||
Theorem | swrdrn3 32119 | Express the range of a subword. Stronger version of swrdrn2 32118. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
β’ ((π β Word π β§ π β (0...π) β§ π β (0...(β―βπ))) β ran (π substr β¨π, πβ©) = (π β (π..^π))) | ||
Theorem | swrdf1 32120 | Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
β’ (π β π β Word π·) & β’ (π β π β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π:dom πβ1-1βπ·) β β’ (π β (π substr β¨π, πβ©):dom (π substr β¨π, πβ©)β1-1βπ·) | ||
Theorem | swrdrndisj 32121 | Condition for the range of two subwords of an injective word to be disjoint. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
β’ (π β π β Word π·) & β’ (π β π β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β π β (π...π)) & β’ (π β π β (π...(β―βπ))) β β’ (π β (ran (π substr β¨π, πβ©) β© ran (π substr β¨π, πβ©)) = β ) | ||
Theorem | splfv3 32122 | Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
β’ (π β π β Word π΄) & β’ (π β πΉ β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π β Word π΄) & β’ (π β π β (0..^((β―βπ) β π))) & β’ (π β πΎ = (πΉ + (β―βπ ))) β β’ (π β ((π splice β¨πΉ, π, π β©)β(π + πΎ)) = (πβ(π + π))) | ||
Theorem | 1cshid 32123 | Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
β’ ((π β Word π β§ π β β€ β§ (β―βπ) = 1) β (π cyclShift π) = π) | ||
Theorem | cshw1s2 32124 | Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (β¨βπ΄π΅ββ© cyclShift 1) = β¨βπ΅π΄ββ©) | ||
Theorem | cshwrnid 32125 | Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ ((π β Word π β§ π β β€) β ran (π cyclShift π) = ran π) | ||
Theorem | cshf1o 32126 | Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023.) |
β’ ((π β Word π· β§ π:dom πβ1-1βπ· β§ π β β€) β (π cyclShift π):dom πβ1-1-ontoβran π) | ||
Theorem | ressplusf 32127 | The group operation function +π of a structure's restriction is the operation function's restriction to the new base. (Contributed by Thierry Arnoux, 26-Mar-2017.) |
β’ π΅ = (BaseβπΊ) & β’ π» = (πΊ βΎs π΄) & ⒠⨣ = (+gβπΊ) & ⒠⨣ Fn (π΅ Γ π΅) & β’ π΄ β π΅ β β’ (+πβπ») = ( ⨣ βΎ (π΄ Γ π΄)) | ||
Theorem | ressnm 32128 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
β’ π» = (πΊ βΎs π΄) & β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (normβπΊ) β β’ ((πΊ β Mnd β§ 0 β π΄ β§ π΄ β π΅) β (π βΎ π΄) = (normβπ»)) | ||
Theorem | abvpropd2 32129 | Weaker version of abvpropd 20450. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (+gβπΎ) = (+gβπΏ)) & β’ (π β (.rβπΎ) = (.rβπΏ)) β β’ (π β (AbsValβπΎ) = (AbsValβπΏ)) | ||
Theorem | oppgle 32130 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π = (oppgβπ ) & β’ β€ = (leβπ ) β β’ β€ = (leβπ) | ||
Theorem | oppgleOLD 32131 | Obsolete version of oppgle 32130 as of 27-Oct-2024. less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (oppgβπ ) & β’ β€ = (leβπ ) β β’ β€ = (leβπ) | ||
Theorem | oppglt 32132 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π = (oppgβπ ) & β’ < = (ltβπ ) β β’ (π β π β < = (ltβπ)) | ||
Theorem | ressprs 32133 | The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
β’ π΅ = (BaseβπΎ) β β’ ((πΎ β Proset β§ π΄ β π΅) β (πΎ βΎs π΄) β Proset ) | ||
Theorem | oduprs 32134 | Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π· = (ODualβπΎ) β β’ (πΎ β Proset β π· β Proset ) | ||
Theorem | posrasymb 32135 | A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β π = π)) | ||
Theorem | resspos 32136 | The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ ((πΉ β Poset β§ π΄ β π) β (πΉ βΎs π΄) β Poset) | ||
Theorem | resstos 32137 | The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ ((πΉ β Toset β§ π΄ β π) β (πΉ βΎs π΄) β Toset) | ||
Theorem | odutos 32138 | Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
β’ π· = (ODualβπΎ) β β’ (πΎ β Toset β π· β Toset) | ||
Theorem | tlt2 32139 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β€ π β¨ π < π)) | ||
Theorem | tlt3 32140 | In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π = π β¨ π < π β¨ π < π)) | ||
Theorem | trleile 32141 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = ((leβπΎ) β© (π΅ Γ π΅)) β β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β€ π β¨ π β€ π)) | ||
Theorem | toslublem 32142* | Lemma for toslub 32143 and xrsclat 32181. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ (π β πΎ β Toset) & β’ (π β π΄ β π΅) & β’ β€ = (leβπΎ) β β’ ((π β§ π β π΅) β ((βπ β π΄ π β€ π β§ βπ β π΅ (βπ β π΄ π β€ π β π β€ π)) β (βπ β π΄ Β¬ π < π β§ βπ β π΅ (π < π β βπ β π΄ π < π)))) | ||
Theorem | toslub 32143 | In a toset, the lowest upper bound lub, defined for partial orders is the supremum, sup(π΄, π΅, < ), defined for total orders. (these are the set.mm definitions: lowest upper bound and supremum are normally synonymous). Note that those two values are also equal if such a supremum does not exist: in that case, both are equal to the empty set. (Contributed by Thierry Arnoux, 15-Feb-2018.) (Revised by Thierry Arnoux, 24-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ (π β πΎ β Toset) & β’ (π β π΄ β π΅) β β’ (π β ((lubβπΎ)βπ΄) = sup(π΄, π΅, < )) | ||
Theorem | tosglblem 32144* | Lemma for tosglb 32145 and xrsclat 32181. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ (π β πΎ β Toset) & β’ (π β π΄ β π΅) & β’ β€ = (leβπΎ) β β’ ((π β§ π β π΅) β ((βπ β π΄ π β€ π β§ βπ β π΅ (βπ β π΄ π β€ π β π β€ π)) β (βπ β π΄ Β¬ πβ‘ < π β§ βπ β π΅ (πβ‘ < π β βπ β π΄ πβ‘ < π)))) | ||
Theorem | tosglb 32145 | Same theorem as toslub 32143, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ (π β πΎ β Toset) & β’ (π β π΄ β π΅) β β’ (π β ((glbβπΎ)βπ΄) = inf(π΄, π΅, < )) | ||
Theorem | clatp0cl 32146 | The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0.βπ) β β’ (π β CLat β 0 β π΅) | ||
Theorem | clatp1cl 32147 | The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
β’ π΅ = (Baseβπ) & β’ 1 = (1.βπ) β β’ (π β CLat β 1 β π΅) | ||
Syntax | cmnt 32148 | Extend class notation with monotone functions. |
class Monot | ||
Syntax | cmgc 32149 | Extend class notation with the monotone Galois connection. |
class MGalConn | ||
Definition | df-mnt 32150* | Define a monotone function between two ordered sets. (Contributed by Thierry Arnoux, 20-Apr-2024.) |
β’ Monot = (π£ β V, π€ β V β¦ β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))}) | ||
Definition | df-mgc 32151* | Define monotone Galois connections. See mgcval 32157 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.) |
β’ MGalConn = (π£ β V, π€ β V β¦ β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))}) | ||
Theorem | mntoval 32152* | Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) β β’ ((π β π β§ π β π) β (πMonotπ) = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πβπ₯) β² (πβπ¦))}) | ||
Theorem | ismnt 32153* | Express the statement "πΉ is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) β β’ ((π β π β§ π β π) β (πΉ β (πMonotπ) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))))) | ||
Theorem | ismntd 32154 | Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β πΆ) & β’ (π β π β π·) & β’ (π β πΉ β (πMonotπ)) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β€ π) β β’ (π β (πΉβπ) β² (πΉβπ)) | ||
Theorem | mntf 32155 | A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) β β’ ((π β π β§ π β π β§ πΉ β (πMonotπ)) β πΉ:π΄βΆπ΅) | ||
Theorem | mgcoval 32156* | Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) β β’ ((π β π β§ π β π) β (πMGalConnπ) = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) | ||
Theorem | mgcval 32157* |
Monotone Galois connection between two functions πΉ and πΊ. If
this relation is satisfied, πΉ is called the lower adjoint of πΊ,
and πΊ is called the upper adjoint of πΉ.
Technically, this is implemented as an operation taking a pair of structures π and π, expected to be posets, which gives a relation between pairs of functions πΉ and πΊ. If such a relation exists, it can be proven to be unique. Galois connections generalize the fundamental theorem of Galois theory about the correspondence between subgroups and subfields. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) β β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ βπ₯ β π΄ βπ¦ β π΅ ((πΉβπ₯) β² π¦ β π₯ β€ (πΊβπ¦))))) | ||
Theorem | mgcf1 32158 | The lower adjoint πΉ of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΉ:π΄βΆπ΅) | ||
Theorem | mgcf2 32159 | The upper adjoint πΊ of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΊ:π΅βΆπ΄) | ||
Theorem | mgccole1 32160 | An inequality for the kernel operator πΊ β πΉ. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΄) β β’ (π β π β€ (πΊβ(πΉβπ))) | ||
Theorem | mgccole2 32161 | Inequality for the closure operator (πΉ β πΊ) of the Galois connection π». (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΅) β β’ (π β (πΉβ(πΊβπ)) β² π) | ||
Theorem | mgcmnt1 32162 | The lower adjoint πΉ of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β€ π) β β’ (π β (πΉβπ) β² (πΉβπ)) | ||
Theorem | mgcmnt2 32163 | The upper adjoint πΊ of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β² π) β β’ (π β (πΊβπ) β€ (πΊβπ)) | ||
Theorem | mgcmntco 32164* | A Galois connection like statement, for two functions with same range. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) & β’ πΆ = (Baseβπ) & β’ < = (leβπ) & β’ (π β π β Proset ) & β’ (π β πΎ β (πMonotπ)) & β’ (π β πΏ β (πMonotπ)) β β’ (π β (βπ₯ β π΄ (πΎβπ₯) < (πΏβ(πΉβπ₯)) β βπ¦ β π΅ (πΎβ(πΊβπ¦)) < (πΏβπ¦))) | ||
Theorem | dfmgc2lem 32165* | Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΅βΆπ΄) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦))) & β’ (π β βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) & β’ ((π β§ π₯ β π΄) β π₯ β€ (πΊβ(πΉβπ₯))) & β’ ((π β§ π’ β π΅) β (πΉβ(πΊβπ’)) β² π’) β β’ (π β πΉπ»πΊ) | ||
Theorem | dfmgc2 32166* | Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) β β’ (π β (πΉπ»πΊ β ((πΉ:π΄βΆπ΅ β§ πΊ:π΅βΆπ΄) β§ ((βπ₯ β π΄ βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ₯) β² (πΉβπ¦)) β§ βπ’ β π΅ βπ£ β π΅ (π’ β² π£ β (πΊβπ’) β€ (πΊβπ£))) β§ (βπ’ β π΅ (πΉβ(πΊβπ’)) β² π’ β§ βπ₯ β π΄ π₯ β€ (πΊβ(πΉβπ₯))))))) | ||
Theorem | mgcmnt1d 32167 | Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΉ β (πMonotπ)) | ||
Theorem | mgcmnt2d 32168 | Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ (π β π β Proset ) & β’ (π β π β Proset ) & β’ (π β πΉπ»πΊ) β β’ (π β πΊ β (πMonotπ)) | ||
Theorem | mgccnv 32169 | The inverse Galois connection is the Galois connection of the dual orders. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ π» = (πMGalConnπ) & β’ π = ((ODualβπ)MGalConn(ODualβπ)) β β’ ((π β Proset β§ π β Proset ) β (πΉπ»πΊ β πΊππΉ)) | ||
Theorem | pwrssmgc 32170* | Given a function πΉ, exhibit a Galois connection between subsets of its domain and subsets of its range. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
β’ πΊ = (π β π« π β¦ (β‘πΉ β π)) & β’ π» = (π β π« π β¦ {π¦ β π β£ (β‘πΉ β {π¦}) β π}) & β’ π = (toIncβπ« π) & β’ π = (toIncβπ« π) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ (π β πΉ:πβΆπ) β β’ (π β πΊ(πMGalConnπ)π») | ||
Theorem | mgcf1olem1 32171 | Property of a Galois connection, lemma for mgcf1o 32173. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β Poset) & β’ (π β π β Poset) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΄) β β’ (π β (πΉβ(πΊβ(πΉβπ))) = (πΉβπ)) | ||
Theorem | mgcf1olem2 32172 | Property of a Galois connection, lemma for mgcf1o 32173. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β Poset) & β’ (π β π β Poset) & β’ (π β πΉπ»πΊ) & β’ (π β π β π΅) β β’ (π β (πΊβ(πΉβ(πΊβπ))) = (πΊβπ)) | ||
Theorem | mgcf1o 32173 | Given a Galois connection, exhibit an order isomorphism. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
β’ π» = (πMGalConnπ) & β’ π΄ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ β² = (leβπ) & β’ (π β π β Poset) & β’ (π β π β Poset) & β’ (π β πΉπ»πΊ) β β’ (π β (πΉ βΎ ran πΊ) Isom β€ , β² (ran πΊ, ran πΉ)) | ||
Axiom | ax-xrssca 32174 | Assume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
β’ βfld = (Scalarββ*π ) | ||
Axiom | ax-xrsvsca 32175 | Assume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
β’ Β·e = ( Β·π ββ*π ) | ||
Theorem | xrs0 32176 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13228 and df-xrs 17448), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ 0 = (0gββ*π ) | ||
Theorem | xrslt 32177 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ < = (ltββ*π ) | ||
Theorem | xrsinvgval 32178 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13228 and df-xrs 17448), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ (π΅ β β* β ((invgββ*π )βπ΅) = -ππ΅) | ||
Theorem | xrsmulgzz 32179 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
β’ ((π΄ β β€ β§ π΅ β β*) β (π΄(.gββ*π )π΅) = (π΄ Β·e π΅)) | ||
Theorem | xrstos 32180 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
β’ β*π β Toset | ||
Theorem | xrsclat 32181 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
β’ β*π β CLat | ||
Theorem | xrsp0 32182 | The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Proof shortened by AV, 28-Sep-2020.) |
β’ -β = (0.ββ*π ) | ||
Theorem | xrsp1 32183 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
β’ +β = (1.ββ*π ) | ||
Theorem | ressmulgnn 32184 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.) |
β’ π» = (πΊ βΎs π΄) & β’ π΄ β (BaseβπΊ) & β’ β = (.gβπΊ) & β’ πΌ = (invgβπΊ) β β’ ((π β β β§ π β π΄) β (π(.gβπ»)π) = (π β π)) | ||
Theorem | ressmulgnn0 32185 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
β’ π» = (πΊ βΎs π΄) & β’ π΄ β (BaseβπΊ) & β’ β = (.gβπΊ) & β’ πΌ = (invgβπΊ) & β’ (0gβπΊ) = (0gβπ») β β’ ((π β β0 β§ π β π΄) β (π(.gβπ»)π) = (π β π)) | ||
Theorem | xrge0base 32186 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ (0[,]+β) = (Baseβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge00 32187 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ 0 = (0gβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge0plusg 32188 | The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017.) |
β’ +π = (+gβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge0le 32189 | The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
β’ β€ = (leβ(β*π βΎs (0[,]+β))) | ||
Theorem | xrge0mulgnn0 32190 | The group multiple function in the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
β’ ((π΄ β β0 β§ π΅ β (0[,]+β)) β (π΄(.gβ(β*π βΎs (0[,]+β)))π΅) = (π΄ Β·e π΅)) | ||
Theorem | xrge0addass 32191 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β ((π΄ +π π΅) +π πΆ) = (π΄ +π (π΅ +π πΆ))) | ||
Theorem | xrge0addgt0 32192 | The sum of nonnegative and positive numbers is positive. See addgtge0 11702. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
β’ (((π΄ β (0[,]+β) β§ π΅ β (0[,]+β)) β§ 0 < π΄) β 0 < (π΄ +π π΅)) | ||
Theorem | xrge0adddir 32193 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β ((π΄ +π π΅) Β·e πΆ) = ((π΄ Β·e πΆ) +π (π΅ Β·e πΆ))) | ||
Theorem | xrge0adddi 32194 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ πΆ β (0[,]+β)) β (πΆ Β·e (π΄ +π π΅)) = ((πΆ Β·e π΄) +π (πΆ Β·e π΅))) | ||
Theorem | xrge0npcan 32195 | Extended nonnegative real version of npcan 11469. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β) β§ π΅ β€ π΄) β ((π΄ +π -ππ΅) +π π΅) = π΄) | ||
Theorem | fsumrp0cl 32196* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β Ξ£π β π΄ π΅ β (0[,)+β)) | ||
Theorem | abliso 32197 | The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
β’ ((π β Abel β§ πΉ β (π GrpIso π)) β π β Abel) | ||
Theorem | gsumsubg 32198 | The group sum in a subgroup is the same as the group sum. (Contributed by Thierry Arnoux, 28-May-2023.) |
β’ π» = (πΊ βΎs π΅) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΅ β (SubGrpβπΊ)) β β’ (π β (πΊ Ξ£g πΉ) = (π» Ξ£g πΉ)) | ||
Theorem | gsumsra 32199 | The group sum in a subring algebra is the same as the ring's group sum. (Contributed by Thierry Arnoux, 28-May-2023.) |
β’ π΄ = ((subringAlg βπ )βπ΅) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β (Baseβπ )) β β’ (π β (π Ξ£g πΉ) = (π΄ Ξ£g πΉ)) | ||
Theorem | gsummpt2co 32200* | Split a finite sum into a sum of a collection of sums over disjoint subsets. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ (π β π β CMnd) & β’ (π β π΄ β Fin) & β’ (π β πΈ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ ((π β§ π₯ β π΄) β π· β πΈ) & β’ πΉ = (π₯ β π΄ β¦ π·) β β’ (π β (π Ξ£g (π₯ β π΄ β¦ πΆ)) = (π Ξ£g (π¦ β πΈ β¦ (π Ξ£g (π₯ β (β‘πΉ β {π¦}) β¦ πΆ))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |