![]() |
Metamath
Proof Explorer Theorem List (p. 330 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrpxdivcld 32901 | Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | wrdfd 32902 | 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 32903 | 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 32904* | 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 | wrdfsupp 32905 | A word has finite support. (Contributed by Thierry Arnoux, 27-May-2025.) |
⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) ⇒ ⊢ (𝜑 → 𝑊 finSupp 𝑍) | ||
Theorem | wrdpmcl 32906 | Closure of a word with permuted symbols. (Contributed by Thierry Arnoux, 27-May-2025.) |
⊢ 𝐽 = (0..^(♯‘𝑊)) & ⊢ (𝜑 → 𝐸:𝐽–1-1-onto→𝐽) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) ⇒ ⊢ (𝜑 → (𝑊 ∘ 𝐸) ∈ Word 𝑆) | ||
Theorem | pfx1s2 32907 | The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (〈“𝐴𝐵”〉 prefix 1) = 〈“𝐴”〉) | ||
Theorem | pfxrn2 32908 | The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14719. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊) | ||
Theorem | pfxrn3 32909 | Express the range of a prefix of a word. Stronger version of pfxrn2 32908. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿))) | ||
Theorem | pfxf1 32910 | 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 32911 | Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023.) |
⊢ (𝜑 → 𝐼 ∈ 𝐷) ⇒ ⊢ (𝜑 → 〈“𝐼”〉:dom 〈“𝐼”〉–1-1→𝐷) | ||
Theorem | s2rnOLD 32912 | Obsolete version of s2rn 14998 as of 1-Aug-2025. Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) ⇒ ⊢ (𝜑 → ran 〈“𝐼𝐽”〉 = {𝐼, 𝐽}) | ||
Theorem | s2f1 32913 | Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) ⇒ ⊢ (𝜑 → 〈“𝐼𝐽”〉:dom 〈“𝐼𝐽”〉–1-1→𝐷) | ||
Theorem | s3rnOLD 32914 | Obsolete version of s2rn 14998 as of 1-Aug-2025. Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐾 ∈ 𝐷) ⇒ ⊢ (𝜑 → ran 〈“𝐼𝐽𝐾”〉 = {𝐼, 𝐽, 𝐾}) | ||
Theorem | s3f1 32915 | 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 32916 | Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.) |
⊢ 〈“𝐼𝐽𝐾”〉 ∈ (◡♯ “ {3}) | ||
Theorem | ccatf1 32917 | 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 | ccatdmss 32918 | The domain of a concatenated word is a superset of the domain of the first word. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝜑 → 𝐴 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐵 ∈ Word 𝑆) ⇒ ⊢ (𝜑 → dom 𝐴 ⊆ dom (𝐴 ++ 𝐵)) | ||
Theorem | pfxlsw2ccat 32919 | 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 | ccatws1f1o 32920 | Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025.) |
⊢ 𝑁 = (♯‘𝑇) & ⊢ 𝐽 = (0..^(𝑁 + 1)) & ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁)) ⇒ ⊢ (𝜑 → (𝑇 ++ 〈“𝑁”〉):𝐽–1-1-onto→𝐽) | ||
Theorem | ccatws1f1olast 32921 | Two ways to reorder symbols in a word 𝑊 according to permutation 𝑇, and add a last symbol 𝑋. (Contributed by Thierry Arnoux, 27-May-2025.) |
⊢ 𝑁 = (♯‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁)) ⇒ ⊢ (𝜑 → ((𝑊 ++ 〈“𝑋”〉) ∘ (𝑇 ++ 〈“𝑁”〉)) = ((𝑊 ∘ 𝑇) ++ 〈“𝑋”〉)) | ||
Theorem | wrdt2ind 32922* | Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ++ 〈“𝑖𝑗”〉) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏) | ||
Theorem | swrdrn2 32923 | The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14686. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ ran 𝑊) | ||
Theorem | swrdrn3 32924 | Express the range of a subword. Stronger version of swrdrn2 32923. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) = (𝑊 “ (𝑀..^𝑁))) | ||
Theorem | swrdf1 32925 | 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 32926 | 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 32927 | Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆))) & ⊢ (𝜑 → 𝑅 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ (0..^((♯‘𝑆) − 𝑇))) & ⊢ (𝜑 → 𝐾 = (𝐹 + (♯‘𝑅))) ⇒ ⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘(𝑋 + 𝐾)) = (𝑆‘(𝑋 + 𝑇))) | ||
Theorem | 1cshid 32928 | Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (♯‘𝑊) = 1) → (𝑊 cyclShift 𝑁) = 𝑊) | ||
Theorem | cshw1s2 32929 | Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (〈“𝐴𝐵”〉 cyclShift 1) = 〈“𝐵𝐴”〉) | ||
Theorem | cshwrnid 32930 | Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊) | ||
Theorem | cshf1o 32931 | 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 32932 | 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 32933 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻)) | ||
Theorem | abvpropd2 32934 | Weaker version of abvpropd 20852. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿)) ⇒ ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿)) | ||
Theorem | oppgle 32935 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ ≤ = (le‘𝑅) ⇒ ⊢ ≤ = (le‘𝑂) | ||
Theorem | oppgleOLD 32936 | Obsolete version of oppgle 32935 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 32937 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ < = (lt‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → < = (lt‘𝑂)) | ||
Theorem | ressprs 32938 | The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset ) | ||
Theorem | posrasymb 32939 | A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
Theorem | resspos 32940 | The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Poset) | ||
Theorem | resstos 32941 | The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ ((𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Toset) | ||
Theorem | odutos 32942 | Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset) | ||
Theorem | tlt2 32943 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋)) | ||
Theorem | tlt3 32944 | In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋)) | ||
Theorem | trleile 32945 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
Theorem | toslublem 32946* | Lemma for toslub 32947 and xrsclat 32995. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑)))) | ||
Theorem | toslub 32947 | 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 32948* | Lemma for tosglb 32949 and xrsclat 32995. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑)))) | ||
Theorem | tosglb 32949 | Same theorem as toslub 32947, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < )) | ||
Theorem | clatp0cl 32950 | 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 32951 | 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 32952 | Extend class notation with monotone functions. |
class Monot | ||
Syntax | cmgc 32953 | Extend class notation with the monotone Galois connection. |
class MGalConn | ||
Definition | df-mnt 32954* | 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 32955* | Define monotone Galois connections. See mgcval 32961 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.) |
⊢ MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))}) | ||
Theorem | mntoval 32956* | Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉Monot𝑊) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝑓‘𝑥) ≲ (𝑓‘𝑦))}) | ||
Theorem | ismnt 32957* | Express the statement "𝐹 is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 ∈ (𝑉Monot𝑊) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))))) | ||
Theorem | ismntd 32958 | Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ 𝐶) & ⊢ (𝜑 → 𝑊 ∈ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌)) | ||
Theorem | mntf 32959 | A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ (𝑉Monot𝑊)) → 𝐹:𝐴⟶𝐵) | ||
Theorem | mgcoval 32960* | Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉MGalConn𝑊) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))}) | ||
Theorem | mgcval 32961* |
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 32962 | 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 32963 | 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 32964 | An inequality for the kernel operator 𝐺 ∘ 𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑋))) | ||
Theorem | mgccole2 32965 | 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 32966 | 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 32967 | 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 32968* | 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 32969* | Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦))) & ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥))) & ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢) ⇒ ⊢ (𝜑 → 𝐹𝐻𝐺) | ||
Theorem | dfmgc2 32970* | Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.) |
⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) ⇒ ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥))))))) | ||
Theorem | mgcmnt1d 32971 | Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹𝐻𝐺) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊)) | ||
Theorem | mgcmnt2d 32972 | Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.) |
⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ (𝜑 → 𝑉 ∈ Proset ) & ⊢ (𝜑 → 𝑊 ∈ Proset ) & ⊢ (𝜑 → 𝐹𝐻𝐺) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉)) | ||
Theorem | mgccnv 32973 | 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 32974* | 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 32975 | Property of a Galois connection, lemma for mgcf1o 32977. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋)) | ||
Theorem | mgcf1olem2 32976 | Property of a Galois connection, lemma for mgcf1o 32977. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌)) | ||
Theorem | mgcf1o 32977 | 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 𝐹)) | ||
Syntax | cchn 32978 | Extend class notation with the class of (finite) chains. |
class ( < Chain𝐴) | ||
Definition | df-chn 32979* | Define the class of (finite) chains. A chain is defined to be a sequence of objects, where each object is less than the next one in the sequence. The term "chain" is usually used in order theory. In the context of algebra, chains are often called "towers", for example for fields, or "series", for example for subgroup or subnormal series. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)} | ||
Theorem | ischn 32980* | Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛))) | ||
Theorem | chnwrd 32981 | A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Word 𝐴) | ||
Theorem | chnltm1 32982 | Basic property of a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝑁 ∈ (dom 𝐶 ∖ {0})) ⇒ ⊢ (𝜑 → (𝐶‘(𝑁 − 1)) < (𝐶‘𝑁)) | ||
Theorem | pfxchn 32983 | A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝐶))) ⇒ ⊢ (𝜑 → (𝐶 prefix 𝐿) ∈ ( < Chain𝐴)) | ||
Theorem | chnind 32984* | Induction over a chain. See nnind 12281 for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃)) & ⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (𝜓 ↔ 𝜏)) & ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝜒) & ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | chnub 32985 | In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝜑 → < Po 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1))) ⇒ ⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶)) | ||
Theorem | chnlt 32986 | Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (𝜑 → < Po 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶))) & ⊢ (𝜑 → 𝐼 ∈ (0..^𝐽)) ⇒ ⊢ (𝜑 → (𝐶‘𝐼) < (𝐶‘𝐽)) | ||
Theorem | chnso 32987 | A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → < Or ran 𝐶) | ||
Axiom | ax-xrssca 32988 | 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 32989 | 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 32990 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13287 and df-xrs 17548), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ 0 = (0g‘ℝ*𝑠) | ||
Theorem | xrslt 32991 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ < = (lt‘ℝ*𝑠) | ||
Theorem | xrsinvgval 32992 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13287 and df-xrs 17548), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵) | ||
Theorem | xrsmulgzz 32993 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
Theorem | xrstos 32994 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ Toset | ||
Theorem | xrsclat 32995 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ CLat | ||
Theorem | xrsp0 32996 | 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 32997 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
⊢ +∞ = (1.‘ℝ*𝑠) | ||
Theorem | xrge0base 32998 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge00 32999 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0plusg 33000 | 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[,]+∞))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |