Mathlib.Order.Atoms

IsAtom definition

(a : α) : Prop

Full source

/-- An atom of an `OrderBot` is an element with no other element between it and `⊥`,
  which is not `⊥`. -/
def IsAtom (a : α) : Prop :=
  a ≠ ⊥a ≠ ⊥ ∧ ∀ b, b < a → b = ⊥

Atom in a Bounded Order

Informal description

An element $ a $ in an order with a bottom element $ \bot $ is called an *atom* if it is not equal to $ \bot $ and there is no other element strictly between $ \bot $ and $ a $. In other words, $ a \neq \bot $ and for any element $ b $, if $ b < a $, then $ b = \bot $.

IsAtom.Iic theorem

(ha : IsAtom a) (hax : a ≤ x) : IsAtom (⟨a, hax⟩ : Set.Iic x)

Full source

theorem IsAtom.Iic (ha : IsAtom a) (hax : a ≤ x) : IsAtom (⟨a, hax⟩ : Set.Iic x) :=
  ⟨fun con => ha.1 (Subtype.mk_eq_mk.1 con), fun ⟨b, _⟩ hba => Subtype.mk_eq_mk.2 (ha.2 b hba)⟩

Atom in Interval is Atom in Original Order

Informal description

Let $a$ be an atom in a bounded order $\alpha$ with bottom element $\bot$, and let $x \in \alpha$ such that $a \leq x$. Then the element $\langle a, hax \rangle$ in the interval $(-\infty, x]$ is also an atom.

IsAtom.of_isAtom_coe_Iic theorem

{a : Set.Iic x} (ha : IsAtom a) : IsAtom (a : α)

Full source

theorem IsAtom.of_isAtom_coe_Iic {a : Set.Iic x} (ha : IsAtom a) : IsAtom (a : α) :=
  ⟨fun con => ha.1 (Subtype.ext con), fun b hba =>
    Subtype.mk_eq_mk.1 (ha.2 ⟨b, hba.le.trans a.prop⟩ hba)⟩

Atom in Interval Implies Atom in Original Order

Informal description

Let $a$ be an element of the interval $(-\infty, x]$ in a bounded order $\alpha$ with bottom element $\bot$. If $a$ is an atom in this interval, then its underlying element in $\alpha$ is also an atom.

isAtom_iff_le_of_ge theorem

: IsAtom a ↔ a ≠ ⊥ ∧ ∀ b ≠ ⊥, b ≤ a → a ≤ b

Full source

theorem isAtom_iff_le_of_ge : IsAtomIsAtom a ↔ a ≠ ⊥ ∧ ∀ b ≠ ⊥, b ≤ a → a ≤ b :=
  and_congr Iff.rfl <|
    forall_congr' fun b => by
      simp only [Ne, @not_imp_comm (b = ⊥), Classical.not_imp, lt_iff_le_not_le]

Characterization of Atoms in a Bounded Order

Informal description

An element $a$ in a bounded order is an atom if and only if $a \neq \bot$ and for every element $b \neq \bot$, if $b \leq a$ then $a \leq b$.

IsAtom.lt_iff theorem

(h : IsAtom a) : x < a ↔ x = ⊥

Full source

theorem IsAtom.lt_iff (h : IsAtom a) : x < a ↔ x = ⊥ :=
  ⟨h.2 x, fun hx => hx.symm ▸ h.1.bot_lt⟩

Characterization of Elements Below an Atom

Informal description

Let $a$ be an atom in a bounded order with bottom element $\bot$. For any element $x$, we have $x < a$ if and only if $x = \bot$.

IsAtom.le_iff theorem

(h : IsAtom a) : x ≤ a ↔ x = ⊥ ∨ x = a

Full source

theorem IsAtom.le_iff (h : IsAtom a) : x ≤ a ↔ x = ⊥ ∨ x = a := by rw [le_iff_lt_or_eq, h.lt_iff]

Characterization of Elements Below or Equal to an Atom

Informal description

Let $a$ be an atom in a bounded order with bottom element $\bot$. For any element $x$, we have $x \leq a$ if and only if $x = \bot$ or $x = a$.

IsAtom.bot_lt theorem

(h : IsAtom a) : ⊥ < a

Full source

lemma IsAtom.bot_lt (h : IsAtom a) : ⊥ < a :=
  h.lt_iff.mpr rfl

Bottom Element is Strictly Below an Atom

Informal description

For any atom $a$ in a bounded order with bottom element $\bot$, we have $\bot < a$.

IsAtom.le_iff_eq theorem

(ha : IsAtom a) (hb : b ≠ ⊥) : b ≤ a ↔ b = a

Full source

lemma IsAtom.le_iff_eq (ha : IsAtom a) (hb : b ≠ ⊥) : b ≤ a ↔ b = a :=
  ha.le_iff.trans <| or_iff_right hb

Characterization of Non-Bottom Elements Below an Atom: $b \leq a \leftrightarrow b = a$

Informal description

Let $a$ be an atom in a bounded order with bottom element $\bot$, and let $b$ be an element such that $b \neq \bot$. Then $b \leq a$ if and only if $b = a$.

IsAtom.Iic_eq theorem

(h : IsAtom a) : Set.Iic a = {⊥, a}

Full source

theorem IsAtom.Iic_eq (h : IsAtom a) : Set.Iic a = {⊥, a} :=
  Set.ext fun _ => h.le_iff

Characterization of the Lower Set of an Atom: $\text{Iic}(a) = \{\bot, a\}$

Informal description

Let $a$ be an atom in a bounded order with bottom element $\bot$. Then the set of all elements less than or equal to $a$ is exactly $\{\bot, a\}$, i.e., $\{x \mid x \leq a\} = \{\bot, a\}$.

bot_covBy_iff theorem

: ⊥ ⋖ a ↔ IsAtom a

Full source

@[simp]
theorem bot_covBy_iff : ⊥⊥ ⋖ a⊥ ⋖ a ↔ IsAtom a := by
  simp only [CovBy, bot_lt_iff_ne_bot, IsAtom, not_imp_not]

Cover Relation Characterizes Atoms: $\bot \lessdot a \leftrightarrow \text{IsAtom}(a)$

Informal description

For an element $a$ in an order with a bottom element $\bot$, the relation $\bot \lessdot a$ (read as "$\bot$ is covered by $a$") holds if and only if $a$ is an atom. That is, $a \neq \bot$ and there is no element strictly between $\bot$ and $a$.

atom_le_iSup theorem

[Order.Frame α] {a : α} (ha : IsAtom a) {f : ι → α} : a ≤ iSup f ↔ ∃ i, a ≤ f i

Full source

theorem atom_le_iSup [Order.Frame α] {a : α} (ha : IsAtom a) {f : ι → α} :
    a ≤ iSup f ↔ ∃ i, a ≤ f i := by
  refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩
  show (a ≤ ⨆ i, f i) → _
  refine fun h => of_not_not fun ha' => ?_
  push_neg at ha'
  have ha'' : Disjoint a (⨆ i, f i) :=
    disjoint_iSup_iff.2 fun i => fun x hxa hxf => le_bot_iff.2 <| of_not_not fun hx =>
      have hxa : x < a := (le_iff_eq_or_lt.1 hxa).resolve_left (by rintro rfl; exact ha' _ hxf)
      hx (ha.2 _ hxa)
  obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
  exact ha.1 rfl

Atom is Below Supremum if and only if Below Some Element in the Family

Informal description

Let $\alpha$ be a frame (complete lattice with infinite distributive laws) and let $a \in \alpha$ be an atom. For any family of elements $(f_i)_{i \in \iota}$ in $\alpha$, the atom $a$ is less than or equal to the supremum $\bigsqcup_{i \in \iota} f_i$ if and only if there exists some index $i \in \iota$ such that $a \leq f_i$.

IsCoatom definition

[OrderTop α] (a : α) : Prop

Full source

/-- A coatom of an `OrderTop` is an element with no other element between it and `⊤`,
  which is not `⊤`. -/
def IsCoatom [OrderTop α] (a : α) : Prop :=
  a ≠ ⊤a ≠ ⊤ ∧ ∀ b, a < b → b = ⊤

Coatom in an ordered set with top

Informal description

An element $a$ in an order with a top element $\top$ is called a *coatom* if it is not equal to $\top$ and there is no element strictly between $a$ and $\top$, i.e., for any element $b$, if $a < b$ then $b = \top$.

isCoatom_dual_iff_isAtom theorem

[OrderBot α] {a : α} : IsCoatom (OrderDual.toDual a) ↔ IsAtom a

Full source

@[simp]
theorem isCoatom_dual_iff_isAtom [OrderBot α] {a : α} :
    IsCoatomIsCoatom (OrderDual.toDual a) ↔ IsAtom a :=
  Iff.rfl

Duality between Atoms and Coatoms: $a^{\text{op}}$ is a coatom iff $a$ is an atom

Informal description

Let $\alpha$ be an ordered set with a bottom element $\bot$. For any element $a \in \alpha$, the dual element $a^{\text{op}}$ in the order dual $\alpha^{\text{op}}$ is a coatom if and only if $a$ is an atom in $\alpha$. Here, an *atom* is a minimal non-$\bot$ element (i.e., $a \neq \bot$ and for any $b < a$, we have $b = \bot$), and a *coatom* is a maximal non-$\top$ element (i.e., $a \neq \top$ and for any $b > a$, we have $b = \top$).

isAtom_dual_iff_isCoatom theorem

[OrderTop α] {a : α} : IsAtom (OrderDual.toDual a) ↔ IsCoatom a

Full source

@[simp]
theorem isAtom_dual_iff_isCoatom [OrderTop α] {a : α} :
    IsAtomIsAtom (OrderDual.toDual a) ↔ IsCoatom a :=
  Iff.rfl

Duality between Atoms and Coatoms: $\text{IsAtom}(\text{toDual}(a)) \leftrightarrow \text{IsCoatom}(a)$

Informal description

Let $\alpha$ be an ordered set with a top element $\top$. For any element $a \in \alpha$, the dual element $\text{toDual}(a)$ in the order dual $\alpha^{\text{op}}$ is an atom if and only if $a$ is a coatom in $\alpha$. In other words, $a$ is a coatom (i.e., $a \neq \top$ and for all $b \in \alpha$, $a < b$ implies $b = \top$) if and only if $\text{toDual}(a)$ is an atom in $\alpha^{\text{op}}$ (i.e., $\text{toDual}(a) \neq \bot$ and for all $b \in \alpha^{\text{op}}$, $b < \text{toDual}(a)$ implies $b = \bot$).

IsCoatom.Ici theorem

(ha : IsCoatom a) (hax : x ≤ a) : IsCoatom (⟨a, hax⟩ : Set.Ici x)

Full source

theorem IsCoatom.Ici (ha : IsCoatom a) (hax : x ≤ a) : IsCoatom (⟨a, hax⟩ : Set.Ici x) :=
  ha.dual.Iic hax

Coatom in Original Order Implies Coatom in Interval $[x, \infty)$

Informal description

Let $\alpha$ be an ordered set with a top element $\top$, and let $a \in \alpha$ be a coatom (i.e., $a \neq \top$ and for any $b \in \alpha$, if $a < b$ then $b = \top$). For any element $x \in \alpha$ such that $x \leq a$, the element $\langle a, h_{ax} \rangle$ in the interval $[x, \infty)$ is also a coatom.

IsCoatom.of_isCoatom_coe_Ici theorem

{a : Set.Ici x} (ha : IsCoatom a) : IsCoatom (a : α)

Full source

theorem IsCoatom.of_isCoatom_coe_Ici {a : Set.Ici x} (ha : IsCoatom a) : IsCoatom (a : α) :=
  @IsAtom.of_isAtom_coe_Iic αᵒᵈ _ _ x a ha

Coatom in Interval Implies Coatom in Original Order

Informal description

Let $a$ be an element of the interval $[x, \infty)$ in an ordered set $\alpha$ with a top element $\top$. If $a$ is a coatom in this interval, then its underlying element in $\alpha$ is also a coatom.

isCoatom_iff_ge_of_le theorem

: IsCoatom a ↔ a ≠ ⊤ ∧ ∀ b ≠ ⊤, a ≤ b → b ≤ a

Full source

theorem isCoatom_iff_ge_of_le : IsCoatomIsCoatom a ↔ a ≠ ⊤ ∧ ∀ b ≠ ⊤, a ≤ b → b ≤ a :=
  isAtom_iff_le_of_ge (α := αᵒᵈ)

Characterization of Coatoms in an Order with Top Element

Informal description

An element $a$ in an order with a top element $\top$ is a coatom if and only if $a \neq \top$ and for every element $b \neq \top$, if $a \leq b$ then $b \leq a$.

IsCoatom.lt_iff theorem

(h : IsCoatom a) : a < x ↔ x = ⊤

Full source

theorem IsCoatom.lt_iff (h : IsCoatom a) : a < x ↔ x = ⊤ :=
  h.dual.lt_iff

Characterization of Elements Above a Coatom

Informal description

Let $a$ be a coatom in an ordered set with top element $\top$. Then for any element $x$, we have $a < x$ if and only if $x = \top$.

IsCoatom.le_iff theorem

(h : IsCoatom a) : a ≤ x ↔ x = ⊤ ∨ x = a

Full source

theorem IsCoatom.le_iff (h : IsCoatom a) : a ≤ x ↔ x = ⊤ ∨ x = a :=
  h.dual.le_iff

Characterization of Elements Above or Equal to a Coatom

Informal description

Let $a$ be a coatom in an ordered set with a top element $\top$. For any element $x$, we have $a \leq x$ if and only if $x = \top$ or $x = a$.

IsCoatom.lt_top theorem

(h : IsCoatom a) : a < ⊤

Full source

lemma IsCoatom.lt_top (h : IsCoatom a) : a < ⊤ :=
  h.lt_iff.mpr rfl

Coatom is Strictly Below Top Element

Informal description

For any coatom $a$ in an ordered set with a top element $\top$, we have $a < \top$.

IsCoatom.le_iff_eq theorem

(ha : IsCoatom a) (hb : b ≠ ⊤) : a ≤ b ↔ b = a

Full source

lemma IsCoatom.le_iff_eq (ha : IsCoatom a) (hb : b ≠ ⊤) : a ≤ b ↔ b = a := ha.dual.le_iff_eq hb

Characterization of Non-Top Elements Above a Coatom: $a \leq b \leftrightarrow b = a$

Informal description

Let $a$ be a coatom in an ordered set with a top element $\top$, and let $b$ be an element such that $b \neq \top$. Then $a \leq b$ if and only if $b = a$.

IsCoatom.Ici_eq theorem

(h : IsCoatom a) : Set.Ici a = {⊤, a}

Full source

theorem IsCoatom.Ici_eq (h : IsCoatom a) : Set.Ici a = {⊤, a} :=
  h.dual.Iic_eq

Characterization of the Upper Set of a Coatom: $\text{Ici}(a) = \{\top, a\}$

Informal description

Let $a$ be a coatom in an ordered set with a top element $\top$. Then the set of all elements greater than or equal to $a$ is exactly $\{\top, a\}$, i.e., $\{x \mid a \leq x\} = \{\top, a\}$.

covBy_top_iff theorem

: a ⋖ ⊤ ↔ IsCoatom a

Full source

@[simp]
theorem covBy_top_iff : a ⋖ ⊤a ⋖ ⊤ ↔ IsCoatom a :=
  toDual_covBy_toDual_iff.symm.trans bot_covBy_iff

Cover Relation Characterizes Coatoms: $a \lessdot \top \leftrightarrow \text{IsCoatom}(a)$

Informal description

For an element $a$ in an order with a top element $\top$, the relation $a \lessdot \top$ (read as "$a$ is covered by $\top$") holds if and only if $a$ is a coatom. That is, $a \neq \top$ and there is no element strictly between $a$ and $\top$.

SetLike.isAtom_iff theorem

[OrderBot A] {K : A} : IsAtom K ↔ K ≠ ⊥ ∧ ∀ H g, H ≤ K → g ∉ H → g ∈ K → H = ⊥

Full source

theorem isAtom_iff [OrderBot A] {K : A} :
    IsAtomIsAtom K ↔ K ≠ ⊥ ∧ ∀ H g, H ≤ K → g ∉ H → g ∈ K → H = ⊥ := by
  simp_rw [IsAtom, lt_iff_le_not_le, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Characterization of Atoms in Set-like Structures: $K$ is an atom $\leftrightarrow$ $K \neq \bot$ and minimality condition holds

Informal description

Let $A$ be a set-like structure with a bottom element $\bot$. For an element $K \in A$, $K$ is an atom if and only if $K \neq \bot$ and for any subset $H \leq K$ and any element $g \in K \setminus H$, if $g \in K$ then $H = \bot$.

SetLike.isCoatom_iff theorem

[OrderTop A] {K : A} : IsCoatom K ↔ K ≠ ⊤ ∧ ∀ H g, K ≤ H → g ∉ K → g ∈ H → H = ⊤

Full source

theorem isCoatom_iff [OrderTop A] {K : A} :
    IsCoatomIsCoatom K ↔ K ≠ ⊤ ∧ ∀ H g, K ≤ H → g ∉ K → g ∈ H → H = ⊤ := by
  simp_rw [IsCoatom, lt_iff_le_not_le, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Characterization of Coatoms in Set-like Structures

Informal description

Let $A$ be a set-like structure with a top element $\top$ and a partial order $\leq$. An element $K \in A$ is a coatom if and only if $K \neq \top$ and for any element $H \in A$ and any $g \in B$ (where $B$ is the base type of elements in $A$), if $K \leq H$, $g \notin K$, and $g \in H$, then $H = \top$.

SetLike.covBy_iff theorem

{K L : A} : K ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Full source

theorem covBy_iff {K L : A} :
    K ⋖ LK ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L := by
  refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_
  push_neg
  rw [lt_iff_le_not_le, lt_iff_le_and_ne, and_and_and_comm]
  simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]

Covering Relation Characterization in Set-like Structures: $K \mathrel{\text{⋖}} L$ iff $K < L$ and any intermediate $H$ containing a new element $g$ must equal $L$

Informal description

Let $A$ be a set-like structure with a partial order and elements of type $B$. For any elements $K, L \in A$, the relation $K \mathrel{\text{⋖}} L$ (read as "$K$ is covered by $L$") holds if and only if: 1. $K < L$, and 2. For any element $H \in A$ and $g \in B$, if $K \leq H \leq L$, $g \notin K$, and $g \in H$, then $H = L$.

SetLike.covBy_iff' theorem

{K L : A} : K ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Full source

/-- Dual variant of `SetLike.covBy_iff` -/
theorem covBy_iff' {K L : A} :
    K ⋖ LK ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K := by
  refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_
  push_neg
  rw [lt_iff_le_and_ne, lt_iff_le_not_le, and_and_and_comm]
  simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]

Covering Relation Characterization in Set-like Structures

Informal description

For any two elements $K$ and $L$ in a set-like structure $A$ with a partial order, the relation $K \mathrel{\text{⋖}} L$ (read as "$K$ is covered by $L$") holds if and only if: 1. $K < L$, and 2. For any element $H$ such that $K \leq H \leq L$ and any element $g \notin H$ but $g \in L$, it follows that $H = K$. Here, $K \mathrel{\text{⋖}} L$ means that $K$ is strictly less than $L$ and there is no element strictly between them in the order.

iInf_le_coatom theorem

[Order.Coframe α] {a : α} (ha : IsCoatom a) {f : ι → α} : iInf f ≤ a ↔ ∃ i, f i ≤ a

Full source

theorem iInf_le_coatom [Order.Coframe α] {a : α} (ha : IsCoatom a) {f : ι → α} :
    iInfiInf f ≤ a ↔ ∃ i, f i ≤ a :=
  atom_le_iSup (α := αᵒᵈ) ha

Infimum is Below Coatom if and only if Some Element in the Family is Below Coatom

Informal description

Let $\alpha$ be a coframe (complete lattice with infinite distributive laws) and let $a \in \alpha$ be a coatom. For any family of elements $(f_i)_{i \in \iota}$ in $\alpha$, the infimum $\bigsqcap_{i \in \iota} f_i$ is less than or equal to the coatom $a$ if and only if there exists some index $i \in \iota$ such that $f_i \leq a$.

Set.Ici.isAtom_iff theorem

{b : Set.Ici a} : IsAtom b ↔ a ⋖ b

Full source

@[simp]
theorem Set.Ici.isAtom_iff {b : Set.Ici a} : IsAtomIsAtom b ↔ a ⋖ b := by
  rw [← bot_covBy_iff]
  refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm
  simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Ici

Atom Characterization in Upper Closure: $b$ is an atom in $[a, \infty) \leftrightarrow a \lessdot b$

Informal description

For an element $b$ in the upper closure $[a, \infty)$ of a preorder, $b$ is an atom in $[a, \infty)$ if and only if $a$ is covered by $b$ (i.e., $a \lessdot b$). Here, an atom in $[a, \infty)$ is a minimal non-bottom element, meaning $b \neq a$ and there is no element strictly between $a$ and $b$.

Set.Iic.isCoatom_iff theorem

{a : Set.Iic b} : IsCoatom a ↔ ↑a ⋖ b

Full source

@[simp]
theorem Set.Iic.isCoatom_iff {a : Set.Iic b} : IsCoatomIsCoatom a ↔ ↑a ⋖ b := by
  rw [← covBy_top_iff]
  refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm
  simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Iic

Coatom Characterization in Lower Closure: $a$ is a coatom in $(-\infty, b] \leftrightarrow a \lessdot b$

Informal description

For an element $a$ in the lower closure $(-\infty, b]$ of a preorder, $a$ is a coatom in $(-\infty, b]$ if and only if $a$ is covered by $b$ (i.e., $a \lessdot b$). Here, a coatom in $(-\infty, b]$ is a maximal non-top element, meaning $a \neq b$ and there is no element strictly between $a$ and $b$.

covBy_iff_atom_Ici theorem

(h : a ≤ b) : a ⋖ b ↔ IsAtom (⟨b, h⟩ : Set.Ici a)

Full source

theorem covBy_iff_atom_Ici (h : a ≤ b) : a ⋖ ba ⋖ b ↔ IsAtom (⟨b, h⟩ : Set.Ici a) := by simp

Covering Relation in Interval $[a, \infty)$ is Equivalent to Atom Condition

Informal description

For any elements $a$ and $b$ in a preorder with $a \leq b$, the relation $a \lessdot b$ (i.e., $a$ is covered by $b$) holds if and only if the element $\langle b, h \rangle$ is an atom in the interval $[a, \infty)$, where $\langle b, h \rangle$ denotes the element $b$ viewed as a member of the interval $[a, \infty)$.

covBy_iff_coatom_Iic theorem

(h : a ≤ b) : a ⋖ b ↔ IsCoatom (⟨a, h⟩ : Set.Iic b)

Full source

theorem covBy_iff_coatom_Iic (h : a ≤ b) : a ⋖ ba ⋖ b ↔ IsCoatom (⟨a, h⟩ : Set.Iic b) := by simp

Covering Relation in Interval $(-\infty, b]$ is Equivalent to Coatom Condition

Informal description

For any elements $a$ and $b$ in a preorder with $a \leq b$, the relation $a \lessdot b$ (i.e., $a$ is covered by $b$) holds if and only if the element $\langle a, h \rangle$ is a coatom in the interval $(-\infty, b]$, where $\langle a, h \rangle$ denotes the element $a$ viewed as a member of the interval $(-\infty, b]$.

IsAtom.inf_eq_bot_of_ne theorem

[SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) : a ⊓ b = ⊥

Full source

theorem IsAtom.inf_eq_bot_of_ne [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a)
    (hb : IsAtom b) (hab : a ≠ b) : a ⊓ b = ⊥ :=
  hab.not_le_or_not_le.elim (ha.lt_iff.1 ∘ inf_lt_left.2) (hb.lt_iff.1 ∘ inf_lt_right.2)

Meet of Distinct Atoms is Bottom

Informal description

Let $\alpha$ be a meet-semilattice with a bottom element $\bot$, and let $a$ and $b$ be atoms in $\alpha$ such that $a \neq b$. Then the meet of $a$ and $b$ is equal to $\bot$, i.e., $a \sqcap b = \bot$.

IsAtom.disjoint_of_ne theorem

[SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) : Disjoint a b

Full source

theorem IsAtom.disjoint_of_ne [SemilatticeInf α] [OrderBot α] {a b : α} (ha : IsAtom a)
    (hb : IsAtom b) (hab : a ≠ b) : Disjoint a b :=
  disjoint_iff.mpr (ha.inf_eq_bot_of_ne hb hab)

Disjointness of Distinct Atoms in a Meet-Semilattice

Informal description

Let $\alpha$ be a meet-semilattice with a bottom element $\bot$, and let $a$ and $b$ be atoms in $\alpha$ such that $a \neq b$. Then $a$ and $b$ are disjoint, i.e., $a \sqcap b = \bot$.

IsCoatom.sup_eq_top_of_ne theorem

[SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) : a ⊔ b = ⊤

Full source

theorem IsCoatom.sup_eq_top_of_ne [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a)
    (hb : IsCoatom b) (hab : a ≠ b) : a ⊔ b = ⊤ :=
  ha.dual.inf_eq_bot_of_ne hb.dual hab

Join of Distinct Coatoms is Top

Informal description

Let $\alpha$ be a join-semilattice with a top element $\top$, and let $a$ and $b$ be coatoms in $\alpha$ such that $a \neq b$. Then the join of $a$ and $b$ is equal to $\top$, i.e., $a \sqcup b = \top$.

IsCoatom.codisjoint_of_ne theorem

[SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) : Codisjoint a b

Full source

theorem IsCoatom.codisjoint_of_ne [SemilatticeSup α] [OrderTop α] {a b : α} (ha : IsCoatom a)
    (hb : IsCoatom b) (hab : a ≠ b) : Codisjoint a b :=
  codisjoint_iff.mpr (ha.sup_eq_top_of_ne hb hab)

Codisjointness of Distinct Coatoms in a Join-Semilattice

Informal description

Let $\alpha$ be a join-semilattice with a top element $\top$, and let $a$ and $b$ be coatoms in $\alpha$ such that $a \neq b$. Then $a$ and $b$ are codisjoint, i.e., $a \sqcup b = \top$.

IsAtomic structure

[OrderBot α]

Full source

/-- A lattice is atomic iff every element other than `⊥` has an atom below it. -/
@[mk_iff]
class IsAtomic [OrderBot α] : Prop where
  /-- Every element other than `⊥` has an atom below it. -/
  eq_bot_or_exists_atom_le : ∀ b : α, b = ⊥ ∨ ∃ a : α, IsAtom a ∧ a ≤ b

Atomic Lattice

Informal description

A lattice with a bottom element $\bot$ is called *atomic* if every element $x \neq \bot$ has an atom below it, i.e., there exists an atom $a$ such that $a \leq x$.

IsCoatomic structure

[OrderTop α]

Full source

/-- A lattice is coatomic iff every element other than `⊤` has a coatom above it. -/
@[mk_iff]
class IsCoatomic [OrderTop α] : Prop where
  /-- Every element other than `⊤` has an atom above it. -/
  eq_top_or_exists_le_coatom : ∀ b : α, b = ⊤ ∨ ∃ a : α, IsCoatom a ∧ b ≤ a

Coatomic lattice

Informal description

A lattice $\alpha$ with a top element $\top$ is called *coatomic* if every element $x \neq \top$ has a coatom above it, where a coatom is an element covered by $\top$ (i.e., the only element strictly above it is $\top$).

IsAtomic.exists_atom theorem

[OrderBot α] [Nontrivial α] [IsAtomic α] : ∃ a : α, IsAtom a

Full source

lemma IsAtomic.exists_atom [OrderBot α] [Nontrivial α] [IsAtomic α] : ∃ a : α, IsAtom a :=
  have ⟨b, hb⟩ := exists_ne (⊥ : α)
  have ⟨a, ha⟩ := (eq_bot_or_exists_atom_le b).resolve_left hb
  ⟨a, ha.1⟩

Existence of Atoms in Nontrivial Atomic Lattices

Informal description

In any nontrivial atomic lattice $\alpha$ with a bottom element $\bot$, there exists an atom $a \in \alpha$.

IsCoatomic.exists_coatom theorem

[OrderTop α] [Nontrivial α] [IsCoatomic α] : ∃ a : α, IsCoatom a

Full source

lemma IsCoatomic.exists_coatom [OrderTop α] [Nontrivial α] [IsCoatomic α] : ∃ a : α, IsCoatom a :=
  have ⟨b, hb⟩ := exists_ne (⊤ : α)
  have ⟨a, ha⟩ := (eq_top_or_exists_le_coatom b).resolve_left hb
  ⟨a, ha.1⟩

Existence of a Coatom in a Nontrivial Coatomic Lattice

Informal description

In a nontrivial lattice $\alpha$ with a top element $\top$ that is coatomic, there exists a coatom $a \in \alpha$, i.e., an element $a \neq \top$ such that for any $b \in \alpha$, if $a < b$ then $b = \top$.

isCoatomic_dual_iff_isAtomic theorem

[OrderBot α] : IsCoatomic αᵒᵈ ↔ IsAtomic α

Full source

@[simp]
theorem isCoatomic_dual_iff_isAtomic [OrderBot α] : IsCoatomicIsCoatomic αᵒᵈ ↔ IsAtomic α :=
  ⟨fun h => ⟨fun b => by apply h.eq_top_or_exists_le_coatom⟩, fun h =>
    ⟨fun b => by apply h.eq_bot_or_exists_atom_le⟩⟩

Duality between atomic and coatomic lattices: $\alpha^{\text{op}}$ coatomic $\iff$ $\alpha$ atomic

Informal description

For any partially ordered set $\alpha$ with a least element $\bot$, the order dual $\alpha^{\text{op}}$ is coatomic if and only if $\alpha$ is atomic. Here: - An *atomic* lattice means every element $x \neq \bot$ has an atom below it. - A *coatomic* lattice means every element $x \neq \top$ has a coatom above it. - The *order dual* $\alpha^{\text{op}}$ reverses the order relation of $\alpha$.

isAtomic_dual_iff_isCoatomic theorem

[OrderTop α] : IsAtomic αᵒᵈ ↔ IsCoatomic α

Full source

@[simp]
theorem isAtomic_dual_iff_isCoatomic [OrderTop α] : IsAtomicIsAtomic αᵒᵈ ↔ IsCoatomic α :=
  ⟨fun h => ⟨fun b => by apply h.eq_bot_or_exists_atom_le⟩, fun h =>
    ⟨fun b => by apply h.eq_top_or_exists_le_coatom⟩⟩

Duality between atomic and coatomic lattices: $\alpha^{\text{op}}$ atomic $\iff$ $\alpha$ coatomic

Informal description

For any partially ordered set $\alpha$ with a greatest element $\top$, the order dual $\alpha^{\text{op}}$ is atomic if and only if $\alpha$ is coatomic. Here: - An *atomic* lattice means every element $x \neq \bot$ has an atom below it. - A *coatomic* lattice means every element $x \neq \top$ has a coatom above it. - The *order dual* $\alpha^{\text{op}}$ reverses the order relation of $\alpha$.

OrderDual.instIsCoatomic instance

: IsCoatomic αᵒᵈ

Full source

instance _root_.OrderDual.instIsCoatomic : IsCoatomic αᵒᵈ :=
  isCoatomic_dual_iff_isAtomic.2 ‹IsAtomic α›

Order Dual of a Coatomic Lattice is Coatomic

Informal description

For any partially ordered set $\alpha$ with a greatest element $\top$, the order dual $\alpha^{\text{op}}$ is coatomic. That is, every element $x \neq \bot$ in $\alpha^{\text{op}}$ has a coatom above it.

IsAtomic.Set.Iic.isAtomic instance

{x : α} : IsAtomic (Set.Iic x)

Full source

instance Set.Iic.isAtomic {x : α} : IsAtomic (Set.Iic x) :=
  ⟨fun ⟨y, hy⟩ =>
    (eq_bot_or_exists_atom_le y).imp Subtype.mk_eq_mk.2 fun ⟨a, ha, hay⟩ =>
      ⟨⟨a, hay.trans hy⟩, ha.Iic (hay.trans hy), hay⟩⟩

Atomicity of Intervals in Atomic Lattices

Informal description

For any element $x$ in a partially ordered set $\alpha$ with a bottom element $\bot$, the interval $(-\infty, x]$ is an atomic lattice. That is, every element $y \leq x$ with $y \neq \bot$ has an atom below it in the interval.

OrderDual.instIsAtomic instance

: IsAtomic αᵒᵈ

Full source

instance _root_.OrderDual.instIsAtomic : IsAtomic αᵒᵈ :=
  isAtomic_dual_iff_isCoatomic.2 ‹IsCoatomic α›

Atomicity of Order Dual Lattices

Informal description

The order dual $\alpha^{\text{op}}$ of an atomic lattice $\alpha$ is also atomic.

IsCoatomic.Set.Ici.isCoatomic instance

{x : α} : IsCoatomic (Set.Ici x)

Full source

instance Set.Ici.isCoatomic {x : α} : IsCoatomic (Set.Ici x) :=
  ⟨fun ⟨y, hy⟩ =>
    (eq_top_or_exists_le_coatom y).imp Subtype.mk_eq_mk.2 fun ⟨a, ha, hay⟩ =>
      ⟨⟨a, le_trans hy hay⟩, ha.Ici (le_trans hy hay), hay⟩⟩

Coatomicity of Intervals in Coatomic Lattices

Informal description

For any element $x$ in a partially ordered set $\alpha$ with a top element $\top$, the interval $[x, \infty)$ is a coatomic lattice. That is, every element $y \geq x$ with $y \neq \top$ has a coatom above it in the interval.

isAtomic_iff_forall_isAtomic_Iic theorem

[OrderBot α] : IsAtomic α ↔ ∀ x : α, IsAtomic (Set.Iic x)

Full source

theorem isAtomic_iff_forall_isAtomic_Iic [OrderBot α] :
    IsAtomicIsAtomic α ↔ ∀ x : α, IsAtomic (Set.Iic x) :=
  ⟨@IsAtomic.Set.Iic.isAtomic _ _ _, fun h =>
    ⟨fun x =>
      ((@eq_bot_or_exists_atom_le _ _ _ (h x)) (⊤ : Set.Iic x)).imp Subtype.mk_eq_mk.1
        (Exists.imp' (↑) fun ⟨_, _⟩ => And.imp_left IsAtom.of_isAtom_coe_Iic)⟩⟩

Characterization of Atomic Lattices via Atomic Intervals

Informal description

A partially ordered set $\alpha$ with a bottom element $\bot$ is atomic if and only if for every element $x \in \alpha$, the interval $(-\infty, x]$ is atomic.

isCoatomic_iff_forall_isCoatomic_Ici theorem

[OrderTop α] : IsCoatomic α ↔ ∀ x : α, IsCoatomic (Set.Ici x)

Full source

theorem isCoatomic_iff_forall_isCoatomic_Ici [OrderTop α] :
    IsCoatomicIsCoatomic α ↔ ∀ x : α, IsCoatomic (Set.Ici x) :=
  isAtomic_dual_iff_isCoatomic.symm.trans <|
    isAtomic_iff_forall_isAtomic_Iic.trans <|
      forall_congr' fun _ => isCoatomic_dual_iff_isAtomic.symm.trans Iff.rfl

Characterization of Coatomic Lattices via Coatomic Intervals

Informal description

A partially ordered set $\alpha$ with a top element $\top$ is coatomic if and only if for every element $x \in \alpha$, the interval $[x, \infty)$ is coatomic.

IsStronglyAtomic structure

(α : Type*) [Preorder α]

Full source

/-- An order is strongly atomic if every nontrivial interval `[a, b]`
contains an element covering `a`. -/
@[mk_iff]
class IsStronglyAtomic (α : Type*) [Preorder α] : Prop where
  exists_covBy_le_of_lt : ∀ (a b : α), a < b → ∃ x, a ⋖ x ∧ x ≤ b

Strongly Atomic Order

Informal description

An order $\alpha$ is called *strongly atomic* if for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a$ is covered by $x$ (i.e., $a \lessdot x$) and $x \leq b$. This means that in any nontrivial interval $[a, b]$, there is an element that covers $a$.

exists_covBy_le_of_lt theorem

[IsStronglyAtomic α] (h : a < b) : ∃ x, a ⋖ x ∧ x ≤ b

Full source

theorem exists_covBy_le_of_lt [IsStronglyAtomic α] (h : a < b) : ∃ x, a ⋖ x ∧ x ≤ b :=
  IsStronglyAtomic.exists_covBy_le_of_lt a b h

Existence of Covering Element in Strongly Atomic Order

Informal description

Let $\alpha$ be a strongly atomic order. For any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a$ is covered by $x$ (i.e., $a \lessdot x$) and $x \leq b$.

IsStronglyCoatomic structure

(α : Type*) [Preorder α]

Full source

/-- An order is strongly coatomic if every nontrivial interval `[a, b]`
contains an element covered by `b`. -/
@[mk_iff]
class IsStronglyCoatomic (α : Type*) [Preorder α] : Prop where
  (exists_le_covBy_of_lt : ∀ (a b : α), a < b → ∃ x, a ≤ x ∧ x ⋖ b)

Strongly coatomic order

Informal description

An order $\alpha$ is called *strongly coatomic* if for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$ (i.e., there is no element strictly between $x$ and $b$).

exists_le_covBy_of_lt theorem

[IsStronglyCoatomic α] (h : a < b) : ∃ x, a ≤ x ∧ x ⋖ b

Full source

theorem exists_le_covBy_of_lt [IsStronglyCoatomic α] (h : a < b) : ∃ x, a ≤ x ∧ x ⋖ b :=
  IsStronglyCoatomic.exists_le_covBy_of_lt a b h

Existence of Covering Element in Strongly Catomic Order

Informal description

Let $\alpha$ be a strongly coatomic order. For any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$ (i.e., $x \lessdot b$).

isStronglyAtomic_dual_iff_is_stronglyCoatomic theorem

: IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α

Full source

theorem isStronglyAtomic_dual_iff_is_stronglyCoatomic :
    IsStronglyAtomicIsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α := by
  simpa [isStronglyAtomic_iff, OrderDual.exists, OrderDual.forall,
    OrderDual.toDual_le_toDual, and_comm, isStronglyCoatomic_iff] using forall_comm

Duality between Strongly Atomic and Strongly Catomic Orders: $\text{IsStronglyAtomic}(\alpha^{\text{op}}) \leftrightarrow \text{IsStronglyCoatomic}(\alpha)$

Informal description

For any preorder $\alpha$, the order dual $\alpha^{\text{op}}$ is strongly atomic if and only if $\alpha$ is strongly coatomic.

isStronglyCoatomic_dual_iff_is_stronglyAtomic theorem

: IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

Full source

@[simp] theorem isStronglyCoatomic_dual_iff_is_stronglyAtomic :
    IsStronglyCoatomicIsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α := by
  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; rfl

Duality between Strongly Catomic and Strongly Atomic Orders: $\text{IsStronglyCoatomic}(\alpha^{\text{op}}) \leftrightarrow \text{IsStronglyAtomic}(\alpha)$

Informal description

For any preorder $\alpha$, the order dual $\alpha^{\text{op}}$ is strongly coatomic if and only if $\alpha$ is strongly atomic.

OrderDual.instIsStronglyCoatomic instance

[IsStronglyAtomic α] : IsStronglyCoatomic αᵒᵈ

Full source

instance OrderDual.instIsStronglyCoatomic [IsStronglyAtomic α] : IsStronglyCoatomic αᵒᵈ := by
  rwa [isStronglyCoatomic_dual_iff_is_stronglyAtomic]

Strongly Coatomic Order Dual of a Strongly Atomic Order

Informal description

For any preorder $\alpha$, if $\alpha$ is strongly atomic, then its order dual $\alpha^{\text{op}}$ is strongly coatomic.

instIsStronglyAtomicOrderDualOfIsStronglyCoatomic instance

[IsStronglyCoatomic α] : IsStronglyAtomic αᵒᵈ

Full source

instance [IsStronglyCoatomic α] : IsStronglyAtomic αᵒᵈ := by
  rwa [isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Strongly Atomic Order Dual of a Strongly Catomic Order

Informal description

For any preorder $\alpha$, if $\alpha$ is strongly coatomic, then its order dual $\alpha^{\text{op}}$ is strongly atomic.

IsStronglyAtomic.isAtomic instance

(α : Type*) [PartialOrder α] [OrderBot α] [IsStronglyAtomic α] : IsAtomic α

Full source

instance IsStronglyAtomic.isAtomic (α : Type*) [PartialOrder α] [OrderBot α] [IsStronglyAtomic α] :
    IsAtomic α where
  eq_bot_or_exists_atom_le a := by
    rw [or_iff_not_imp_left, ← Ne, ← bot_lt_iff_ne_bot]
    refine fun hlt ↦ ?_
    obtain ⟨x, hx, hxa⟩ := hlt.exists_covby_le
    exact ⟨x, bot_covBy_iff.1 hx, hxa⟩

Strongly Atomic Implies Atomic

Informal description

Every strongly atomic partial order with a bottom element is atomic. That is, if for every pair of elements $a < b$ there exists an element $x$ such that $a$ is covered by $x$ and $x \leq b$, then every non-bottom element has an atom below it.

IsStronglyCoatomic.toIsCoatomic instance

(α : Type*) [PartialOrder α] [OrderTop α] [IsStronglyCoatomic α] : IsCoatomic α

Full source

instance IsStronglyCoatomic.toIsCoatomic (α : Type*) [PartialOrder α] [OrderTop α]
    [IsStronglyCoatomic α] : IsCoatomic α :=
  isAtomic_dual_iff_isCoatomic.1 <| IsStronglyAtomic.isAtomic (α := αᵒᵈ)

Strongly Coatomic Implies Coatomic

Informal description

For any partially ordered set $\alpha$ with a greatest element $\top$, if $\alpha$ is strongly coatomic, then it is also coatomic. That is, if for every pair of elements $a < b$ in $\alpha$ there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$, then every element $x \neq \top$ has a coatom above it.

Set.OrdConnected.isStronglyAtomic theorem

[IsStronglyAtomic α] {s : Set α} (h : Set.OrdConnected s) : IsStronglyAtomic s

Full source

theorem Set.OrdConnected.isStronglyAtomic [IsStronglyAtomic α] {s : Set α}
    (h : Set.OrdConnected s) : IsStronglyAtomic s where
  exists_covBy_le_of_lt := by
    rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd
    obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le
    exact ⟨⟨x, h.out' hc hd ⟨hcx.le, hxd⟩⟩,
      ⟨by simpa using hcx.lt, fun y hy hy' ↦ hcx.2 (by simpa using hy) (by simpa using hy')⟩, hxd⟩

Order Connected Subsets Inherit Strong Atomicity

Informal description

Let $\alpha$ be a strongly atomic preorder and let $s$ be an order connected subset of $\alpha$. Then $s$ is also strongly atomic.

Set.OrdConnected.isStronglyCoatomic theorem

[IsStronglyCoatomic α] {s : Set α} (h : Set.OrdConnected s) : IsStronglyCoatomic s

Full source

theorem Set.OrdConnected.isStronglyCoatomic [IsStronglyCoatomic α] {s : Set α}
    (h : Set.OrdConnected s) : IsStronglyCoatomic s :=
  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 h.dual.isStronglyAtomic

Strongly coatomic property for order-connected subsets

Informal description

Let $\alpha$ be a preorder that is strongly coatomic, and let $s$ be an order-connected subset of $\alpha$. Then $s$ is also strongly coatomic, meaning that for any two elements $a < b$ in $s$, there exists an element $x \in s$ such that $a \leq x$ and $x$ is covered by $b$ (i.e., there is no element strictly between $x$ and $b$ in $s$).

instIsStronglyAtomicElemOfOrdConnected instance

[IsStronglyAtomic α] {s : Set α} [Set.OrdConnected s] : IsStronglyAtomic s

Full source

instance [IsStronglyAtomic α] {s : Set α} [Set.OrdConnected s] : IsStronglyAtomic s :=
  Set.OrdConnected.isStronglyAtomic <| by assumption

Strong Atomicity of Order-Connected Subsets

Informal description

For any strongly atomic preorder $\alpha$ and any order-connected subset $s$ of $\alpha$, the subset $s$ is also strongly atomic.

instIsStronglyCoatomicElemOfOrdConnected instance

[IsStronglyCoatomic α] {s : Set α} [h : Set.OrdConnected s] : IsStronglyCoatomic s

Full source

instance [IsStronglyCoatomic α] {s : Set α} [h : Set.OrdConnected s] : IsStronglyCoatomic s :=
  Set.OrdConnected.isStronglyCoatomic <| by assumption

Strongly Coatomic Property for Order-Connected Subsets

Informal description

For any strongly coatomic preorder $\alpha$ and any order-connected subset $s$ of $\alpha$, the subset $s$ is also strongly coatomic.

SuccOrder.toIsStronglyAtomic instance

[SuccOrder α] : IsStronglyAtomic α

Full source

instance SuccOrder.toIsStronglyAtomic [SuccOrder α] : IsStronglyAtomic α where
  exists_covBy_le_of_lt a _ hab :=
    ⟨SuccOrder.succ a, Order.covBy_succ_of_not_isMax fun ha ↦ ha.not_lt hab,
      SuccOrder.succ_le_of_lt hab⟩

Successor Orders are Strongly Atomic

Informal description

Every order $\alpha$ equipped with a successor function is strongly atomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a$ is covered by $x$ (denoted $a \lessdot x$) and $x \leq b$.

instIsStronglyCoatomicOfPredOrder instance

[PredOrder α] : IsStronglyCoatomic α

Full source

instance [PredOrder α] : IsStronglyCoatomic α := by
  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; infer_instance

Predecessor Orders are Strongly Coatomic

Informal description

For any preorder $\alpha$ equipped with a predecessor order structure, $\alpha$ is strongly coatomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$ (i.e., there is no element strictly between $x$ and $b$).

IsStronglyAtomic.of_wellFounded_lt theorem

(h : WellFounded ((· < ·) : α → α → Prop)) : IsStronglyAtomic α

Full source

theorem IsStronglyAtomic.of_wellFounded_lt (h : WellFounded ((· < ·) : α → α → Prop)) :
    IsStronglyAtomic α where
  exists_covBy_le_of_lt a b hab := by
    refine ⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab,rfl.le⟩, ?_⟩
    have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab,rfl.le⟩)
    exact ⟨⟨hmem.1,fun c hac hlt ↦ WellFounded.not_lt_min h
      (Set.Ioc a b) ⟨b, hab,rfl.le⟩ ⟨hac, hlt.le.trans hmem.2⟩ hlt ⟩, hmem.2⟩

Well-founded strict order implies strongly atomic order

Informal description

If a preorder $\alpha$ has a well-founded strict less-than relation $<$, then $\alpha$ is strongly atomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a$ is covered by $x$ (denoted $a \lessdot x$) and $x \leq b$.

IsStronglyCoatomic.of_wellFounded_gt theorem

(h : WellFounded ((· > ·) : α → α → Prop)) : IsStronglyCoatomic α

Full source

theorem IsStronglyCoatomic.of_wellFounded_gt (h : WellFounded ((· > ·) : α → α → Prop)) :
    IsStronglyCoatomic α :=
  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 <| IsStronglyAtomic.of_wellFounded_lt (α := αᵒᵈ) h

Well-founded $>$ implies strongly coatomic order

Informal description

For any preorder $\alpha$, if the strict greater-than relation $>$ on $\alpha$ is well-founded, then $\alpha$ is strongly coatomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$ (i.e., there is no element strictly between $x$ and $b$).

instIsStronglyAtomicOfWellFoundedLT instance

[WellFoundedLT α] : IsStronglyAtomic α

Full source

instance [WellFoundedLT α] : IsStronglyAtomic α :=
  IsStronglyAtomic.of_wellFounded_lt wellFounded_lt

Well-founded Strict Orders are Strongly Atomic

Informal description

Every preorder $\alpha$ with a well-founded strict less-than relation $<$ is strongly atomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a$ is covered by $x$ (denoted $a \lessdot x$) and $x \leq b$.

instIsStronglyCoatomicOfWellFoundedGT instance

[WellFoundedGT α] : IsStronglyCoatomic α

Full source

instance [WellFoundedGT α] : IsStronglyCoatomic α :=
    IsStronglyCoatomic.of_wellFounded_gt wellFounded_gt

Well-founded "greater than" implies strongly coatomic order

Informal description

Every preorder $\alpha$ with a well-founded "greater than" relation is strongly coatomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$ (i.e., there is no element strictly between $x$ and $b$).

isAtomic_of_orderBot_wellFounded_lt theorem

[OrderBot α] (h : WellFounded ((· < ·) : α → α → Prop)) : IsAtomic α

Full source

theorem isAtomic_of_orderBot_wellFounded_lt [OrderBot α]
    (h : WellFounded ((· < ·) : α → α → Prop)) : IsAtomic α :=
  (IsStronglyAtomic.of_wellFounded_lt h).isAtomic

Well-founded strict order implies atomic lattice

Informal description

Let $\alpha$ be a partially ordered set with a bottom element $\bot$. If the strict order relation $<$ on $\alpha$ is well-founded, then $\alpha$ is atomic. That is, every element $x \neq \bot$ has an atom below it.

isCoatomic_of_orderTop_gt_wellFounded theorem

[OrderTop α] (h : WellFounded ((· > ·) : α → α → Prop)) : IsCoatomic α

Full source

theorem isCoatomic_of_orderTop_gt_wellFounded [OrderTop α]
    (h : WellFounded ((· > ·) : α → α → Prop)) : IsCoatomic α :=
  isAtomic_dual_iff_isCoatomic.1 (@isAtomic_of_orderBot_wellFounded_lt αᵒᵈ _ _ h)

Well-founded strict greater-than relation implies coatomic lattice

Informal description

Let $\alpha$ be a partially ordered set with a top element $\top$. If the strict order relation $>$ on $\alpha$ is well-founded, then $\alpha$ is coatomic. That is, every element $x \neq \top$ has a coatom above it.

BooleanAlgebra.le_iff_atom_le_imp theorem

{α} [BooleanAlgebra α] [IsAtomic α] {x y : α} : x ≤ y ↔ ∀ a, IsAtom a → a ≤ x → a ≤ y

Full source

theorem le_iff_atom_le_imp {α} [BooleanAlgebra α] [IsAtomic α] {x y : α} :
    x ≤ y ↔ ∀ a, IsAtom a → a ≤ x → a ≤ y := by
  refine ⟨fun h a _ => (le_trans · h), fun h => ?_⟩
  have : x ⊓ yᶜ = ⊥ := of_not_not fun hbot =>
    have ⟨a, ha, hle⟩ := (eq_bot_or_exists_atom_le _).resolve_left hbot
    have ⟨hx, hy'⟩ := le_inf_iff.1 hle
    have hy := h a ha hx
    have : a ≤ y ⊓ yᶜ := le_inf_iff.2 ⟨hy, hy'⟩
    ha.1 (by simpa using this)
  exact (eq_compl_iff_isCompl.1 (by simp)).inf_right_eq_bot_iff.1 this

Characterization of Order in Atomic Boolean Algebras via Atoms

Informal description

Let $\alpha$ be an atomic Boolean algebra. For any elements $x, y \in \alpha$, $x$ is less than or equal to $y$ if and only if every atom $a$ in $\alpha$ that is less than or equal to $x$ is also less than or equal to $y$. In other words: $$x \leq y \leftrightarrow \forall a \text{ (atom) }, (a \leq x \rightarrow a \leq y).$$

CompleteBooleanAlgebra.toCompleteAtomicBooleanAlgebra abbrev

{α} [CompleteBooleanAlgebra α] [IsAtomic α] : CompleteAtomicBooleanAlgebra α

Full source

abbrev toCompleteAtomicBooleanAlgebra {α} [CompleteBooleanAlgebra α] [IsAtomic α] :
    CompleteAtomicBooleanAlgebra α where
  __ := ‹CompleteBooleanAlgebra α›
  iInf_iSup_eq f := BooleanAlgebra.eq_iff_atom_le_iff.2 fun a ha => by
    simp only [le_iInf_iff, atom_le_iSup ha]
    rw [Classical.skolem]

Atomic Complete Boolean Algebra is Complete Atomic Boolean Algebra

Informal description

For any complete Boolean algebra $\alpha$ that is also atomic, $\alpha$ is a complete atomic Boolean algebra.

IsAtomistic structure

[OrderBot α]

Full source

/-- A lattice is atomistic iff every element is a `sSup` of a set of atoms. -/
@[mk_iff]
class IsAtomistic [OrderBot α] : Prop where
  /-- Every element is a `sSup` of a set of atoms. -/
  isLUB_atoms : ∀ b : α, ∃ s : Set α, IsLUB s b ∧ ∀ a, a ∈ s → IsAtom a

Atomistic Lattice

Informal description

A lattice with a bottom element $\bot$ is called *atomistic* if every element is the supremum of a set of atoms, where an atom is a minimal non-$\bot$ element in the lattice.

IsCoatomistic structure

[OrderTop α]

Full source

/-- A lattice is coatomistic iff every element is an `sInf` of a set of coatoms. -/
@[mk_iff]
class IsCoatomistic [OrderTop α] : Prop where
  /-- Every element is a `sInf` of a set of coatoms. -/
  isGLB_coatoms : ∀ b : α, ∃ s : Set α, IsGLB s b ∧ ∀ a, a ∈ s → IsCoatom a

Coatomistic lattice

Informal description

A lattice with a top element $\top$ is called *coatomistic* if every element is the infimum of a set of coatoms (elements covered by $\top$).

isCoatomistic_dual_iff_isAtomistic theorem

[OrderBot α] : IsCoatomistic αᵒᵈ ↔ IsAtomistic α

Full source

@[simp]
theorem isCoatomistic_dual_iff_isAtomistic [OrderBot α] : IsCoatomisticIsCoatomistic αᵒᵈ ↔ IsAtomistic α :=
  ⟨fun h => ⟨fun b => by apply h.isGLB_coatoms⟩, fun h => ⟨fun b => by apply h.isLUB_atoms⟩⟩

Duality between Atomistic and Coatomistic Lattices: $\text{IsCoatomistic}(\alpha^{\text{op}}) \leftrightarrow \text{IsAtomistic}(\alpha)$

Informal description

For any lattice $\alpha$ with a bottom element $\bot$, the order dual $\alpha^{\text{op}}$ is coatomistic if and only if $\alpha$ is atomistic. Here, a lattice is *coatomistic* if every element is the infimum of a set of coatoms (elements covered by $\top$), and *atomistic* if every element is the supremum of a set of atoms (minimal non-$\bot$ elements).

isAtomistic_dual_iff_isCoatomistic theorem

[OrderTop α] : IsAtomistic αᵒᵈ ↔ IsCoatomistic α

Full source

@[simp]
theorem isAtomistic_dual_iff_isCoatomistic [OrderTop α] : IsAtomisticIsAtomistic αᵒᵈ ↔ IsCoatomistic α :=
  ⟨fun h => ⟨fun b => by apply h.isLUB_atoms⟩, fun h => ⟨fun b => by apply h.isGLB_coatoms⟩⟩

Duality between Atomistic and Coatomistic Lattices: $\alpha^{\text{op}}$ is Atomistic iff $\alpha$ is Coatomistic

Informal description

For a lattice $\alpha$ with a top element $\top$, the order dual $\alpha^{\text{op}}$ is atomistic if and only if $\alpha$ is coatomistic.

OrderDual.instIsCoatomistic instance

[OrderBot α] [h : IsAtomistic α] : IsCoatomistic αᵒᵈ

Full source

instance _root_.OrderDual.instIsCoatomistic [OrderBot α] [h : IsAtomistic α] : IsCoatomistic αᵒᵈ :=
  isCoatomistic_dual_iff_isAtomistic.2 h

Order Dual of an Atomistic Lattice is Coatomistic

Informal description

For any lattice $\alpha$ with a bottom element $\bot$ that is atomistic, the order dual $\alpha^{\text{op}}$ is coatomistic. Here, an atomistic lattice is one where every element is the supremum of a set of atoms (minimal non-$\bot$ elements), and a coatomistic lattice is one where every element is the infimum of a set of coatoms (elements covered by $\top$).

IsAtomistic.instIsAtomic instance

: IsAtomic α

Full source

instance (priority := 100) : IsAtomic α :=
  ⟨fun b => by
    rcases isLUB_atoms b with ⟨s, hsb, hs⟩
    rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
    · simp_all
    · exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩⟩

Atomistic Lattices are Atomic

Informal description

Every atomistic lattice is atomic. That is, if every element in a lattice with a bottom element $\bot$ is the supremum of a set of atoms, then every element $x \neq \bot$ has an atom below it.

isLUB_atoms_le theorem

(b : α) : IsLUB {a : α | IsAtom a ∧ a ≤ b} b

Full source

theorem isLUB_atoms_le (b : α) : IsLUB { a : α | IsAtom a ∧ a ≤ b } b := by
  rcases isLUB_atoms b with ⟨s, hsb, hs⟩
  exact ⟨fun c hc ↦ hc.2, fun c hc ↦ hsb.2 fun i hi ↦ hc ⟨hs _ hi, hsb.1 hi⟩⟩

Supremum of Atoms Below an Element

Informal description

For any element $b$ in a lattice $\alpha$ with a bottom element $\bot$, the set of all atoms $a$ such that $a \leq b$ has $b$ as its least upper bound. In other words, $b$ is the supremum of the set $\{a \in \alpha \mid \text{$a$ is an atom and } a \leq b\}$.

isLUB_atoms_top theorem

[OrderTop α] : IsLUB {a : α | IsAtom a} ⊤

Full source

theorem isLUB_atoms_top [OrderTop α] : IsLUB { a : α | IsAtom a } ⊤ := by
  simpa using isLUB_atoms_le (⊤ : α)

Supremum of All Atoms is the Top Element

Informal description

In a lattice $\alpha$ with a top element $\top$, the set of all atoms in $\alpha$ has $\top$ as its least upper bound. That is, $\top$ is the supremum of the set $\{a \in \alpha \mid \text{$a$ is an atom}\}$.

le_iff_atom_le_imp theorem

{a b : α} : a ≤ b ↔ ∀ c : α, IsAtom c → c ≤ a → c ≤ b

Full source

theorem le_iff_atom_le_imp {a b : α} : a ≤ b ↔ ∀ c : α, IsAtom c → c ≤ a → c ≤ b :=
  ⟨fun hab _ _ hca ↦ hca.trans hab,
   fun h ↦ (isLUB_atoms_le a).mono (isLUB_atoms_le b) fun _ ⟨h₁, h₂⟩ ↦ ⟨h₁, h _ h₁ h₂⟩⟩

Order Comparison via Atoms: $a \leq b$ iff All Atoms Below $a$ Are Below $b$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$ with a bottom element $\bot$, we have $a \leq b$ if and only if for every atom $c$ in $\alpha$, if $c \leq a$ then $c \leq b$.

OrderDual.instIsAtomistic instance

[h : IsCoatomistic α] : IsAtomistic αᵒᵈ

Full source

instance _root_.OrderDual.instIsAtomistic [h : IsCoatomistic α] : IsAtomistic αᵒᵈ :=
  isAtomistic_dual_iff_isCoatomistic.2 h

Order Dual of a Coatomistic Lattice is Atomistic

Informal description

For any lattice $\alpha$ that is coatomistic (i.e., every element is the infimum of a set of coatoms), the order dual $\alpha^{\text{op}}$ is atomistic (i.e., every element is the supremum of a set of atoms).

IsCoatomistic.instIsCoatomic instance

: IsCoatomic α

Full source

instance (priority := 100) : IsCoatomic α :=
  ⟨fun b => by
    rcases isGLB_coatoms b with ⟨s, hsb, hs⟩
    rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
    · simp_all
    · exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩⟩

Coatomistic Lattices are Coatomic

Informal description

Every coatomistic lattice is coatomic. That is, if every element in a lattice with a top element $\top$ can be expressed as the infimum of a set of coatoms (elements covered by $\top$), then the lattice is coatomic (every element $x \neq \top$ has a coatom above it).

sSup_atoms_le_eq theorem

{α} [CompleteLattice α] [IsAtomistic α] (b : α) : sSup {a : α | IsAtom a ∧ a ≤ b} = b

Full source

@[simp]
theorem sSup_atoms_le_eq {α} [CompleteLattice α] [IsAtomistic α] (b : α) :
    sSup { a : α | IsAtom a ∧ a ≤ b } = b :=
  (isLUB_atoms_le b).sSup_eq

Supremum of Atoms Below an Element in an Atomistic Lattice

Informal description

In a complete atomistic lattice $\alpha$, for any element $b \in \alpha$, the supremum of all atoms $a$ such that $a \leq b$ is equal to $b$. That is, \[ \bigvee \{a \in \alpha \mid \text{$a$ is an atom and } a \leq b\} = b. \]

sSup_atoms_eq_top theorem

{α} [CompleteLattice α] [IsAtomistic α] : sSup {a : α | IsAtom a} = ⊤

Full source

@[simp]
theorem sSup_atoms_eq_top {α} [CompleteLattice α] [IsAtomistic α] :
    sSup { a : α | IsAtom a } = ⊤ :=
  isLUB_atoms_top.sSup_eq

Supremum of All Atoms Equals Top in Atomistic Lattice

Informal description

In a complete atomistic lattice $\alpha$, the supremum of all atoms is equal to the top element $\top$. That is, \[ \bigvee \{a \in \alpha \mid \text{$a$ is an atom}\} = \top. \]

CompleteLattice.isAtomistic_iff theorem

{α} [CompleteLattice α] : IsAtomistic α ↔ ∀ b : α, ∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Full source

nonrec lemma CompleteLattice.isAtomistic_iff {α} [CompleteLattice α] :
    IsAtomisticIsAtomistic α ↔ ∀ b : α, ∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a := by
  simp_rw [isAtomistic_iff, isLUB_iff_sSup_eq, eq_comm]

Characterization of Atomistic Complete Lattices: $b = \bigvee s$ for a set $s$ of atoms

Informal description

A complete lattice $\alpha$ is atomistic if and only if every element $b \in \alpha$ is the supremum of a set of atoms, i.e., there exists a set $s \subseteq \alpha$ such that $b = \bigvee s$ and every element $a \in s$ is an atom (i.e., $a \neq \bot$ and for any $x$, if $x < a$ then $x = \bot$).

CompleteLattice.isCoatomistic_iff theorem

{α} [CompleteLattice α] : IsCoatomistic α ↔ ∀ b : α, ∃ s : Set α, b = sInf s ∧ ∀ a ∈ s, IsCoatom a

Full source

nonrec lemma CompleteLattice.isCoatomistic_iff {α} [CompleteLattice α] :
    IsCoatomisticIsCoatomistic α ↔ ∀ b : α, ∃ s : Set α, b = sInf s ∧ ∀ a ∈ s, IsCoatom a := by
  simp_rw [isCoatomistic_iff, isGLB_iff_sInf_eq, eq_comm]

Characterization of Coatomistic Complete Lattices: $b = \bigwedge s$ for a set $s$ of coatoms

Informal description

A complete lattice $\alpha$ is coatomistic if and only if every element $b \in \alpha$ can be expressed as the infimum of a set of coatoms, i.e., there exists a set $s \subseteq \alpha$ such that $b = \bigwedge s$ and every element $a \in s$ is a coatom (i.e., $a \neq \top$ and for any $x$, if $a < x$ then $x = \top$).

CompleteAtomicBooleanAlgebra.instIsAtomistic instance

{α} [CompleteAtomicBooleanAlgebra α] : IsAtomistic α

Full source

instance {α} [CompleteAtomicBooleanAlgebra α] : IsAtomistic α :=
  CompleteLattice.isAtomistic_iff.2 fun b ↦ by
    inhabit α
    refine ⟨{ a | IsAtom a ∧ a ≤ b }, ?_, fun a ha => ha.1⟩
    refine le_antisymm ?_ (sSup_le fun c hc => hc.2)
    have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq, iInf_const]
    rw [← this]; clear this
    simp_rw [iInf_iSup_eq, iSup_le_iff]; intro g
    if h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥ then simp [h] else
    refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩; clear h
    have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
    revert this
    nontriviality α
    cases g c <;> simp

Complete Atomic Boolean Algebras are Atomistic

Informal description

Every complete atomic Boolean algebra is atomistic, meaning every element is the supremum of a set of atoms.

CompleteAtomicBooleanAlgebra.instIsCoatomistic instance

{α} [CompleteAtomicBooleanAlgebra α] : IsCoatomistic α

Full source

instance {α} [CompleteAtomicBooleanAlgebra α] : IsCoatomistic α :=
  isAtomistic_dual_iff_isCoatomistic.1 inferInstance

Complete Atomic Boolean Algebras are Coatomistic

Informal description

Every complete atomic Boolean algebra is coatomistic, meaning every element is the infimum of a set of coatoms.

IsSimpleOrder structure

(α : Type*) [LE α] [BoundedOrder α] : Prop extends Nontrivial α

Full source

/-- An order is simple iff it has exactly two elements, `⊥` and `⊤`. -/
@[mk_iff]
class IsSimpleOrder (α : Type*) [LE α] [BoundedOrder α] : Prop extends Nontrivial α where
  /-- Every element is either `⊥` or `⊤` -/
  eq_bot_or_eq_top : ∀ a : α, a = ⊥ ∨ a = ⊤

Simple Order

Informal description

An order is called simple if it has exactly two distinct elements: the least element $\bot$ and the greatest element $\top$.

isSimpleOrder_iff_isSimpleOrder_orderDual theorem

[LE α] [BoundedOrder α] : IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ

Full source

theorem isSimpleOrder_iff_isSimpleOrder_orderDual [LE α] [BoundedOrder α] :
    IsSimpleOrderIsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ := by
  constructor <;> intro i <;> haveI := i
  · exact
      { exists_pair_ne := @exists_pair_ne α _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }
  · exact
      { exists_pair_ne := @exists_pair_ne αᵒᵈ _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }

Duality of Simple Orders: $\text{IsSimpleOrder}(\alpha) \leftrightarrow \text{IsSimpleOrder}(\alpha^{\text{op}})$

Informal description

For any partially ordered set $\alpha$ with a bounded order (having both a least element $\bot$ and a greatest element $\top$), the order $\alpha$ is simple (having exactly two distinct elements $\bot$ and $\top$) if and only if its order dual $\alpha^{\text{op}}$ is simple.

IsSimpleOrder.bot_ne_top theorem

[LE α] [BoundedOrder α] [IsSimpleOrder α] : (⊥ : α) ≠ (⊤ : α)

Full source

theorem IsSimpleOrder.bot_ne_top [LE α] [BoundedOrder α] [IsSimpleOrder α] : (⊥ : α) ≠ (⊤ : α) := by
  obtain ⟨a, b, h⟩ := exists_pair_ne α
  rcases eq_bot_or_eq_top a with (rfl | rfl) <;> rcases eq_bot_or_eq_top b with (rfl | rfl) <;>
    first |simpa|simpa using h.symm

Bottom and Top are Distinct in a Simple Order

Informal description

In a simple order $\alpha$ with a least element $\bot$ and a greatest element $\top$, the bottom element is not equal to the top element, i.e., $\bot \neq \top$.

OrderDual.instIsSimpleOrder instance

{α} [LE α] [BoundedOrder α] [IsSimpleOrder α] : IsSimpleOrder αᵒᵈ

Full source

instance OrderDual.instIsSimpleOrder {α} [LE α] [BoundedOrder α] [IsSimpleOrder α] :
    IsSimpleOrder αᵒᵈ := isSimpleOrder_iff_isSimpleOrder_orderDual.1 (by infer_instance)

Duality of Simple Orders: $\alpha$ is simple if and only if $\alpha^{\text{op}}$ is simple

Informal description

For any partially ordered set $\alpha$ with a bounded order (having both a least element $\bot$ and a greatest element $\top$) that is simple (i.e., has exactly two distinct elements $\bot$ and $\top$), the order dual $\alpha^{\text{op}}$ is also simple.

IsSimpleOrder.preorder definition

{α} [LE α] [BoundedOrder α] [IsSimpleOrder α] : Preorder α

Full source

/-- A simple `BoundedOrder` induces a preorder. This is not an instance to prevent loops. -/
protected def IsSimpleOrder.preorder {α} [LE α] [BoundedOrder α] [IsSimpleOrder α] :
    Preorder α where
  le := (· ≤ ·)
  le_refl a := by rcases eq_bot_or_eq_top a with (rfl | rfl) <;> simp
  le_trans a b c := by
    rcases eq_bot_or_eq_top a with (rfl | rfl)
    · simp
    · rcases eq_bot_or_eq_top b with (rfl | rfl)
      · rcases eq_bot_or_eq_top c with (rfl | rfl) <;> simp
      · simp

Preorder structure on a simple order

Informal description

Given a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$), this defines a preorder structure on $\alpha$ where: - The relation $\leq$ is the given order relation. - Reflexivity holds: for any $a \in \alpha$, $a \leq a$. - Transitivity holds: for any $a, b, c \in \alpha$, if $a \leq b$ and $b \leq c$, then $a \leq c$.

IsSimpleOrder.linearOrder definition

[DecidableEq α] : LinearOrder α

Full source

/-- A simple partial ordered `BoundedOrder` induces a linear order.
This is not an instance to prevent loops. -/
protected def IsSimpleOrder.linearOrder [DecidableEq α] : LinearOrder α :=
  { (inferInstance : PartialOrder α) with
    le_total := fun a b => by rcases eq_bot_or_eq_top a with (rfl | rfl) <;> simp
    -- Note from #23976: do we want this inlined or should this be a separate definition?
    toDecidableLE := fun a b =>
      if ha : a = ⊥ then isTrue (ha.le.trans bot_le)
      else
        if hb : b = ⊤ then isTrue (le_top.trans hb.ge)
        else
          isFalse fun H =>
            hb (top_unique (le_trans (top_le_iff.mpr (Or.resolve_left
              (eq_bot_or_eq_top a) ha)) H))
    toDecidableEq := ‹_› }

Linear order structure on a simple order

Informal description

Given a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$) and a decidable equality on $\alpha$, the structure defines a linear order on $\alpha$ where: - The relation $\leq$ is total: for any $a, b \in \alpha$, either $a \leq b$ or $b \leq a$. - The equality is decidable. - The partial order structure is inherited from the existing partial order on $\alpha$.

isAtom_top theorem

: IsAtom (⊤ : α)

Full source

theorem isAtom_top : IsAtom (⊤ : α) :=
  ⟨top_ne_bot, fun a ha => Or.resolve_right (eq_bot_or_eq_top a) (ne_of_lt ha)⟩

Top Element is an Atom in a Simple Order

Informal description

In a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$), the top element $\top$ is an atom. That is, $\top \neq \bot$ and there is no element strictly between $\bot$ and $\top$.

isAtom_iff_eq_top theorem

{a : α} : IsAtom a ↔ a = ⊤

Full source

@[simp]
theorem isAtom_iff_eq_top {a : α} : IsAtomIsAtom a ↔ a = ⊤ :=
  ⟨fun h ↦ (eq_bot_or_eq_top a).resolve_left h.1, (· ▸ isAtom_top)⟩

Characterization of Atoms in Simple Orders: $a$ is an atom $\iff$ $a = \top$

Informal description

In a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$), an element $a$ is an atom if and only if $a = \top$.

isCoatom_bot theorem

: IsCoatom (⊥ : α)

Full source

theorem isCoatom_bot : IsCoatom (⊥ : α) :=
  isAtom_dual_iff_isCoatom.1 isAtom_top

Bottom Element is a Coatom in a Simple Order

Informal description

In a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$), the bottom element $\bot$ is a coatom. That is, $\bot \neq \top$ and there is no element strictly between $\bot$ and $\top$.

isCoatom_iff_eq_bot theorem

{a : α} : IsCoatom a ↔ a = ⊥

Full source

@[simp]
theorem isCoatom_iff_eq_bot {a : α} : IsCoatomIsCoatom a ↔ a = ⊥ :=
  ⟨fun h ↦ (eq_bot_or_eq_top a).resolve_right h.1, (· ▸ isCoatom_bot)⟩

Characterization of Coatoms in Simple Orders: $a$ is a coatom $\iff$ $a = \bot$

Informal description

In a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$), an element $a$ is a coatom if and only if $a = \bot$.

bot_covBy_top theorem

: (⊥ : α) ⋖ ⊤

Full source

theorem bot_covBy_top : (⊥ : α) ⋖ ⊤ :=
  isAtom_top.bot_covBy

Bottom Element is Covered by Top Element in Simple Order

Informal description

In a simple order $\alpha$ with least element $\bot$ and greatest element $\top$, the bottom element $\bot$ is covered by the top element $\top$, denoted $\bot \lessdot \top$. This means that $\bot < \top$ and there is no element $x$ in $\alpha$ such that $\bot < x < \top$.

IsSimpleOrder.lattice definition

{α} [DecidableEq α] [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : Lattice α

Full source

/-- A simple partial ordered `BoundedOrder` induces a lattice.
This is not an instance to prevent loops -/
protected def lattice {α} [DecidableEq α] [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] :
    Lattice α :=
  @LinearOrder.toLattice α IsSimpleOrder.linearOrder

Lattice structure on a simple order

Informal description

Given a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$) with decidable equality and a partial order structure, the structure defines a lattice on $\alpha$ where: - The supremum (join) operation $\sqcup$ is given by the maximum - The infimum (meet) operation $\sqcap$ is given by the minimum This is not declared as a global instance to prevent potential definition loops.

IsSimpleOrder.distribLattice definition

: DistribLattice α

Full source

/-- A lattice that is a `BoundedOrder` is a distributive lattice.
This is not an instance to prevent loops -/
protected def distribLattice : DistribLattice α :=
  { (inferInstance : Lattice α) with
    le_sup_inf := fun x y z => by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp }

Distributive lattice structure on a simple order

Informal description

Given a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$), the structure defines a distributive lattice on $\alpha$ where: - The supremum (join) operation $\sqcup$ is given by the maximum - The infimum (meet) operation $\sqcap$ is given by the minimum - The distributive property $(x \sqcup y) \sqcap (x \sqcup z) \leq x \sqcup (y \sqcap z)$ holds for all $x, y, z \in \alpha$

IsSimpleOrder.instIsAtomic instance

: IsAtomic α

Full source

instance (priority := 100) : IsAtomic α :=
  ⟨fun b => (eq_bot_or_eq_top b).imp_right fun h => ⟨⊤, ⟨isAtom_top, ge_of_eq h⟩⟩⟩

Simple Orders are Atomic

Informal description

Every simple order $\alpha$ (a bounded order with exactly two elements $\bot$ and $\top$) is atomic. That is, every element $x \neq \bot$ has an atom below it (which in this case must be $\top$).

IsSimpleOrder.instIsCoatomic instance

: IsCoatomic α

Full source

instance (priority := 100) : IsCoatomic α :=
  isAtomic_dual_iff_isCoatomic.1 (by infer_instance)

Simple Orders are Coatomic

Informal description

Every simple order $\alpha$ (a bounded order with exactly two elements $\bot$ and $\top$) is coatomic. That is, every element $x \neq \top$ has a coatom above it (which in this case must be $\bot$).

IsSimpleOrder.equivBool definition

{α} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] : α ≃ Bool

Full source

/-- Every simple lattice is isomorphic to `Bool`, regardless of order. -/
@[simps]
def equivBool {α} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] : α ≃ Bool where
  toFun x := x = ⊤
  invFun x := x.casesOn ⊥ ⊤
  left_inv x := by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp [bot_ne_top]
  right_inv x := by cases x <;> simp [bot_ne_top]

Bijection between a simple order and Bool

Informal description

For any simple order $\alpha$ (i.e., an order with exactly two distinct elements $\bot$ and $\top$), there exists a bijection $\alpha \simeq \text{Bool}$ that maps $\bot$ to $\text{false}$ and $\top$ to $\text{true}$. The inverse map sends $\text{false}$ to $\bot$ and $\text{true}$ to $\top$.

IsSimpleOrder.orderIsoBool definition

: α ≃o Bool

Full source

/-- Every simple lattice over a partial order is order-isomorphic to `Bool`. -/
def orderIsoBool : α ≃o Bool :=
  { equivBool with
    map_rel_iff' := @fun a b => by
      rcases eq_bot_or_eq_top a with (rfl | rfl)
      · simp [bot_ne_top]
      · rcases eq_bot_or_eq_top b with (rfl | rfl)
        · simp [bot_ne_top.symm, bot_ne_top, Bool.false_lt_true]
        · simp [bot_ne_top] }

Order isomorphism between a simple order and Bool

Informal description

For any simple order $\alpha$ (i.e., a bounded order with exactly two distinct elements $\bot$ and $\top$), there exists an order isomorphism $\alpha \simeq_o \text{Bool}$ that maps $\bot$ to $\text{false}$ and $\top$ to $\text{true}$, and preserves the order relation in both directions.

IsSimpleOrder.booleanAlgebra definition

{α} [DecidableEq α] [Lattice α] [BoundedOrder α] [IsSimpleOrder α] : BooleanAlgebra α

Full source

/-- A simple `BoundedOrder` is also a `BooleanAlgebra`. -/
protected def booleanAlgebra {α} [DecidableEq α] [Lattice α] [BoundedOrder α] [IsSimpleOrder α] :
    BooleanAlgebra α :=
  { inferInstanceAs (BoundedOrder α), IsSimpleOrder.distribLattice with
    compl := fun x => if x = ⊥ then ⊤ else ⊥
    sdiff := fun x y => if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥
    sdiff_eq := fun x y => by
      rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp [bot_ne_top, SDiff.sdiff, compl]
    inf_compl_le_bot := fun x => by
      rcases eq_bot_or_eq_top x with (rfl | rfl)
      · simp
      · simp
    top_le_sup_compl := fun x => by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp }

Boolean algebra structure on a simple order

Informal description

Given a simple order $\alpha$ (a bounded lattice with exactly two distinct elements $\bot$ and $\top$), the structure defines a Boolean algebra on $\alpha$ where: - The complement operation is defined as $x^\complement = \top$ if $x = \bot$, and $x^\complement = \bot$ if $x = \top$. - The set difference operation is defined as $x \setminus y = \top$ if $x = \top$ and $y = \bot$, otherwise $x \setminus y = \bot$. - The Heyting implication is defined accordingly to satisfy the Boolean algebra axioms.

IsSimpleOrder.completeLattice definition

: CompleteLattice α

Full source

/-- A simple `BoundedOrder` is also complete. -/
protected noncomputable def completeLattice : CompleteLattice α :=
  { (inferInstance : Lattice α),
    (inferInstance : BoundedOrder α) with
    sSup := fun s => if ⊤ ∈ s then ⊤ else ⊥
    sInf := fun s => if ⊥ ∈ s then ⊥ else ⊤
    le_sSup := fun s x h => by
      rcases eq_bot_or_eq_top x with (rfl | rfl)
      · exact bot_le
      · rw [if_pos h]
    sSup_le := fun s x h => by
      rcases eq_bot_or_eq_top x with (rfl | rfl)
      · rw [if_neg]
        intro con
        exact bot_ne_top (eq_top_iff.2 (h ⊤ con))
      · exact le_top
    sInf_le := fun s x h => by
      rcases eq_bot_or_eq_top x with (rfl | rfl)
      · rw [if_pos h]
      · exact le_top
    le_sInf := fun s x h => by
      rcases eq_bot_or_eq_top x with (rfl | rfl)
      · exact bot_le
      · rw [if_neg]
        intro con
        exact top_ne_bot (eq_bot_iff.2 (h ⊥ con)) }

Complete lattice structure on a simple order

Informal description

For a simple order $\alpha$ (a bounded order with exactly two distinct elements $\bot$ and $\top$), the complete lattice structure on $\alpha$ is defined as follows: - The supremum $\bigsqcup s$ of a set $s$ is $\top$ if $\top \in s$, otherwise $\bot$. - The infimum $\bigsqcap s$ of a set $s$ is $\bot$ if $\bot \in s$, otherwise $\top$. - The supremum satisfies the properties: - $\bigsqcup s$ is an upper bound for $s$. - If $x$ is any upper bound for $s$, then $\bigsqcup s \leq x$. - The infimum satisfies the properties: - $\bigsqcap s$ is a lower bound for $s$. - If $x$ is any lower bound for $s$, then $x \leq \bigsqcap s$.

IsSimpleOrder.completeBooleanAlgebra definition

: CompleteBooleanAlgebra α

Full source

/-- A simple `BoundedOrder` is also a `CompleteBooleanAlgebra`. -/
protected noncomputable def completeBooleanAlgebra : CompleteBooleanAlgebra α :=
  { __ := IsSimpleOrder.completeLattice
    __ := IsSimpleOrder.booleanAlgebra
    iInf_sup_le_sup_sInf := fun x s => by
      rcases eq_bot_or_eq_top x with (rfl | rfl)
      · simp [bot_sup_eq, ← sInf_eq_iInf]
      · simp only [top_le_iff, top_sup_eq, iInf_top, le_sInf_iff, le_refl]
    inf_sSup_le_iSup_inf := fun x s => by
      rcases eq_bot_or_eq_top x with (rfl | rfl)
      · simp only [le_bot_iff, sSup_eq_bot, bot_inf_eq, iSup_bot, le_refl]
      · simp only [top_inf_eq, ← sSup_eq_iSup]
        exact le_rfl }

Complete Boolean algebra structure on a simple order

Informal description

Given a simple order $\alpha$ (a bounded lattice with exactly two distinct elements $\bot$ and $\top$), the structure defines a complete Boolean algebra on $\alpha$ where: - The lattice operations and order structure are inherited from the complete lattice structure of $\alpha$. - The Boolean algebra operations are defined as in `IsSimpleOrder.booleanAlgebra`. - The following properties hold: - For any element $x$ and any set $s$, the infimum of $s$ joined with $x$ is less than or equal to the supremum of the set obtained by joining $x$ with each element of $s$. - For any element $x$ and any set $s$, the meet of $x$ with the supremum of $s$ is less than or equal to the supremum of the set obtained by meeting $x$ with each element of $s$.

IsSimpleOrder.instComplementedLattice instance

: ComplementedLattice α

Full source

instance : ComplementedLattice α :=
  letI := IsSimpleOrder.completeBooleanAlgebra (α := α); inferInstance

Simple Orders are Complemented Lattices

Informal description

Every simple order is a complemented lattice. That is, for a simple order $\alpha$ (a bounded lattice with exactly two distinct elements $\bot$ and $\top$), every element has a complement. Specifically, $\bot$ and $\top$ are complements of each other.

IsSimpleOrder.instIsAtomistic instance

: IsAtomistic α

Full source

instance (priority := 100) : IsAtomistic α where
  isLUB_atoms b := (eq_bot_or_eq_top b).elim (fun h ↦ ⟨∅, by simp [h]⟩) (fun h ↦ ⟨{⊤}, by simp [h]⟩)

Simple Orders are Atomistic Lattices

Informal description

Every simple order is an atomistic lattice. That is, in a simple order (which has exactly two distinct elements $\bot$ and $\top$), every element is the supremum of a set of atoms (where the only atom is $\top$).

IsSimpleOrder.instIsCoatomistic instance

: IsCoatomistic α

Full source

instance (priority := 100) : IsCoatomistic α :=
  isAtomistic_dual_iff_isCoatomistic.1 (by infer_instance)

Simple Orders are Coatomistic Lattices

Informal description

Every simple order is a coatomistic lattice. That is, in a simple order (which has exactly two distinct elements $\bot$ and $\top$), every element is the infimum of a set of coatoms (where the only coatom is $\bot$).

isSimpleOrder_iff_isAtom_top theorem

[PartialOrder α] [BoundedOrder α] : IsSimpleOrder α ↔ IsAtom (⊤ : α)

Full source

theorem isSimpleOrder_iff_isAtom_top [PartialOrder α] [BoundedOrder α] :
    IsSimpleOrderIsSimpleOrder α ↔ IsAtom (⊤ : α) :=
  ⟨fun h => @isAtom_top _ _ _ h, fun h =>
    { exists_pair_ne := ⟨⊤, ⊥, h.1⟩
      eq_bot_or_eq_top := fun a => ((eq_or_lt_of_le le_top).imp_right (h.2 a)).symm }⟩

Characterization of Simple Orders via Top Atom: $\text{IsSimpleOrder} \alpha \leftrightarrow \text{IsAtom}(\top)$

Informal description

A bounded partial order $\alpha$ is a simple order (having exactly two distinct elements $\bot$ and $\top$) if and only if the top element $\top$ is an atom (i.e., $\top \neq \bot$ and there is no element strictly between $\bot$ and $\top$).

isSimpleOrder_iff_isCoatom_bot theorem

[PartialOrder α] [BoundedOrder α] : IsSimpleOrder α ↔ IsCoatom (⊥ : α)

Full source

theorem isSimpleOrder_iff_isCoatom_bot [PartialOrder α] [BoundedOrder α] :
    IsSimpleOrderIsSimpleOrder α ↔ IsCoatom (⊥ : α) :=
  isSimpleOrder_iff_isSimpleOrder_orderDual.trans isSimpleOrder_iff_isAtom_top

Characterization of Simple Orders via Bottom Coatom: $\text{IsSimpleOrder}(\alpha) \leftrightarrow \text{IsCoatom}(\bot)$

Informal description

A bounded partial order $\alpha$ is a simple order (having exactly two distinct elements $\bot$ and $\top$) if and only if the bottom element $\bot$ is a coatom (i.e., $\bot \neq \top$ and there is no element strictly between $\bot$ and $\top$).

Set.isSimpleOrder_Iic_iff_isAtom theorem

[PartialOrder α] [OrderBot α] {a : α} : IsSimpleOrder (Iic a) ↔ IsAtom a

Full source

theorem isSimpleOrder_Iic_iff_isAtom [PartialOrder α] [OrderBot α] {a : α} :
    IsSimpleOrderIsSimpleOrder (Iic a) ↔ IsAtom a :=
  isSimpleOrder_iff_isAtom_top.trans <|
    and_congr (not_congr Subtype.mk_eq_mk)
      ⟨fun h b ab => Subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab), fun h ⟨b, _⟩ hbotb =>
        Subtype.mk_eq_mk.2 (h b (Subtype.mk_lt_mk.1 hbotb))⟩

Characterization of Simple Interval via Atom: $\text{IsSimpleOrder}((-\infty, a]) \leftrightarrow \text{IsAtom}(a)$

Informal description

Let $\alpha$ be a partial order with a bottom element $\bot$. For any element $a \in \alpha$, the interval $(-\infty, a]$ (with the induced order) is a simple order (having exactly two distinct elements $\bot$ and $a$) if and only if $a$ is an atom in $\alpha$ (i.e., $a \neq \bot$ and there is no element strictly between $\bot$ and $a$).

Set.isSimpleOrder_Ici_iff_isCoatom theorem

[PartialOrder α] [OrderTop α] {a : α} : IsSimpleOrder (Ici a) ↔ IsCoatom a

Full source

theorem isSimpleOrder_Ici_iff_isCoatom [PartialOrder α] [OrderTop α] {a : α} :
    IsSimpleOrderIsSimpleOrder (Ici a) ↔ IsCoatom a :=
  isSimpleOrder_iff_isCoatom_bot.trans <|
    and_congr (not_congr Subtype.mk_eq_mk)
      ⟨fun h b ab => Subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab), fun h ⟨b, _⟩ hbotb =>
        Subtype.mk_eq_mk.2 (h b (Subtype.mk_lt_mk.1 hbotb))⟩

Characterization of Simple Interval via Coatom: $\text{IsSimpleOrder}([a, \infty)) \leftrightarrow \text{IsCoatom}(a)$

Informal description

Let $\alpha$ be a partial order with a top element $\top$. For any element $a \in \alpha$, the interval $[a, \infty)$ (with the induced order) is a simple order (having exactly two distinct elements $a$ and $\top$) if and only if $a$ is a coatom in $\alpha$ (i.e., $a \neq \top$ and there is no element strictly between $a$ and $\top$).

OrderEmbedding.isAtom_of_map_bot_of_image theorem

[OrderBot α] [OrderBot β] (f : β ↪o α) (hbot : f ⊥ = ⊥) {b : β} (hb : IsAtom (f b)) : IsAtom b

Full source

theorem isAtom_of_map_bot_of_image [OrderBot α] [OrderBot β] (f : β ↪o α) (hbot : f ⊥ = ⊥) {b : β}
    (hb : IsAtom (f b)) : IsAtom b := by
  simp only [← bot_covBy_iff] at hb ⊢
  exact CovBy.of_image f (hbot.symm ▸ hb)

Order Embedding Preserves Atoms Under Bottom Preservation

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given an order embedding $f \colon \beta \hookrightarrow \alpha$ such that $f(\bot_\beta) = \bot_\alpha$, and an element $b \in \beta$ such that $f(b)$ is an atom in $\alpha$, then $b$ is an atom in $\beta$.

OrderEmbedding.isCoatom_of_map_top_of_image theorem

[OrderTop α] [OrderTop β] (f : β ↪o α) (htop : f ⊤ = ⊤) {b : β} (hb : IsCoatom (f b)) : IsCoatom b

Full source

theorem isCoatom_of_map_top_of_image [OrderTop α] [OrderTop β] (f : β ↪o α) (htop : f ⊤ = ⊤)
    {b : β} (hb : IsCoatom (f b)) : IsCoatom b :=
  f.dual.isAtom_of_map_bot_of_image htop hb

Order Embedding Preserves Coatoms Under Top Preservation

Informal description

Let $\alpha$ and $\beta$ be partial orders with top elements $\top_\alpha$ and $\top_\beta$ respectively. Given an order embedding $f \colon \beta \hookrightarrow \alpha$ such that $f(\top_\beta) = \top_\alpha$, and an element $b \in \beta$ such that $f(b)$ is a coatom in $\alpha$, then $b$ is a coatom in $\beta$.

GaloisInsertion.isAtom_of_u_bot theorem

 [OrderBot α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) {b : β}
  (hb : IsAtom (u b)) : IsAtom b

Full source

theorem isAtom_of_u_bot [OrderBot α] [OrderBot β] {l : α → β} {u : β → α}
    (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) {b : β} (hb : IsAtom (u b)) : IsAtom b :=
  OrderEmbedding.isAtom_of_map_bot_of_image
    ⟨⟨u, gi.u_injective⟩, @GaloisInsertion.u_le_u_iff _ _ _ _ _ _ gi⟩ hbot hb

Galois Insertion Preserves Atoms Under Bottom Preservation

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$ such that $u(\bot_\beta) = \bot_\alpha$, and an element $b \in \beta$ such that $u(b)$ is an atom in $\alpha$, then $b$ is an atom in $\beta$.

GaloisInsertion.isAtom_iff theorem

 [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥)
  (h_atom : ∀ a, IsAtom a → u (l a) = a) (a : α) : IsAtom (l a) ↔ IsAtom a

Full source

theorem isAtom_iff [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α}
    (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ a, IsAtom a → u (l a) = a) (a : α) :
    IsAtomIsAtom (l a) ↔ IsAtom a := by
  refine ⟨fun hla => ?_, fun ha => gi.isAtom_of_u_bot hbot ((h_atom a ha).symm ▸ ha)⟩
  obtain ⟨a', ha', hab'⟩ :=
    (eq_bot_or_exists_atom_le (u (l a))).resolve_left (hbot ▸ fun h => hla.1 (gi.u_injective h))
  have :=
    (hla.le_iff.mp <| (gi.l_u_eq (l a) ▸ gi.gc.monotone_l hab' : l a' ≤ l a)).resolve_left fun h =>
      ha'.1 (hbot ▸ h_atom a' ha' ▸ congr_arg u h)
  have haa' : a = a' :=
    (ha'.le_iff.mp <|
          (gi.gc.le_u_l a).trans_eq (h_atom a' ha' ▸ congr_arg u this.symm)).resolve_left
      (mt (congr_arg l) (gi.gc.l_bot.symm ▸ hla.1))
  exact haa'.symm ▸ ha'

Characterization of Atoms under Galois Insertion in Atomic Lattices

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively, where $\alpha$ is atomic. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$ such that $u(\bot_\beta) = \bot_\alpha$ and for every atom $a$ in $\alpha$, $u(l(a)) = a$, then for any element $a \in \alpha$, $l(a)$ is an atom in $\beta$ if and only if $a$ is an atom in $\alpha$.

GaloisInsertion.isAtom_iff' theorem

 [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥)
  (h_atom : ∀ a, IsAtom a → u (l a) = a) (b : β) : IsAtom (u b) ↔ IsAtom b

Full source

theorem isAtom_iff' [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α}
    (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ a, IsAtom a → u (l a) = a) (b : β) :
    IsAtomIsAtom (u b) ↔ IsAtom b := by rw [← gi.isAtom_iff hbot h_atom, gi.l_u_eq]

Characterization of Atoms via Galois Insertion in Atomic Lattices (Dual Form)

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively, where $\alpha$ is atomic. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$ such that $u(\bot_\beta) = \bot_\alpha$ and for every atom $a$ in $\alpha$, $u(l(a)) = a$, then for any element $b \in \beta$, $u(b)$ is an atom in $\alpha$ if and only if $b$ is an atom in $\beta$.

GaloisInsertion.isCoatom_of_image theorem

 [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) {b : β} (hb : IsCoatom (u b)) : IsCoatom b

Full source

theorem isCoatom_of_image [OrderTop α] [OrderTop β] {l : α → β} {u : β → α}
    (gi : GaloisInsertion l u) {b : β} (hb : IsCoatom (u b)) : IsCoatom b :=
  OrderEmbedding.isCoatom_of_map_top_of_image
    ⟨⟨u, gi.u_injective⟩, @GaloisInsertion.u_le_u_iff _ _ _ _ _ _ gi⟩ gi.gc.u_top hb

Galois Insertion Preserves Coatoms via Upper Adjoint

Informal description

Let $\alpha$ and $\beta$ be partial orders with top elements $\top_\alpha$ and $\top_\beta$ respectively. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$ (where $l \colon \alpha \to \beta$ is the lower adjoint and $u \colon \beta \to \alpha$ is the upper adjoint), and an element $b \in \beta$ such that $u(b)$ is a coatom in $\alpha$, then $b$ is a coatom in $\beta$.

GaloisInsertion.isCoatom_iff theorem

 [OrderTop α] [IsCoatomic α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u)
  (h_coatom : ∀ a : α, IsCoatom a → u (l a) = a) (b : β) : IsCoatom (u b) ↔ IsCoatom b

Full source

theorem isCoatom_iff [OrderTop α] [IsCoatomic α] [OrderTop β] {l : α → β} {u : β → α}
    (gi : GaloisInsertion l u) (h_coatom : ∀ a : α, IsCoatom a → u (l a) = a) (b : β) :
    IsCoatomIsCoatom (u b) ↔ IsCoatom b := by
  refine ⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩
  obtain ⟨a, ha, hab⟩ :=
    (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
      hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h
  have : l a = b :=
    (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
      ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)
  exact this ▸ (h_coatom a ha).symm ▸ ha

Characterization of Coatoms under Galois Insertion with Coatomic Domain

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets with top elements $\top_\alpha$ and $\top_\beta$ respectively, where $\alpha$ is coatomic. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$ (with $l \colon \alpha \to \beta$ the lower adjoint and $u \colon \beta \to \alpha$ the upper adjoint) such that for every coatom $a$ in $\alpha$, $u(l(a)) = a$, then for any element $b \in \beta$, $u(b)$ is a coatom in $\alpha$ if and only if $b$ is a coatom in $\beta$.

GaloisCoinsertion.isCoatom_of_l_top theorem

 [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (hbot : l ⊤ = ⊤) {a : α}
  (hb : IsCoatom (l a)) : IsCoatom a

Full source

theorem isCoatom_of_l_top [OrderTop α] [OrderTop β] {l : α → β} {u : β → α}
    (gi : GaloisCoinsertion l u) (hbot : l ⊤ = ⊤) {a : α} (hb : IsCoatom (l a)) : IsCoatom a :=
  gi.dual.isAtom_of_u_bot hbot hb.dual

Galois Coinsertion Preserves Coatoms Under Top Preservation

Informal description

Let $\alpha$ and $\beta$ be partial orders with top elements $\top_\alpha$ and $\top_\beta$ respectively. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$ such that $l(\top_\alpha) = \top_\beta$, and an element $a \in \alpha$ such that $l(a)$ is a coatom in $\beta$, then $a$ is a coatom in $\alpha$.

GaloisCoinsertion.isCoatom_iff theorem

 [OrderTop α] [OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤)
  (h_coatom : ∀ b, IsCoatom b → l (u b) = b) (b : β) : IsCoatom (u b) ↔ IsCoatom b

Full source

theorem isCoatom_iff [OrderTop α] [OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α}
    (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ b, IsCoatom b → l (u b) = b)
    (b : β) : IsCoatomIsCoatom (u b) ↔ IsCoatom b :=
  gi.dual.isAtom_iff htop h_coatom b

Characterization of Coatoms under Galois Coinsertion in Coatomic Lattices

Informal description

Let $\alpha$ and $\beta$ be partial orders with top elements $\top_\alpha$ and $\top_\beta$ respectively, where $\beta$ is coatomic. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$ such that $l(\top_\alpha) = \top_\beta$ and for every coatom $b$ in $\beta$, $l(u(b)) = b$, then for any element $b \in \beta$, $u(b)$ is a coatom in $\alpha$ if and only if $b$ is a coatom in $\beta$.

GaloisCoinsertion.isCoatom_iff' theorem

 [OrderTop α] [OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤)
  (h_coatom : ∀ b, IsCoatom b → l (u b) = b) (a : α) : IsCoatom (l a) ↔ IsCoatom a

Full source

theorem isCoatom_iff' [OrderTop α] [OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α}
    (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ b, IsCoatom b → l (u b) = b)
    (a : α) : IsCoatomIsCoatom (l a) ↔ IsCoatom a :=
  gi.dual.isAtom_iff' htop h_coatom a

Characterization of Coatoms via Galois Coinsertion in Coatomic Lattices (Dual Form)

Informal description

Let $\alpha$ and $\beta$ be partial orders with top elements $\top_\alpha$ and $\top_\beta$ respectively, where $\beta$ is coatomic. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$ such that $l(\top_\alpha) = \top_\beta$ and for every coatom $b$ in $\beta$, $l(u(b)) = b$, then for any element $a \in \alpha$, $l(a)$ is a coatom in $\beta$ if and only if $a$ is a coatom in $\alpha$.

GaloisCoinsertion.isAtom_of_image theorem

 [OrderBot α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) {a : α} (hb : IsAtom (l a)) : IsAtom a

Full source

theorem isAtom_of_image [OrderBot α] [OrderBot β] {l : α → β} {u : β → α}
    (gi : GaloisCoinsertion l u) {a : α} (hb : IsAtom (l a)) : IsAtom a :=
  gi.dual.isCoatom_of_image hb.dual

Galois Coinsertion Preserves Atoms via Lower Adjoint

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$ (where $l \colon \alpha \to \beta$ is the lower adjoint and $u \colon \beta \to \alpha$ is the upper adjoint), and an element $a \in \alpha$ such that $l(a)$ is an atom in $\beta$, then $a$ is an atom in $\alpha$.

GaloisCoinsertion.isAtom_iff theorem

 [OrderBot α] [OrderBot β] [IsAtomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u)
  (h_atom : ∀ b, IsAtom b → l (u b) = b) (a : α) : IsAtom (l a) ↔ IsAtom a

Full source

theorem isAtom_iff [OrderBot α] [OrderBot β] [IsAtomic β] {l : α → β} {u : β → α}
    (gi : GaloisCoinsertion l u) (h_atom : ∀ b, IsAtom b → l (u b) = b) (a : α) :
    IsAtomIsAtom (l a) ↔ IsAtom a :=
  gi.dual.isCoatom_iff h_atom a

Characterization of Atoms under Galois Coinsertion with Atomic Codomain

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively, and suppose $\beta$ is atomic. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$ (where $l \colon \alpha \to \beta$ is the lower adjoint and $u \colon \beta \to \alpha$ is the upper adjoint) such that for every atom $b$ in $\beta$, $l(u(b)) = b$, then for any element $a \in \alpha$, $l(a)$ is an atom in $\beta$ if and only if $a$ is an atom in $\alpha$.

OrderIso.isAtom_iff theorem

[OrderBot α] [OrderBot β] (f : α ≃o β) (a : α) : IsAtom (f a) ↔ IsAtom a

Full source

@[simp]
theorem isAtom_iff [OrderBot α] [OrderBot β] (f : α ≃o β) (a : α) : IsAtomIsAtom (f a) ↔ IsAtom a :=
  ⟨f.toGaloisCoinsertion.isAtom_of_image, fun ha =>
    f.toGaloisInsertion.isAtom_of_u_bot (map_bot f.symm) <| (f.symm_apply_apply a).symm ▸ ha⟩

Order Isomorphism Preserves Atoms: $f(a)$ is an atom iff $a$ is an atom

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given an order isomorphism $f : \alpha \simeq_o \beta$ and an element $a \in \alpha$, then $f(a)$ is an atom in $\beta$ if and only if $a$ is an atom in $\alpha$.

OrderIso.isCoatom_iff theorem

[OrderTop α] [OrderTop β] (f : α ≃o β) (a : α) : IsCoatom (f a) ↔ IsCoatom a

Full source

@[simp]
theorem isCoatom_iff [OrderTop α] [OrderTop β] (f : α ≃o β) (a : α) :
    IsCoatomIsCoatom (f a) ↔ IsCoatom a :=
  f.dual.isAtom_iff a

Order Isomorphism Preserves Coatoms: $f(a)$ is a coatom iff $a$ is a coatom

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets with top elements $\top_\alpha$ and $\top_\beta$ respectively. Given an order isomorphism $f : \alpha \simeq_o \beta$ and an element $a \in \alpha$, then $f(a)$ is a coatom in $\beta$ if and only if $a$ is a coatom in $\alpha$.

OrderIso.isSimpleOrder_iff theorem

[BoundedOrder α] [BoundedOrder β] (f : α ≃o β) : IsSimpleOrder α ↔ IsSimpleOrder β

Full source

theorem isSimpleOrder_iff [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) :
    IsSimpleOrderIsSimpleOrder α ↔ IsSimpleOrder β := by
  rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤,
    f.map_top]

Order Isomorphism Preserves Simplicity: $\alpha$ is simple iff $\beta$ is simple under $f \colon \alpha \simeq_o \beta$

Informal description

Let $\alpha$ and $\beta$ be bounded orders. Given an order isomorphism $f \colon \alpha \simeq_o \beta$, the order $\alpha$ is simple (i.e., has exactly two distinct elements $\bot$ and $\top$) if and only if $\beta$ is simple.

OrderIso.isSimpleOrder theorem

[BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) : IsSimpleOrder α

Full source

theorem isSimpleOrder [BoundedOrder α] [BoundedOrder β] [h : IsSimpleOrder β] (f : α ≃o β) :
    IsSimpleOrder α :=
  f.isSimpleOrder_iff.mpr h

Order Isomorphism Preserves Simplicity: $\alpha$ is simple if $\beta$ is simple under $f \colon \alpha \simeq_o \beta$

Informal description

Let $\alpha$ and $\beta$ be bounded orders, and let $f \colon \alpha \simeq_o \beta$ be an order isomorphism. If $\beta$ is a simple order (i.e., has exactly two distinct elements $\bot$ and $\top$), then $\alpha$ is also a simple order.

OrderIso.isAtomic_iff theorem

[OrderBot α] [OrderBot β] (f : α ≃o β) : IsAtomic α ↔ IsAtomic β

Full source

protected theorem isAtomic_iff [OrderBot α] [OrderBot β] (f : α ≃o β) :
    IsAtomicIsAtomic α ↔ IsAtomic β := by
  simp only [isAtomic_iff, f.surjective.forall, f.surjective.exists, ← map_bot f, f.eq_iff_eq,
    f.le_iff_le, f.isAtom_iff]

Order Isomorphism Preserves Atomicity: $\alpha$ is atomic iff $\beta$ is atomic via $f$

Informal description

Let $\alpha$ and $\beta$ be partial orders with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. Given an order isomorphism $f : \alpha \simeq_o \beta$, the order $\alpha$ is atomic if and only if $\beta$ is atomic. Here, an order is *atomic* if every element $x \neq \bot$ has an atom below it.

OrderIso.isCoatomic_iff theorem

[OrderTop α] [OrderTop β] (f : α ≃o β) : IsCoatomic α ↔ IsCoatomic β

Full source

protected theorem isCoatomic_iff [OrderTop α] [OrderTop β] (f : α ≃o β) :
    IsCoatomicIsCoatomic α ↔ IsCoatomic β := by
  simp only [← isAtomic_dual_iff_isCoatomic, f.dual.isAtomic_iff]

Order Isomorphism Preserves Coatomicity: $\alpha$ is coatomic iff $\beta$ is coatomic via $f$

Informal description

Let $\alpha$ and $\beta$ be partial orders with top elements $\top_\alpha$ and $\top_\beta$ respectively. Given an order isomorphism $f : \alpha \simeq_o \beta$, the order $\alpha$ is coatomic if and only if $\beta$ is coatomic. Here, an order is *coatomic* if every element $x \neq \top$ has a coatom above it.

Lattice.isStronglyAtomic theorem

[OrderBot α] [IsUpperModularLattice α] [IsAtomistic α] : IsStronglyAtomic α

Full source

/-- An upper-modular lattice that is atomistic is strongly atomic.
Not an instance to prevent loops. -/
theorem Lattice.isStronglyAtomic [OrderBot α] [IsUpperModularLattice α] [IsAtomistic α] :
    IsStronglyAtomic α where
  exists_covBy_le_of_lt a b hab := by
    obtain ⟨s, hsb, h⟩ := isLUB_atoms b
    refine by_contra fun hcon ↦ hab.not_le <| (isLUB_le_iff hsb).2 fun x hx ↦ ?_
    simp_rw [not_exists, and_comm (b := _ ≤ _), not_and] at hcon
    specialize hcon (x ⊔ a) (sup_le (hsb.1 hx) hab.le)
    obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)
    · exact False.elim <| hcon <|
        (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy
    rwa [inf_eq_left] at h_inf

Strong Atomicity of Upper Modular Atomistic Lattices

Informal description

Let $\alpha$ be a lattice with a bottom element $\bot$. If $\alpha$ is both upper modular and atomistic, then $\alpha$ is strongly atomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a$ is covered by $x$ (i.e., $a \lessdot x$) and $x \leq b$.

Lattice.isStronglyCoatomic theorem

[OrderTop α] [IsLowerModularLattice α] [IsCoatomistic α] : IsStronglyCoatomic α

Full source

/-- A lower-modular lattice that is coatomistic is strongly coatomic.
Not an instance to prevent loops. -/
theorem Lattice.isStronglyCoatomic [OrderTop α] [IsLowerModularLattice α]
    [IsCoatomistic α] : IsStronglyCoatomic α := by
  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
  exact Lattice.isStronglyAtomic

Strong Coatomicity of Lower Modular Coatomistic Lattices

Informal description

Let $\alpha$ be a lattice with a top element $\top$. If $\alpha$ is lower modular and coatomistic, then $\alpha$ is strongly coatomic. That is, for any two elements $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$ (i.e., $x \lessdot b$).

IsCompl.isAtom_iff_isCoatom theorem

: IsAtom a ↔ IsCoatom b

Full source

theorem isAtom_iff_isCoatom : IsAtomIsAtom a ↔ IsCoatom b :=
  Set.isSimpleOrder_Iic_iff_isAtom.symm.trans <|
    hc.IicOrderIsoIci.isSimpleOrder_iff.trans Set.isSimpleOrder_Ici_iff_isCoatom

Complementary Atom and Coatom in Modular Lattices: $a$ is an atom iff $b$ is a coatom

Informal description

Let $\alpha$ be a bounded modular lattice, and let $a, b \in \alpha$ be complementary elements (i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$). Then $a$ is an atom if and only if $b$ is a coatom.

IsCompl.isCoatom_iff_isAtom theorem

: IsCoatom a ↔ IsAtom b

Full source

theorem isCoatom_iff_isAtom : IsCoatomIsCoatom a ↔ IsAtom b :=
  hc.symm.isAtom_iff_isCoatom.symm

Complementary Coatom and Atom in Modular Lattices: $a$ is a coatom iff $b$ is an atom

Informal description

Let $\alpha$ be a bounded modular lattice, and let $a, b \in \alpha$ be complementary elements (i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$). Then $a$ is a coatom if and only if $b$ is an atom.

isCoatomic_of_isAtomic_of_complementedLattice_of_isModular theorem

[IsAtomic α] : IsCoatomic α

Full source

theorem isCoatomic_of_isAtomic_of_complementedLattice_of_isModular [IsAtomic α] :
    IsCoatomic α :=
  ⟨fun x => by
    rcases exists_isCompl x with ⟨y, xy⟩
    apply (eq_bot_or_exists_atom_le y).imp _ _
    · rintro rfl
      exact eq_top_of_isCompl_bot xy
    · rintro ⟨a, ha, ay⟩
      rcases exists_isCompl (xy.symm.IicOrderIsoIci ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩
      refine ⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici ?_, xb⟩
      rw [← hb.isAtom_iff_isCoatom, OrderIso.isAtom_iff]
      apply ha.Iic⟩

Atomicity implies coatomicity in modular complemented lattices

Informal description

In a bounded modular complemented lattice $\alpha$, if $\alpha$ is atomic (i.e., every non-bottom element has an atom below it), then $\alpha$ is coatomic (i.e., every non-top element has a coatom above it).

isAtomic_of_isCoatomic_of_complementedLattice_of_isModular theorem

[IsCoatomic α] : IsAtomic α

Full source

theorem isAtomic_of_isCoatomic_of_complementedLattice_of_isModular [IsCoatomic α] :
    IsAtomic α :=
  isCoatomic_dual_iff_isAtomic.1 isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

Coatomicity implies atomicity in modular complemented lattices

Informal description

In a bounded modular complemented lattice $\alpha$, if $\alpha$ is coatomic (i.e., every non-top element has a coatom above it), then $\alpha$ is atomic (i.e., every non-bottom element has an atom below it).

isAtomic_iff_isCoatomic theorem

: IsAtomic α ↔ IsCoatomic α

Full source

theorem isAtomic_iff_isCoatomic : IsAtomicIsAtomic α ↔ IsCoatomic α :=
  ⟨fun _ => isCoatomic_of_isAtomic_of_complementedLattice_of_isModular,
   fun _ => isAtomic_of_isCoatomic_of_complementedLattice_of_isModular⟩

Equivalence of Atomicity and Coatomicity in Modular Complemented Lattices

Informal description

In a bounded modular complemented lattice $\alpha$, the lattice is atomic (every non-bottom element has an atom below it) if and only if it is coatomic (every non-top element has a coatom above it).

ComplementedLattice.isStronglyAtomic theorem

[IsAtomic α] : IsStronglyAtomic α

Full source

/-- A complemented modular atomic lattice is strongly atomic.
Not an instance to prevent loops. -/
theorem ComplementedLattice.isStronglyAtomic [IsAtomic α] : IsStronglyAtomic α where
  exists_covBy_le_of_lt a b hab := by
    obtain ⟨⟨a', ha'b : a' ≤ b⟩, ha'⟩ := exists_isCompl (α := Set.Iic b) ⟨a, hab.le⟩
    obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'
    · obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint
      exact False.elim <| hab.ne rfl
    refine ⟨d ⊔ a, IsUpperModularLattice.covBy_sup_of_inf_covBy ?_, sup_le (hd.2.trans ha'b) hab.le⟩
    convert hd.1.bot_covBy
    rw [← le_bot_iff, ← show a ⊓ a' = ⊥ by simpa using Subtype.coe_inj.2 ha'.inf_eq_bot, inf_comm]
    exact inf_le_inf_left _ hd.2

Strong atomicity in complemented modular atomic lattices

Informal description

In a complemented modular lattice $\alpha$, if $\alpha$ is atomic (i.e., every non-bottom element has an atom below it), then $\alpha$ is strongly atomic (i.e., for any $a < b$ in $\alpha$, there exists an element $x$ such that $a$ is covered by $x$ and $x \leq b$).

ComplementedLattice.isStronglyCoatomic theorem

[IsCoatomic α] : IsStronglyCoatomic α

Full source

/-- A complemented modular coatomic lattice is strongly coatomic.
Not an instance to prevent loops. -/
theorem ComplementedLattice.isStronglyCoatomic [IsCoatomic α] : IsStronglyCoatomic α :=
  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 <| ComplementedLattice.isStronglyAtomic

Strong coatomicity in complemented modular coatomic lattices

Informal description

In a complemented modular lattice $\alpha$, if $\alpha$ is coatomic (i.e., every non-top element has a coatom above it), then $\alpha$ is strongly coatomic (i.e., for any $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$).

ComplementedLattice.isStronglyAtomic' theorem

[h : IsAtomic α] : IsStronglyCoatomic α

Full source

/-- A complemented modular atomic lattice is strongly coatomic.
Not an instance to prevent loops. -/
theorem ComplementedLattice.isStronglyAtomic' [h : IsAtomic α] : IsStronglyCoatomic α := by
  rw [isAtomic_iff_isCoatomic] at h
  exact isStronglyCoatomic

Strong Coatomicity in Complemented Modular Atomic Lattices

Informal description

In a complemented modular lattice $\alpha$, if $\alpha$ is atomic (i.e., every non-bottom element has an atom below it), then $\alpha$ is strongly coatomic (i.e., for any $a < b$ in $\alpha$, there exists an element $x$ such that $a \leq x$ and $x$ is covered by $b$).

ComplementedLattice.isStronglyCoatomic' theorem

[h : IsCoatomic α] : IsStronglyAtomic α

Full source

/-- A complemented modular coatomic lattice is strongly atomic.
Not an instance to prevent loops. -/
theorem ComplementedLattice.isStronglyCoatomic' [h : IsCoatomic α] : IsStronglyAtomic α := by
  rw [← isAtomic_iff_isCoatomic] at h
  exact isStronglyAtomic

Strong Atomicity from Coatomicity in Complemented Modular Lattices

Informal description

In a complemented modular lattice $\alpha$, if $\alpha$ is coatomic (i.e., every non-top element has a coatom above it), then $\alpha$ is strongly atomic (i.e., for any $a < b$ in $\alpha$, there exists an element $x$ such that $a \lessdot x \leq b$).

Prop.instIsSimpleOrderProp instance

: IsSimpleOrder Prop

Full source

instance : IsSimpleOrder Prop where
  eq_bot_or_eq_top p := by simp [em']

Propositions Form a Simple Order

Informal description

The set of propositions $\mathrm{Prop}$ forms a simple order, where the only elements are the least element $\bot$ (false) and the greatest element $\top$ (true).

Prop.isAtom_iff theorem

{p : Prop} : IsAtom p ↔ p

Full source

theorem isAtom_iff {p : Prop} : IsAtomIsAtom p ↔ p := by simp

Characterization of Atoms in Proposition Lattice: $p$ is an atom iff $p$ is true

Informal description

For any proposition $p$, $p$ is an atom in the lattice of propositions if and only if $p$ is true. In other words, the only atom in the lattice of propositions is the true proposition $\top$.

Prop.isCoatom_iff theorem

{p : Prop} : IsCoatom p ↔ ¬p

Full source

theorem isCoatom_iff {p : Prop} : IsCoatomIsCoatom p ↔ ¬ p := by simp

Characterization of Coatoms in Proposition Lattice: $p$ is a coatom iff $p$ is false

Informal description

For any proposition $p$, $p$ is a coatom in the lattice of propositions if and only if $p$ is false. In other words, the only coatom in the lattice of propositions is the false proposition $\bot$.

Pi.isAtom_iff theorem

 {f : ∀ i, π i} [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] : IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ j, j ≠ i → f j = ⊥

Full source

theorem isAtom_iff {f : ∀ i, π i} [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] :
    IsAtomIsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ j, j ≠ i → f j = ⊥ := by
  classical
  constructor
  case mpr =>
    rintro ⟨i, ⟨hfi, hlt⟩, hbot⟩
    refine ⟨fun h => hfi ((Pi.eq_bot_iff.1 h) _), fun g hgf => Pi.eq_bot_iff.2 fun j => ?_⟩
    have ⟨hgf, k, hgfk⟩ := Pi.lt_def.1 hgf
    obtain rfl : i = k := of_not_not fun hki => by rw [hbot _ (Ne.symm hki)] at hgfk; simp at hgfk
    if hij : j = i then subst hij; refine hlt _ hgfk else
    exact eq_bot_iff.2 <| le_trans (hgf _) (eq_bot_iff.1 (hbot _ hij))
  case mp =>
    rintro ⟨hbot, h⟩
    have ⟨i, hbot⟩ : ∃ i, f i ≠ ⊥ := by rw [ne_eq, Pi.eq_bot_iff, not_forall] at hbot; exact hbot
    refine ⟨i, ⟨hbot, ?c⟩, ?d⟩
    case c =>
      intro b hb
      have := h (Function.update ⊥ i b)
      simp only [lt_def, le_def, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
      simpa using this
        (fun j => by by_cases h : j = i; { subst h; simpa using le_of_lt hb }; simp [h])
        i (by simpa using hb) i
    case d =>
      intro j hj
      have := h (Function.update ⊥ j (f j))
      simp only [lt_def, le_def, Pi.eq_bot_iff, and_imp, forall_exists_index] at this
      simpa using this (fun k => by by_cases h : k = j; { subst h; simp }; simp [h]) i
        (by rwa [Function.update_of_ne (Ne.symm hj), bot_apply, bot_lt_iff_ne_bot]) j

Characterization of Atoms in Product Lattices

Informal description

For a function $f : \forall i, \pi_i$ in a product of partially ordered sets with bottom elements, $f$ is an atom if and only if there exists an index $i$ such that $f(i)$ is an atom in $\pi_i$ and for all other indices $j \neq i$, $f(j) = \bot$.

Pi.isAtom_single theorem

 {i : ι} [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] {a : π i} (h : IsAtom a) :
  IsAtom (Function.update (⊥ : ∀ i, π i) i a)

Full source

theorem isAtom_single {i : ι} [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)]
    {a : π i} (h : IsAtom a) : IsAtom (Function.update (⊥ : ∀ i, π i) i a) :=
  isAtom_iff.2 ⟨i, by simpa, fun _ hji => Function.update_of_ne hji ..⟩

Atom Construction in Product Lattices via Single Update

Informal description

Let $\{ \pi_i \}_{i \in \iota}$ be a family of partially ordered sets with bottom elements $\bot$, and let $a$ be an atom in $\pi_i$ for some index $i \in \iota$. Then the function $f : \forall i, \pi_i$ defined by updating the constant $\bot$ function at index $i$ with $a$ (i.e., $f = \text{update } \bot \, i \, a$) is an atom in the product lattice $\forall i, \pi_i$.

Pi.isAtom_iff_eq_single theorem

 [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] {f : ∀ i, π i} :
  IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Full source

theorem isAtom_iff_eq_single [DecidableEq ι] [∀ i, PartialOrder (π i)]
    [∀ i, OrderBot (π i)] {f : ∀ i, π i} :
    IsAtomIsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a := by
  constructor
  case mp =>
    intro h
    have ⟨i, h, hbot⟩ := isAtom_iff.1 h
    refine ⟨_, _, h, funext fun j => if hij : j = i then hij ▸ by simp else ?_⟩
    rw [Function.update_of_ne hij, hbot _ hij, bot_apply]
  case mpr =>
    rintro ⟨i, a, h, rfl⟩
    exact isAtom_single h

Characterization of Atoms in Product Lattices as Single Updates

Informal description

Let $\{ \pi_i \}_{i \in \iota}$ be a family of partially ordered sets with bottom elements $\bot$, and let $f : \forall i, \pi_i$ be a function. Then $f$ is an atom in the product lattice if and only if there exists an index $i \in \iota$ and an atom $a \in \pi_i$ such that $f$ is equal to the function obtained by updating the constant $\bot$ function at $i$ with $a$, i.e., $f = \text{update } \bot \, i \, a$.

Pi.isAtomic instance

[∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] [∀ i, IsAtomic (π i)] : IsAtomic (∀ i, π i)

Full source

instance isAtomic [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] [∀ i, IsAtomic (π i)] :
    IsAtomic (∀ i, π i) where
  eq_bot_or_exists_atom_le b := or_iff_not_imp_left.2 fun h =>
    have ⟨i, hi⟩ : ∃ i, b i ≠ ⊥ := not_forall.1 (h.imp Pi.eq_bot_iff.2)
    have ⟨a, ha, hab⟩ := (eq_bot_or_exists_atom_le (b i)).resolve_left hi
    have : DecidableEq ι := open scoped Classical in inferInstance
    ⟨Function.update ⊥ i a, isAtom_single ha, update_le_iff.2 ⟨hab, by simp⟩⟩

Atomicity of Product Lattices

Informal description

For any family of types $\{\pi_i\}_{i \in \iota}$ where each $\pi_i$ is a partially ordered set with a bottom element $\bot$ and is atomic (i.e., every element $x \neq \bot$ has an atom below it), the product lattice $\forall i, \pi_i$ is also atomic.

Pi.isCoatomic instance

[∀ i, PartialOrder (π i)] [∀ i, OrderTop (π i)] [∀ i, IsCoatomic (π i)] : IsCoatomic (∀ i, π i)

Full source

instance isCoatomic [∀ i, PartialOrder (π i)] [∀ i, OrderTop (π i)] [∀ i, IsCoatomic (π i)] :
    IsCoatomic (∀ i, π i) :=
  isAtomic_dual_iff_isCoatomic.1 <|
    show IsAtomic (∀ i, (π i)ᵒᵈ) from inferInstance

Coatomicity of Product Lattices

Informal description

For any family of partially ordered sets $\{\pi_i\}_{i \in \iota}$ where each $\pi_i$ has a greatest element $\top$ and is coatomic (i.e., every element $x \neq \top$ has a coatom above it), the product lattice $\forall i, \pi_i$ is also coatomic.

Pi.isAtomistic instance

[∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] [∀ i, IsAtomistic (π i)] : IsAtomistic (∀ i, π i)

Full source

instance isAtomistic [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] [∀ i, IsAtomistic (π i)] :
    IsAtomistic (∀ i, π i) where
  isLUB_atoms s := by
    classical
    refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
    rw [isLUB_pi]
    intro i
    simp_rw [isAtom_iff_eq_single]
    refine ⟨?_, ?_⟩
    · rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
      exact hs i
    · refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
      refine hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, fun j ↦ ?_⟩, by simp⟩
      obtain rfl | hij := eq_or_ne j i <;> simp [*]

Atomistic Structure on Product Lattices

Informal description

For any family of types $\pi_i$ each equipped with a partial order and a bottom element $\bot$, if each $\pi_i$ is an atomistic lattice (i.e., every element is the supremum of a set of atoms), then the product lattice $\forall i, \pi_i$ is also atomistic.

Pi.isCoatomistic instance

[∀ i, CompleteLattice (π i)] [∀ i, IsCoatomistic (π i)] : IsCoatomistic (∀ i, π i)

Full source

instance isCoatomistic [∀ i, CompleteLattice (π i)] [∀ i, IsCoatomistic (π i)] :
    IsCoatomistic (∀ i, π i) :=
  isAtomistic_dual_iff_isCoatomistic.1 <|
    show IsAtomistic (∀ i, (π i)ᵒᵈ) from inferInstance

Coatomistic Structure on Product Lattices

Informal description

For any family of complete lattices $(\pi_i)_{i \in \iota}$ where each $\pi_i$ is coatomistic (i.e., every element is the infimum of a set of coatoms), the product lattice $\forall i, \pi_i$ is also coatomistic.

isAtom_compl theorem

: IsAtom aᶜ ↔ IsCoatom a

Full source

@[simp] lemma isAtom_compl : IsAtomIsAtom aᶜ ↔ IsCoatom a := isCompl_compl.symm.isAtom_iff_isCoatom

Complement of Atom is Coatom in Boolean Algebra

Informal description

Let $a$ be an element in a Boolean algebra. The complement $a^\complement$ is an atom if and only if $a$ is a coatom.

isCoatom_compl theorem

: IsCoatom aᶜ ↔ IsAtom a

Full source

@[simp] lemma isCoatom_compl : IsCoatomIsCoatom aᶜ ↔ IsAtom a := isCompl_compl.symm.isCoatom_iff_isAtom

Complement Characterization: $a^\complement$ is a coatom iff $a$ is an atom

Informal description

In a Boolean algebra, the complement $a^\complement$ of an element $a$ is a coatom if and only if $a$ is an atom.

Set.isAtom_singleton theorem

(x : α) : IsAtom ({ x } : Set α)

Full source

theorem isAtom_singleton (x : α) : IsAtom ({x} : Set α) :=
  ⟨singleton_ne_empty _, fun _ hs => ssubset_singleton_iff.mp hs⟩

Singleton Sets are Atoms in Power Set Lattices

Informal description

For any element $x$ of a type $\alpha$, the singleton set $\{x\}$ is an atom in the power set lattice of $\alpha$. That is, $\{x\} \neq \emptyset$ and for any set $s \subset \{x\}$, we have $s = \emptyset$.

Set.isAtom_iff theorem

{s : Set α} : IsAtom s ↔ ∃ x, s = { x }

Full source

theorem isAtom_iff {s : Set α} : IsAtomIsAtom s ↔ ∃ x, s = {x} := by
  refine
    ⟨?_, by
      rintro ⟨x, rfl⟩
      exact isAtom_singleton x⟩
  rw [isAtom_iff_le_of_ge, bot_eq_empty, ← nonempty_iff_ne_empty]
  rintro ⟨⟨x, hx⟩, hs⟩
  exact
    ⟨x, eq_singleton_iff_unique_mem.2
        ⟨hx, fun y hy => (hs {y} (singleton_ne_empty _) (singleton_subset_iff.2 hy) hx).symm⟩⟩

Characterization of Atoms in Power Sets: $s$ is an atom iff $s$ is a singleton set

Informal description

A set $s$ in the power set of a type $\alpha$ is an atom if and only if there exists an element $x \in \alpha$ such that $s$ is the singleton set $\{x\}$.

Set.isCoatom_iff theorem

(s : Set α) : IsCoatom s ↔ ∃ x, s = { x }ᶜ

Full source

theorem isCoatom_iff (s : Set α) : IsCoatomIsCoatom s ↔ ∃ x, s = {x}ᶜ := by
  rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]
  simp_rw [@eq_comm _ s, compl_eq_comm]

Characterization of Coatoms in Power Sets: $s$ is a coatom iff $s$ is a complement of a singleton set

Informal description

A set $s$ in the power set of a type $\alpha$ is a coatom if and only if there exists an element $x \in \alpha$ such that $s$ is the complement of the singleton set $\{x\}$.

Set.isCoatom_singleton_compl theorem

(x : α) : IsCoatom ({ x }ᶜ : Set α)

Full source

theorem isCoatom_singleton_compl (x : α) : IsCoatom ({x}{x}ᶜ : Set α) :=
  (isCoatom_iff {x}{x}ᶜ).mpr ⟨x, rfl⟩

Complements of Singletons are Coatoms in Power Sets

Informal description

For any element $x$ of a type $\alpha$, the complement of the singleton set $\{x\}$ in the power set of $\alpha$ is a coatom. That is, $\{x\}^c$ is not equal to the universal set, and for any set $s$ strictly containing $\{x\}^c$, we must have $s$ equal to the universal set.

Set.instIsAtomistic instance

: IsAtomistic (Set α)

Full source

instance : IsAtomistic (Set α) := inferInstance

Atomistic Structure of Power Sets

Informal description

For any type $\alpha$, the power set $\mathcal{P}(\alpha)$ is an atomistic lattice, meaning every subset of $\alpha$ is the union of a set of atoms (which in this case are the singleton sets $\{x\}$ for $x \in \alpha$).

Set.instIsCoatomistic instance

: IsCoatomistic (Set α)

Full source

instance : IsCoatomistic (Set α) := inferInstance

The Power Set is Coatomistic

Informal description

For any type $\alpha$, the power set $\mathcal{P}(\alpha)$ is a coatomistic lattice, meaning every subset of $\alpha$ is the intersection of a set of coatoms (which in this case are the complements of singleton sets $\{x\}^c$ for $x \in \alpha$).

Mathlib.Order.Atoms

Main definitions

Atoms and Coatoms

Atomic and Atomistic Lattices

Simple Lattices

Main results