isAtom_iff_le_of_ge
theorem isAtom_iff_le_of_ge :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] {a : α},
IsAtom a ↔ a ≠ ⊥ ∧ ∀ (b : α), b ≠ ⊥ → b ≤ a → a ≤ b
The theorem `isAtom_iff_le_of_ge` states that for any type `α` that has a preorder and a bottom element, an element `a` of `α` is an atom if and only if `a` is not the bottom element and for all elements `b` of `α`, if `b` is not the bottom element, then whenever `b` is less than or equal to `a`, it follows that `a` is less than or equal to `b`. In essence, it says that an atom is an element that is only comparable to the bottom element (except for equality).
More concisely: An element `a` of a preordered type with a bottom element is an atom if and only if it is not the bottom element and for all non-bottom elements `b`, if `b` is less than or equal to `a`, then `a` is less than or equal to `b`.
|
isAtomic_dual_iff_isCoatomic
theorem isAtomic_dual_iff_isCoatomic :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α], IsAtomic αᵒᵈ ↔ IsCoatomic α
This theorem states that for any type `α` with a partial order and a greatest element (order top), the dual of `α` is atomic if and only if `α` is coatomic. In this context, an "atomic" order means that every element is below some atom (an indivisible unit), while a "coatomic" order means every element is below some coatom (an element that cannot be divided further).
More concisely: For a type `α` with a partial order and a greatest element, the dual order is atomic if and only if `α` is coatomic.
|
IsAtom.bot_covBy
theorem IsAtom.bot_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsAtom a → ⊥ ⋖ a
This theorem, which is an alternative formulation of the reverse direction of `bot_covBy_iff`, states that for any type `α` that is a partial order with a least element (represented by `⊥`), if an element `a` of `α` is an atom, then `⊥` is covered by `a`. Here, an atom is defined as an element with no other element between it and `⊥`, and is not `⊥` itself. In this context, `⊥` being "covered by" `a` means that there is no other element between them.
More concisely: For any type `α` with a least element `⊥` and partial order structure, if `a` is an atom, then `⊥` is covered by `a`. (That is, there is no element between `⊥` and `a` in the partial order.)
|
OrderIso.isSimpleOrder_iff
theorem OrderIso.isSimpleOrder_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β], α ≃o β → (IsSimpleOrder α ↔ IsSimpleOrder β)
This theorem states that for any two types `α` and `β`, given that they both are Partial Orders and Bounded Orders, if there exists an order isomorphism (`≃o`) between `α` and `β`, then `α` is a simple order if and only if `β` is a simple order. In mathematical terms, a simple order is an order where there are no elements in between any two distinct elements. The theorem establishes that this property is preserved under an order isomorphism.
More concisely: If `α` and `β` are types that are Partial Orders and Bounded Orders with an order isomorphism `α ≃o β`, then `α` is a simple order if and only if `β` is a simple order.
|
isAtomistic_dual_iff_isCoatomistic
theorem isAtomistic_dual_iff_isCoatomistic :
∀ {α : Type u_1} [inst : CompleteLattice α], IsAtomistic αᵒᵈ ↔ IsCoatomistic α
This theorem states that for any type `α` equipped with a structure of `CompleteLattice`, the dual lattice `αᵒᵈ` is atomistic if and only if the original lattice `α` is coatomistic. In the context of lattice theory, a lattice is said to be atomistic if any element can be written as a join of atoms, and coatomistic if any element can be written as a meet of coatoms. The theorem thus provides a duality between atomistic and coatomistic lattices, saying that flipping the lattice (forming the dual) swaps these two properties.
More concisely: A complete lattice `α` has atomistic dual if and only if it is coatomistic.
|
IsCoatomistic.eq_sInf_coatoms
theorem IsCoatomistic.eq_sInf_coatoms :
∀ {α : Type u_1} [inst : CompleteLattice α] [self : IsCoatomistic α] (b : α),
∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a
This theorem states that for any type `α` that forms a complete lattice and has the property `IsCoatomistic`, every element `b` of `α` can be expressed as the infimum (`sInf`) of a set of coatoms. A coatom in this context refers to an element that has no other elements between it and the top element of the order, and is not the top element itself. Here, the theorem ensures that not only can `b` be written as the infimum of some set `s`, but also that all elements `a` in `s` are coatoms.
More concisely: For every complete lattice `α` with the property `IsCoatomistic`, every element `b` can be written as the infimum of a set of coatoms.
|
IsCoatomic.eq_top_or_exists_le_coatom
theorem IsCoatomic.eq_top_or_exists_le_coatom :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] [self : IsCoatomic α] (b : α),
b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
The theorem `IsCoatomic.eq_top_or_exists_le_coatom` states that for any partially ordered set with a greatest element (denoted by `⊤`), and for any element `b` of this set, the following is true: Either `b` is the greatest element `⊤`, or there exists another element `a` that is a coatom and `b` is less than or equal to `a`. A coatom is defined in this context as an element which is not `⊤` but has no other elements between it and `⊤`.
More concisely: For any element `b` in a partially ordered set with a greatest element `⊤`, either `b` equals `⊤` or there exists a coatom `a` such that `b ≤ a`.
|
IsSimpleOrder.LT.lt.eq_top
theorem IsSimpleOrder.LT.lt.eq_top :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : BoundedOrder α] [inst_2 : IsSimpleOrder α] {a b : α},
a < b → b = ⊤
This theorem, `IsSimpleOrder.LT.lt.eq_top`, is an alias of `IsSimpleOrder.eq_top_of_lt`. It states that for any type `α` that has a pre-order, a bounded order, and is a simple order, if an element `a` of type `α` is less than another element `b` of type `α`, then `b` must be equal to the greatest element or top (`⊤`) of the order.
More concisely: In a simple order with a greatest element, if `a` is less than `b`, then `b` is the greatest element.
|
Set.isSimpleOrder_Iic_iff_isAtom
theorem Set.isSimpleOrder_Iic_iff_isAtom :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsSimpleOrder ↑(Set.Iic a) ↔ IsAtom a := by
sorry
This theorem states that for any partially ordered type `α` that also has a bottom element, and for any element `a` of type `α`, the condition of the interval from negative infinity to `a` (inclusive) being a simple order is equivalent to the element `a` being an atom. In the context of ordered types, a simple order is an order with no elements in between, and an atom is an element with no other element between it and the bottom element, and it itself is not the bottom element. Essentially, this theorem connects the properties of an individual element and the order structure on the entire interval leading up to that element.
More concisely: For any partially ordered type with a bottom element, an element is an atom if and only if the interval from negative infinity to that element forms a simple order.
|
IsAtom.lt_iff
theorem IsAtom.lt_iff :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a x : α}, IsAtom a → (x < a ↔ x = ⊥)
The theorem `IsAtom.lt_iff` states that for any type `α` that has a partial order and a least element (denoted by `⊥`), given any elements `a` and `x` of `α`, if `a` is an atom (meaning that there exists no element between `a` and `⊥`, and `a` is not `⊥`), then `x` is less than `a` if and only if `x` is equal to `⊥`.
More concisely: For any type with a partial order and a least element, an atom (which is neither the least element nor equal to it) is related to any other element via the partial order if and only if that other element is the least element.
|
IsAtomic.eq_bot_or_exists_atom_le
theorem IsAtomic.eq_bot_or_exists_atom_le :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] [self : IsAtomic α] (b : α),
b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
This theorem states that for any given element in a partially ordered set, which is also an atomic order with a least element (denoted `⊥`), that element is either the least element itself (`⊥`), or there exists an atom less than or equal to it. Here, an atom is defined as an element which has no other elements between it and the least element, and is not the least element itself.
More concisely: In a partially ordered set with a least element (denoted `⊥`), every element is either the least element itself or has an atom below it.
|
GaloisInsertion.isAtom_of_u_bot
theorem GaloisInsertion.isAtom_of_u_bot :
∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
[inst_3 : OrderBot β] {l : α → β} {u : β → α},
GaloisInsertion l u → u ⊥ = ⊥ → ∀ {b : β}, IsAtom (u b) → IsAtom b
The theorem `GaloisInsertion.isAtom_of_u_bot` states that for any two types `α` and `β`, each equipped with a partial order and a least element (`OrderBot`), and two functions `l : α → β` and `u : β → α` forming a Galois insertion (i.e., `l` is left adjoint to `u`), if the image of the least element of `β` under `u` is also the least element of `α`, then any element `b` of `β` such that `u b` is an atom of `α` (i.e., `u b` is an element with no other element between it and the least element of `α`, and `u b` is not the least element of `α`), is also an atom of `β`. In other words, if an element becomes an atom when mapped from `β` to `α` by `u`, it was already an atom in `β`.
More concisely: If `l : α -> β` and `u : β -> α` form a Galois insertion with `OrderBot` elements `b0 : β` and `a0 : α` such that `u (b0) = a0`, then any atom `a` of `α` with `u a = b` is an atom of `β`.
|
IsSimpleOrder.LT.lt.eq_bot
theorem IsSimpleOrder.LT.lt.eq_bot :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : BoundedOrder α] [inst_2 : IsSimpleOrder α] {a b : α},
a < b → a = ⊥
This theorem, `IsSimpleOrder.LT.lt.eq_bot`, is an alias of `IsSimpleOrder.eq_bot_of_lt`. It states that for any given type `α` that has a Preorder relation, is a BoundedOrder, and is a SimpleOrder, if an element `a` is less than another element `b`, then `a` must be equal to the bottom element of the order (`⊥`). This essentially means that in a simple order, the element `a` can't be less than `b` unless it's the smallest possible element in the order.
More concisely: In a simple order `α` with bottom element `⊥`, if `a < b` then `a = ⊥`.
|
isSimpleOrder_iff_isAtom_top
theorem isSimpleOrder_iff_isAtom_top :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α], IsSimpleOrder α ↔ IsAtom ⊤
The theorem `isSimpleOrder_iff_isAtom_top` states that for any type `α` that has a partial order and a bounded order, `α` is a simple order if and only if the top element (denoted as `⊤`) is an atom.
In this context, an atom of a bounded order is an element with no other element between it and the bottom element (denoted as `⊥`). Also, the atom is not equal to the bottom element. And a simple order is a special type of partial order where every non-top element is below some other element.
More concisely: A bounded partial order `α` is simple if and only if its top element `⊤` is an atom that is strictly above the bottom element `⊥`.
|
CovBy.isCoatom
theorem CovBy.isCoatom : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a ⋖ ⊤ → IsCoatom a
The theorem named `CovBy.isCoatom` states that for any type `α` that has a partial order and a greatest element (`⊤`), if an element `a` of this type strictly precedes the greatest element, then `a` is a coatom. In mathematical terms, a coatom of a partially ordered set is an element that is not the greatest element, and there is no other element that lies strictly between it and the greatest element.
More concisely: If `α` is a type with a partial order and a greatest element `⊤`, then an element `a` strictly preceding `⊤` is a coatom if and only if there is no element `x` such that `a < x < ⊤`.
|
Mathlib.Order.Atoms._auxLemma.3
theorem Mathlib.Order.Atoms._auxLemma.3 :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, (⊥ < a) = (a ≠ ⊥)
This theorem, `Mathlib.Order.Atoms._auxLemma.3`, states that for any type `α` that has a partial order and a least element (notated as `⊥`), and for any element `a` of this type, the proposition that the least element is less than `a` is equivalent to the proposition that `a` is not equal to the least element. In other words, `a` being greater than the absolute minimum implies that `a` is distinct from it.
More concisely: For any type with a partial order and a least element, the least element is strictly less than any element distinct from it.
|
IsAtom.of_compl
theorem IsAtom.of_compl : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {a : α}, IsAtom aᶜ → IsCoatom a
This theorem, referred to as `IsAtom.of_compl`, states that for any Boolean algebra `α` and any element `a` in `α`, if the complement of `a` is an atom, then `a` itself is a coatom. Here, an atom in a Boolean algebra is an element for which there is no other element between it and the bottom (`⊥`), excluding the bottom. Likewise, a coatom is an element for which there is no other element between it and the top (`⊤`), excluding the top itself.
More concisely: If an element in a Boolean algebra has its complement as an atom, then that element is a coatom.
|
IsCoatom.dual
theorem IsCoatom.dual :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → IsAtom (OrderDual.toDual a) := by
sorry
The theorem `IsCoatom.dual` states that for any type `α` with a preorder and an order top, if an element `a` is a coatom, then the dual of `a` is an atom. Here, a coatom is an element where there's no other element between it and the top element, and it's not the top element itself; while an atom is an element where there's no other element between it and the bottom element, and it's not the bottom element itself. The dual of an element is just the element itself in the dual order, where the order is reversed.
More concisely: If an element `a` is a coatom in a preordered type with an order top, then the dual of `a` is an atom.
|
isCoatomic_dual_iff_isAtomic
theorem isCoatomic_dual_iff_isAtomic :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α], IsCoatomic αᵒᵈ ↔ IsAtomic α
This theorem states that for any type `α` with a partial order and a bottom element, `α` is coatomic in the dual order if and only if `α` is atomic. In mathematical terms, a poset (partially ordered set) is said to be atomic if every element greater than the bottom element is the least upper bound of some set of atomic elements. Similarly, a poset is coatomic if every element less than the top element is the greatest lower bound of some set of coatomic elements. The dual order is the inverse of the original order.
More concisely: A type `α` with a partial order and a bottom element is coatomic in the dual order if and only if it is atomic.
|
Mathlib.Order.Atoms._auxLemma.4
theorem Mathlib.Order.Atoms._auxLemma.4 : ∀ {a b : Prop}, (¬a → ¬b) = (b → a)
This theorem, `Mathlib.Order.Atoms._auxLemma.4`, states that for any two propositions `a` and `b`, the statement "if `a` is not true, then `b` is not true" is logically equivalent to the statement "if `b` is true, then `a` is also true". In mathematical notation, this theorem expresses the equivalence between `¬a → ¬b` and `b → a`.
More concisely: The negation of proposition `a` is logically equivalent to the implication `b` implies `a`. In symbols, `¬a ≃ b → a`.
|
IsSimpleOrder.eq_bot_or_eq_top
theorem IsSimpleOrder.eq_bot_or_eq_top :
∀ {α : Type u_3} [inst : LE α] [inst_1 : BoundedOrder α] [self : IsSimpleOrder α] (a : α), a = ⊥ ∨ a = ⊤
The theorem `IsSimpleOrder.eq_bot_or_eq_top` states that for any given type `α` that has an order (`LE α`), a bounded order (`BoundedOrder α`), and is a simple order (`IsSimpleOrder α`), any element `a` of this type `α` is either the least element (denoted as `⊥`) or the greatest element (denoted as `⊤`).
More concisely: In a simple order `α` with least (⊥) and greatest (⊤) elements, every element `a` lies below or equals the greatest element (⊤) or is equal to the least element (⊥).
|
IsAtom.le_iff
theorem IsAtom.le_iff :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a x : α}, IsAtom a → (x ≤ a ↔ x = ⊥ ∨ x = a) := by
sorry
The theorem `IsAtom.le_iff` states that for all types `α` equipped with a partial ordering and a least element denoted by `⊥`, and for all elements `a` and `x` in `α`, if `a` is an atom (meaning `a` is not the least element and there are no elements between `a` and `⊥`), then `x` is less than or equal to `a` if, and only if, `x` is either `⊥` or `a`. In other words, in an ordered set with a least element, if `a` is an atom, then any element `x` that's not greater than `a` must be either the least element, `⊥`, or `a` itself.
More concisely: For all types `α` with a partial ordering and least element `⊥`, if `a` is an atom in `α`, then `x ≤ a` if and only if `x = ⊥` or `x = a`.
|
IsAtom.compl
theorem IsAtom.compl : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {a : α}, IsAtom a → IsCoatom aᶜ
The theorem `IsAtom.compl` states that for any type `α` that is a Boolean algebra, given an element `a` of `α` that is an atom, the complement of `a` (denoted as `aᶜ`) is a coatom. In other words, if `a` is an atom, which means it is an element with no other element between it and the bottom (`⊥`) and it is not the bottom (`⊥`), then its complement is a coatom, which means there is no other element between it and the top (`⊤`) and it is not the top (`⊤`).
More concisely: If `α` is a Boolean algebra and `a` is an atom in `α`, then the complement `aᶜ` is a coatom in `α`.
|
IsCompl.isAtom_iff_isCoatom
theorem IsCompl.isAtom_iff_isCoatom :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] [inst_2 : IsModularLattice α] {a b : α},
IsCompl a b → (IsAtom a ↔ IsCoatom b)
This theorem states that for any type `α` that forms a lattice, is a bounded order, and is a modular lattice, given any two elements `a` and `b` of this type, if `a` and `b` are complements (as indicated by `IsCompl a b`), then `a` is an atom (an element with no other element between it and the bottom element, and which is not the bottom element itself) if and only if `b` is a coatom (an element with no other element between it and the top element, and which is not the top element itself).
More concisely: For any lattice type `α` that is bounded and modular, elements `a` and `b` are complements if and only if `a` is an atom if and only if `b` is a coatom.
|
bot_covBy_iff
theorem bot_covBy_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ ⋖ a ↔ IsAtom a := by
sorry
This theorem states that for any type `α` which is a partial order and has a least element, a specific element `a` of this type is covered by the least element if and only if `a` is an atom. Here, an atom of an `OrderBot` is defined as an element which has no other element between it and the least element, and it is not the least element itself. "Covered by" means that there's no other element between these two elements. In mathematical terms, we say `⊥` covers `a` if there is no element `b` such that `⊥ < b < a`.
More concisely: For any partial order type `α` with a least element, an element `a` is covered by the least element if and only if `a` is an atom (i.e., there is no element between `a` and the least element).
|
OrderIso.isAtom_iff
theorem OrderIso.isAtom_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
[inst_3 : OrderBot β] (f : α ≃o β) (a : α), IsAtom (f a) ↔ IsAtom a
The theorem `OrderIso.isAtom_iff` states that for any types `α` and `β`, each equipped with partial order structures and a least element (`OrderBot`), if `f` is an order isomorphism (bijective and order-preserving function) from `α` to `β` and `a` is an element of `α`, then `a` being an atom in `α` is equivalent to `f(a)` being an atom in `β`. In other words, `a` is an atom in `α` (meaning `a` is not the least element and there's no other element between `a` and the least element) if and only if its image under `f`, `f(a)`, is an atom in `β`.
More concisely: For any order isomorphisms between partially ordered types with least elements, the image of an atom under the function is an atom in the image type.
|
IsCompl.isCoatom_iff_isAtom
theorem IsCompl.isCoatom_iff_isAtom :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] [inst_2 : IsModularLattice α] {a b : α},
IsCompl a b → (IsCoatom a ↔ IsAtom b)
The theorem `IsCompl.isCoatom_iff_isAtom` states that for any type `α` that forms a bounded modular lattice, given any two elements `a` and `b` of this lattice, if `a` and `b` are complements, then `a` is a coatom if and only if `b` is an atom. In other words, if `a` and `b` are complementary in the lattice, then `a` being just below the top element (`⊤`) with no other elements in between corresponds to `b` being just above the bottom element (`⊥`) with no other elements in between, and vice versa.
More concisely: For any bounded modular lattice type `α`, if `a` and `b` are complementary elements, then `a` is a coatom if and only if `b` is an atom.
|
IsCoatom.compl
theorem IsCoatom.compl : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {a : α}, IsCoatom a → IsAtom aᶜ
This theorem, named as `IsCoatom.compl`, states that for any type `α` that is a Boolean algebra and any element `a` of `α`, if `a` is a coatom of the Boolean algebra, then the complement of `a`, represented as `aᶜ`, is an atom of the Boolean algebra.
In more informal terms, this theorem is asserting that if `a` is a coatom, which means it's an element that is just one step below the top element and there are no other elements between it and the top element, then the complement of `a` is an atom, meaning it's an element just one step above the bottom element and there are no other elements between it and the bottom element. This is a property that holds in Boolean algebras.
More concisely: If `α` is a Boolean algebra and `a` is a coatom in `α`, then the complement `aᶜ` is an atom in `α`.
|
isAtom_top
theorem isAtom_top :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [inst_2 : IsSimpleOrder α], IsAtom ⊤
The theorem `isAtom_top` states that for any type `α` which has a `PartialOrder`, is a `BoundedOrder`, and is a `SimpleOrder`, the top element `⊤` is an atom. In the context of order theory, an atom is defined as an element which has no other elements between it and the bottom element `⊥`, and it is not the bottom element itself. Thus, in these particular kinds of orders, the top element is such a minimal element above the bottom.
More concisely: In any type endowed with a SimpleOrder that is both Bounded and Partial, the top element is an atom.
|
CovBy.is_atom
theorem CovBy.is_atom : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ ⋖ a → IsAtom a := by
sorry
The theorem `CovBy.is_atom` states that for any type `α` that has a partial order and a least element (or bottom element), if the least element is strictly covered by some element `a` (i.e., the least element is less than `a` and there is no element between them), then `a` is an atom. In this context, an atom is defined as an element that is not the least element and has no other elements between it and the least element.
More concisely: If a type with a partial order and a least element has an element strictly covering the least element with no elements between them, then that element is an atom.
|
IsCoatom.covBy_top
theorem IsCoatom.covBy_top :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → a ⋖ ⊤
The theorem `IsCoatom.covBy_top` states that for any type `α` with a partial order and a greatest element (denoted `⊤`), if an element `a` is a coatom, then `a` is covered by `⊤`. In this context, an element `a` being a coatom means that there are no elements between it and `⊤`, and it is not `⊤` itself. Being "covered by `⊤`" is a relation defined as: `a` is less than `⊤` and there is no other element between `a` and `⊤`.
More concisely: For any type equipped with a partial order and a greatest element, if an element is a coatom (i.e., an upper bound that is not the greatest element), then it is covered by the greatest element.
|
IsAtom.dual
theorem IsAtom.dual :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, IsAtom a → IsCoatom (OrderDual.toDual a) := by
sorry
The theorem `IsAtom.dual` states that for any type `α` that has a preorder and a least element (expressed as `OrderBot α`), if an element `a` of `α` is an atom, then the dual of `a` (obtained via `OrderDual.toDual`) is a coatom. In other words, an atom in the original order becomes a coatom in the dual order. An atom is defined as an element which has no other elements between it and the bottom element (`⊥`), and is not `⊥` itself. A coatom is an element which has no other elements between it and the top element (`⊤`), and is not `⊤` itself.
More concisely: If `α` is a type with a preorder and a least element, and `a` is an atom of `α` in the original order, then `OrderDual.toDual a` is a coatom in the dual order.
|
IsCoatom.of_compl
theorem IsCoatom.of_compl : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {a : α}, IsCoatom aᶜ → IsAtom a
The theorem `IsCoatom.of_compl` states that for any type `α` that is a boolean algebra, and for any element `a` of `α`, if the complement of `a` is a coatom (i.e., an element with no other element between it and the greatest element `⊤`, and it is not `⊤` itself), then `a` is an atom (meaning it is an element with no other element between it and the lowest element `⊥`, and it is not `⊥` itself). In other words, the atom-hood of `a` can be deduced from the coatom-hood of its complement `aᶜ`.
More concisely: If `α` is a boolean algebra and `a` is an element with complement `aᶜ` that is a coatom, then `a` is an atom.
|
IsAtomistic.eq_sSup_atoms
theorem IsAtomistic.eq_sSup_atoms :
∀ {α : Type u_1} [inst : CompleteLattice α] [self : IsAtomistic α] (b : α), ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
This theorem states that for any type `α` that is a complete lattice and is atomistic, every element `b` of type `α` can be represented as the supremum (`sSup`) of a set of atoms (`s`). In other words, there exists a set `s` such that `b` equals the supremum of `s` and every element `a` in `s` is an atom. In the context of this theorem, an atom is an element that is only one step above the bottom element (`⊥`) with no other elements in between.
More concisely: For every complete lattice `α` that is atomistic, each element `b` can be expressed as the supremum of a set of atoms.
|