Home | Metamath
Proof Explorer Theorem List (p. 307 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xdivcld 30601 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xdivcl 30602 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xdivmul 30603 | Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴)) | ||
Theorem | rexdiv 30604 | The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵)) | ||
Theorem | xdivrec 30605 | Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵))) | ||
Theorem | xdivid 30606 | A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1) | ||
Theorem | xdiv0 30607 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0) | ||
Theorem | xdiv0rp 30608 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0) | ||
Theorem | eliccioo 30609 | Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐵))) | ||
Theorem | elxrge02 30610 | Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 = 0 ∨ 𝐴 ∈ ℝ+ ∨ 𝐴 = +∞)) | ||
Theorem | xdivpnfrp 30611 | Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ ℝ+ → (+∞ /𝑒 𝐴) = +∞) | ||
Theorem | rpxdivcld 30612 | Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ+) | ||
Theorem | xrpxdivcld 30613 | Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | wrdfd 30614 | 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 30615 | 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 30616* | 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 30617 | The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (〈“𝐴𝐵”〉 prefix 1) = 〈“𝐴”〉) | ||
Theorem | pfxrn2 30618 | The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14049. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊) | ||
Theorem | pfxrn3 30619 | Express the range of a prefix of a word. Stronger version of pfxrn2 30618. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿))) | ||
Theorem | pfxf1 30620 | 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 30621 | 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 30622 | Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) ⇒ ⊢ (𝜑 → ran 〈“𝐼𝐽”〉 = {𝐼, 𝐽}) | ||
Theorem | s2f1 30623 | 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 30624 | Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐾 ∈ 𝐷) ⇒ ⊢ (𝜑 → ran 〈“𝐼𝐽𝐾”〉 = {𝐼, 𝐽, 𝐾}) | ||
Theorem | s3f1 30625 | 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 30626 | Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.) |
⊢ 〈“𝐼𝐽𝐾”〉 ∈ (◡♯ “ {3}) | ||
Theorem | ccatf1 30627 | 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 30628 | 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 30629* | Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ++ 〈“𝑖𝑗”〉) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏) | ||
Theorem | swrdrn2 30630 | The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14016. (Contributed by Thierry Arnoux, 12-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) ⊆ ran 𝑊) | ||
Theorem | swrdrn3 30631 | Express the range of a subword. Stronger version of swrdrn2 30630. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr 〈𝑀, 𝑁〉) = (𝑊 “ (𝑀..^𝑁))) | ||
Theorem | swrdf1 30632 | 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 30633 | 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 30634 | Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆))) & ⊢ (𝜑 → 𝑅 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ (0..^((♯‘𝑆) − 𝑇))) & ⊢ (𝜑 → 𝐾 = (𝐹 + (♯‘𝑅))) ⇒ ⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘(𝑋 + 𝐾)) = (𝑆‘(𝑋 + 𝑇))) | ||
Theorem | 1cshid 30635 | Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (♯‘𝑊) = 1) → (𝑊 cyclShift 𝑁) = 𝑊) | ||
Theorem | cshw1s2 30636 | Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (〈“𝐴𝐵”〉 cyclShift 1) = 〈“𝐵𝐴”〉) | ||
Theorem | cshwrnid 30637 | Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊) | ||
Theorem | cshf1o 30638 | 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 30639 | 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 30640 | The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (norm‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻)) | ||
Theorem | abvpropd2 30641 | Weaker version of abvpropd 19615. (Contributed by Thierry Arnoux, 8-Nov-2017.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿)) ⇒ ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿)) | ||
Theorem | oppgle 30642 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ ≤ = (le‘𝑅) ⇒ ⊢ ≤ = (le‘𝑂) | ||
Theorem | oppglt 30643 | less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ < = (lt‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → < = (lt‘𝑂)) | ||
Theorem | ressprs 30644 | The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset ) | ||
Theorem | oduprs 30645 | Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset ) | ||
Theorem | posrasymb 30646 | A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
Theorem | tospos 30647 | A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset) | ||
Theorem | resspos 30648 | The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Poset) | ||
Theorem | resstos 30649 | The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
⊢ ((𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Toset) | ||
Theorem | tleile 30650 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
Theorem | tltnle 30651 | In a Toset, less-than is equivalent to not inverse "less than or equal to" see pltnle 17578. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋)) | ||
Theorem | odutos 30652 | Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset) | ||
Theorem | tlt2 30653 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋)) | ||
Theorem | tlt3 30654 | In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋)) | ||
Theorem | trleile 30655 | In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋)) | ||
Theorem | toslublem 30656* | Lemma for toslub 30657 and xrsclat 30669. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑)))) | ||
Theorem | toslub 30657 | 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 30658* | Lemma for tosglb 30659 and xrsclat 30669. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑)))) | ||
Theorem | tosglb 30659 | Same theorem as toslub 30657, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < )) | ||
Theorem | clatp0cl 30660 | 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 30661 | The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 1 = (1.‘𝑊) ⇒ ⊢ (𝑊 ∈ CLat → 1 ∈ 𝐵) | ||
Axiom | ax-xrssca 30662 | 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 30663 | 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 30664 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12645 and df-xrs 16777), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ 0 = (0g‘ℝ*𝑠) | ||
Theorem | xrslt 30665 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
⊢ < = (lt‘ℝ*𝑠) | ||
Theorem | xrsinvgval 30666 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 12645 and df-xrs 16777), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵) | ||
Theorem | xrsmulgzz 30667 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
Theorem | xrstos 30668 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ Toset | ||
Theorem | xrsclat 30669 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
⊢ ℝ*𝑠 ∈ CLat | ||
Theorem | xrsp0 30670 | 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 30671 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
⊢ +∞ = (1.‘ℝ*𝑠) | ||
Theorem | ressmulgnn 30672 | Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐴 ⊆ (Base‘𝐺) & ⊢ ∗ = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋)) | ||
Theorem | ressmulgnn0 30673 | 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 30674 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge00 30675 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0plusg 30676 | 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 30677 | The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
Theorem | xrge0mulgnn0 30678 | 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 30679 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
Theorem | xrge0addgt0 30680 | The sum of nonnegative and positive numbers is positive. See addgtge0 11130. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵)) | ||
Theorem | xrge0adddir 30681 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
Theorem | xrge0adddi 30682 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵))) | ||
Theorem | xrge0npcan 30683 | Extended nonnegative real version of npcan 10897. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
Theorem | fsumrp0cl 30684* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
Theorem | abliso 30685 | 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 30686 | 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 30687 | 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 30688* | 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 (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))))) | ||
Theorem | gsummpt2d 30689* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19094. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝑥 = 〈𝑦, 𝑧〉 → 𝐶 = 𝐷) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) | ||
Theorem | lmodvslmhm 30690* | Scalar multiplication in a left module by a fixed element is a group homomorphism. (Contributed by Thierry Arnoux, 12-Jun-2023.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐾 ↦ (𝑥 · 𝑌)) ∈ (𝐹 GrpHom 𝑊)) | ||
Theorem | gsumvsmul1 30691* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 19358, since every ring is a left module over itself. (Contributed by Thierry Arnoux, 12-Jun-2023.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LMod) & ⊢ (𝜑 → 𝑆 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑆 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌)) | ||
Theorem | gsummptres 30692* | Extend a finite group sum by padding outside with zeroes. Proof generated using OpenAI's proof assistant. (Contributed by Thierry Arnoux, 11-Jul-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐷)) → 𝐶 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑥 ∈ (𝐴 ∩ 𝐷) ↦ 𝐶))) | ||
Theorem | gsumzresunsn 30693 | Append an element to a finite group sum expressed as a function restriction. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (𝐹‘𝑋) & ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝐹 “ (𝐴 ∪ {𝑋})) ⊆ (𝑍‘(𝐹 “ (𝐴 ∪ {𝑋})))) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ∪ {𝑋}))) = ((𝐺 Σg (𝐹 ↾ 𝐴)) + 𝑌)) | ||
Theorem | xrge0tsmsd 30694* | Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 30-Jan-2017.) |
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) & ⊢ (𝜑 → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < )) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆}) | ||
Theorem | xrge0tsmsbi 30695 | Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 23-Jun-2017.) |
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐺 tsums 𝐹) ↔ 𝐶 = ∪ (𝐺 tsums 𝐹))) | ||
Theorem | xrge0tsmseq 30696 | Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → 𝐶 = ∪ (𝐺 tsums 𝐹)) | ||
Theorem | cntzun 30697 | The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑍‘(𝑋 ∪ 𝑌)) = ((𝑍‘𝑋) ∩ (𝑍‘𝑌))) | ||
Theorem | cntzsnid 30698 | The centralizer of the identity element is the whole base set. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → (𝑍‘{ 0 }) = 𝐵) | ||
Theorem | cntrcrng 30699 | The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝑍 = (𝑅 ↾s (Cntr‘(mulGrp‘𝑅))) ⇒ ⊢ (𝑅 ∈ Ring → 𝑍 ∈ CRing) | ||
Syntax | comnd 30700 | Extend class notation with the class of all right ordered monoids. |
class oMnd |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |