| Metamath
Proof Explorer Theorem List (p. 186 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | latnlej 18501 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍)) | ||
| Theorem | latnlej1l 18502 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑌) | ||
| Theorem | latnlej1r 18503 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑍) | ||
| Theorem | latnlej2 18504 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 10-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (¬ 𝑋 ≤ 𝑌 ∧ ¬ 𝑋 ≤ 𝑍)) | ||
| Theorem | latnlej2l 18505 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑌) | ||
| Theorem | latnlej2r 18506 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑍) | ||
| Theorem | latjidm 18507 | Lattice join is idempotent. Analogue of unidm 4157. (Contributed by NM, 8-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋) | ||
| Theorem | latmcom 18508 | The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) | ||
| Theorem | latmle1 18509 | A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋) | ||
| Theorem | latmle2 18510 | A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) | ||
| Theorem | latlem12 18511 | An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍))) | ||
| Theorem | latleeqm1 18512 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋)) | ||
| Theorem | latleeqm2 18513 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑌 ∧ 𝑋) = 𝑋)) | ||
| Theorem | latmlem1 18514 | Add meet to both sides of a lattice ordering. (Contributed by NM, 10-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑍))) | ||
| Theorem | latmlem2 18515 | Add meet to both sides of a lattice ordering. (sslin 4243 analog.) (Contributed by NM, 10-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑍 ∧ 𝑋) ≤ (𝑍 ∧ 𝑌))) | ||
| Theorem | latmlem12 18516 | Add join to both sides of a lattice ordering. (ss2in 4245 analog.) (Contributed by NM, 10-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑍 ≤ 𝑊) → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑊))) | ||
| Theorem | latnlemlt 18517 | Negation of "less than or equal to" expressed in terms of meet and less-than. (nssinpss 4267 analog.) (Contributed by NM, 5-Feb-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) < 𝑋)) | ||
| Theorem | latnle 18518 | Equivalent expressions for "not less than" in a lattice. (chnle 31533 analog.) (Contributed by NM, 16-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑌 ≤ 𝑋 ↔ 𝑋 < (𝑋 ∨ 𝑌))) | ||
| Theorem | latmidm 18519 | Lattice meet is idempotent. Analogue of inidm 4227. (Contributed by NM, 8-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋) | ||
| Theorem | latabs1 18520 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs1 31535 analog.) (Contributed by NM, 8-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (𝑋 ∧ 𝑌)) = 𝑋) | ||
| Theorem | latabs2 18521 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs2 31536 analog.) (Contributed by NM, 8-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋) | ||
| Theorem | latledi 18522 | An ortholattice is distributive in one ordering direction. (ledi 31559 analog.) (Contributed by NM, 7-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍))) | ||
| Theorem | latmlej11 18523 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑋 ∨ 𝑍)) | ||
| Theorem | latmlej12 18524 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑍 ∨ 𝑋)) | ||
| Theorem | latmlej21 18525 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑋 ∨ 𝑍)) | ||
| Theorem | latmlej22 18526 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑍 ∨ 𝑋)) | ||
| Theorem | lubsn 18527 | The least upper bound of a singleton. (chsupsn 31432 analog.) (Contributed by NM, 20-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑋}) = 𝑋) | ||
| Theorem | latjass 18528 | Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 31552 analog.) (Contributed by NM, 17-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = (𝑋 ∨ (𝑌 ∨ 𝑍))) | ||
| Theorem | latj12 18529 | Swap 1st and 2nd members of lattice join. (chj12 31553 analog.) (Contributed by NM, 4-Jun-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑌 ∨ (𝑋 ∨ 𝑍))) | ||
| Theorem | latj32 18530 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 2-Dec-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ 𝑌)) | ||
| Theorem | latj13 18531 | Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑍 ∨ (𝑌 ∨ 𝑋))) | ||
| Theorem | latj31 18532 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 23-Jun-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑌) ∨ 𝑋)) | ||
| Theorem | latjrot 18533 | Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑋) ∨ 𝑌)) | ||
| Theorem | latj4 18534 | Rearrangement of lattice join of 4 classes. (chj4 31554 analog.) (Contributed by NM, 14-Jun-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑊))) | ||
| Theorem | latj4rot 18535 | Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑊 ∨ 𝑋) ∨ (𝑌 ∨ 𝑍))) | ||
| Theorem | latjjdi 18536 | Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = ((𝑋 ∨ 𝑌) ∨ (𝑋 ∨ 𝑍))) | ||
| Theorem | latjjdir 18537 | Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑍))) | ||
| Theorem | mod1ile 18538 | The weak direction of the modular law (e.g., pmod1i 39850, atmod1i1 39859) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑍 → (𝑋 ∨ (𝑌 ∧ 𝑍)) ≤ ((𝑋 ∨ 𝑌) ∧ 𝑍))) | ||
| Theorem | mod2ile 18539 | The weak direction of the modular law (e.g., pmod2iN 39851) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 ≤ 𝑋 → ((𝑋 ∧ 𝑌) ∨ 𝑍) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍)))) | ||
| Theorem | latmass 18540 | Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍))) | ||
| Theorem | latdisdlem 18541* | Lemma for latdisd 18542. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑢 ∨ (𝑣 ∧ 𝑤)) = ((𝑢 ∨ 𝑣) ∧ (𝑢 ∨ 𝑤)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
| Theorem | latdisd 18542* | In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∨ (𝑦 ∧ 𝑧)) = ((𝑥 ∨ 𝑦) ∧ (𝑥 ∨ 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
| Syntax | ccla 18543 | Extend class notation with complete lattices. |
| class CLat | ||
| Definition | df-clat 18544 | Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
| ⊢ CLat = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))} | ||
| Theorem | isclat 18545 | The predicate "is a complete lattice". (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝐾 ∈ CLat ↔ (𝐾 ∈ Poset ∧ (dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵))) | ||
| Theorem | clatpos 18546 | A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.) |
| ⊢ (𝐾 ∈ CLat → 𝐾 ∈ Poset) | ||
| Theorem | clatlem 18547 | Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → ((𝑈‘𝑆) ∈ 𝐵 ∧ (𝐺‘𝑆) ∈ 𝐵)) | ||
| Theorem | clatlubcl 18548 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝑈‘𝑆) ∈ 𝐵) | ||
| Theorem | clatlubcl2 18549 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝑈) | ||
| Theorem | clatglbcl 18550 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) | ||
| Theorem | clatglbcl2 18551 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝐺) | ||
| Theorem | oduclatb 18552 | Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ CLat ↔ 𝐷 ∈ CLat) | ||
| Theorem | clatl 18553 | A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5805 to shorten proof and eliminate joindmss 18424 and meetdmss 18438? |
| ⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat) | ||
| Theorem | isglbd 18554* | Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐻 ≤ 𝑦) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝐻) & ⊢ (𝜑 → 𝐾 ∈ CLat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝐻) | ||
| Theorem | lublem 18555* | Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧))) | ||
| Theorem | lubub 18556 | The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ≤ (𝑈‘𝑆)) | ||
| Theorem | lubl 18557* | The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → (𝑈‘𝑆) ≤ 𝑋)) | ||
| Theorem | lubss 18558 | Subset law for least upper bounds. (chsupss 31361 analog.) (Contributed by NM, 20-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝑈‘𝑆) ≤ (𝑈‘𝑇)) | ||
| Theorem | lubel 18559 | An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵) → 𝑋 ≤ (𝑈‘𝑆)) | ||
| Theorem | lubun 18560 | The LUB of a union. (Contributed by NM, 5-Mar-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑈‘(𝑆 ∪ 𝑇)) = ((𝑈‘𝑆) ∨ (𝑈‘𝑇))) | ||
| Theorem | clatglb 18561* | Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝐺‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆)))) | ||
| Theorem | clatglble 18562 | The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑋) | ||
| Theorem | clatleglb 18563* | Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑋 ≤ (𝐺‘𝑆) ↔ ∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦)) | ||
| Theorem | clatglbss 18564 | Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝐺‘𝑇) ≤ (𝐺‘𝑆)) | ||
| Syntax | cdlat 18565 | The class of distributive lattices. |
| class DLat | ||
| Definition | df-dlat 18566* | A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 18542) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))} | ||
| Theorem | isdlat 18567* | Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
| Theorem | dlatmjdi 18568 | In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) | ||
| Theorem | dlatl 18569 | A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝐾 ∈ DLat → 𝐾 ∈ Lat) | ||
| Theorem | odudlatb 18570 | The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ DLat ↔ 𝐷 ∈ DLat)) | ||
| Theorem | dlatjmdi 18571 | In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍))) | ||
| Syntax | cipo 18572 | Class function defining inclusion posets. |
| class toInc | ||
| Definition | df-ipo 18573* |
For any family of sets, define the poset of that family ordered by
inclusion. See ipobas 18576, ipolerval 18577, and ipole 18579 for its contract.
EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.) |
| ⊢ toInc = (𝑓 ∈ V ↦ ⦋{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({〈(Base‘ndx), 𝑓〉, 〈(TopSet‘ndx), (ordTop‘𝑜)〉} ∪ {〈(le‘ndx), 𝑜〉, 〈(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})〉})) | ||
| Theorem | ipostr 18574 | The structure of df-ipo 18573 is a structure defining indices up to 11. (Contributed by Mario Carneiro, 25-Oct-2015.) |
| ⊢ ({〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉} ∪ {〈(le‘ndx), ≤ 〉, 〈(oc‘ndx), ⊥ 〉}) Struct 〈1, ;11〉 | ||
| Theorem | ipoval 18575* | Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} ⇒ ⊢ (𝐹 ∈ 𝑉 → 𝐼 = ({〈(Base‘ndx), 𝐹〉, 〈(TopSet‘ndx), (ordTop‘ ≤ )〉} ∪ {〈(le‘ndx), ≤ 〉, 〈(oc‘ndx), (𝑥 ∈ 𝐹 ↦ ∪ {𝑦 ∈ 𝐹 ∣ (𝑦 ∩ 𝑥) = ∅})〉})) | ||
| Theorem | ipobas 18576 | Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by Mario Carneiro, 25-Oct-2015.) |
| ⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝑉 → 𝐹 = (Base‘𝐼)) | ||
| Theorem | ipolerval 18577* | Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝑉 → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} = (le‘𝐼)) | ||
| Theorem | ipotset 18578 | Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ (𝐹 ∈ 𝑉 → (ordTop‘ ≤ ) = (TopSet‘𝐼)) | ||
| Theorem | ipole 18579 | Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌)) | ||
| Theorem | ipolt 18580 | Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ < = (lt‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌)) | ||
| Theorem | ipopos 18581 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ 𝐼 ∈ Poset | ||
| Theorem | isipodrs 18582* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ ((toInc‘𝐴) ∈ Dirset ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)) | ||
| Theorem | ipodrscl 18583 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ ((toInc‘𝐴) ∈ Dirset → 𝐴 ∈ V) | ||
| Theorem | ipodrsfi 18584* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ (((toInc‘𝐴) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → ∃𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧) | ||
| Theorem | fpwipodrs 18585 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (toInc‘(𝒫 𝐴 ∩ Fin)) ∈ Dirset) | ||
| Theorem | ipodrsima 18586* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴) & ⊢ ((𝜑 ∧ (𝑢 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝐴)) → (𝐹‘𝑢) ⊆ (𝐹‘𝑣)) & ⊢ (𝜑 → (toInc‘𝐵) ∈ Dirset) & ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝐵) ∈ 𝑉) ⇒ ⊢ (𝜑 → (toInc‘(𝐹 “ 𝐵)) ∈ Dirset) | ||
| Theorem | isacs3lem 18587* | An algebraic closure system satisfies isacs3 18595. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶))) | ||
| Theorem | acsdrsel 18588 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝐶 ∧ (toInc‘𝑌) ∈ Dirset) → ∪ 𝑌 ∈ 𝐶) | ||
| Theorem | isacs4lem 18589* | In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶)) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪ (𝐹 “ 𝑡)))) | ||
| Theorem | isacs5lem 18590* | If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪ (𝐹 “ 𝑡))) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) | ||
| Theorem | acsdrscl 18591 | In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝒫 𝑋 ∧ (toInc‘𝑌) ∈ Dirset) → (𝐹‘∪ 𝑌) = ∪ (𝐹 “ 𝑌)) | ||
| Theorem | acsficl 18592 | A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝐹‘𝑆) = ∪ (𝐹 “ (𝒫 𝑆 ∩ Fin))) | ||
| Theorem | isacs5 18593* | A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) | ||
| Theorem | isacs4 18594* | A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝒫 𝑋((toInc‘𝑠) ∈ Dirset → (𝐹‘∪ 𝑠) = ∪ (𝐹 “ 𝑠)))) | ||
| Theorem | isacs3 18595* | A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶))) | ||
| Theorem | acsficld 18596 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 18592. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘𝑆) = ∪ (𝑁 “ (𝒫 𝑆 ∩ Fin))) | ||
| Theorem | acsficl2d 18597* | In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 18592. Deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑁‘𝑆) ↔ ∃𝑥 ∈ (𝒫 𝑆 ∩ Fin)𝑌 ∈ (𝑁‘𝑥))) | ||
| Theorem | acsfiindd 18598 | In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼)) | ||
| Theorem | acsmapd 18599* | In an algebraic closure system, if 𝑇 is contained in the closure of 𝑆, there is a map 𝑓 from 𝑇 into the set of finite subsets of 𝑆 such that the closure of ∪ ran 𝑓 contains 𝑇. This is proven by applying acsficl2d 18597 to each element of 𝑇. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑇 ⊆ (𝑁‘𝑆)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑇 ⊆ (𝑁‘∪ ran 𝑓))) | ||
| Theorem | acsmap2d 18600* | In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is independent, then there is a map 𝑓 from 𝑇 into the set of finite subsets of 𝑆 such that 𝑆 equals the union of ran 𝑓. This is proven by taking the map 𝑓 from acsmapd 18599 and observing that, since 𝑆 and 𝑇 have the same closure, the closure of ∪ ran 𝑓 must contain 𝑆. Since 𝑆 is independent, by mrissmrcd 17683, ∪ ran 𝑓 must equal 𝑆. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑆 = ∪ ran 𝑓)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |