order.atoms

# Atoms, Coatoms, and Simple Lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module defines atoms, which are minimal non-⊥ elements in bounded lattices, simple lattices, which are lattices with only two elements, and related ideas.

## Main definitions #

### Atoms and Coatoms #

• is_atom a indicates that the only element below a is ⊥.
• is_coatom a indicates that the only element above a is ⊤.

### Atomic and Atomistic Lattices #

• is_atomic indicates that every element other than ⊥ is above an atom.
• is_coatomic indicates that every element other than ⊤ is below a coatom.
• is_atomistic indicates that every element is the Sup of a set of atoms.
• is_coatomistic indicates that every element is the Inf of a set of coatoms.

### Simple Lattices #

• is_simple_order indicates that an order has only two unique elements, ⊥ and ⊤.
• is_simple_order.bounded_order
• is_simple_order.distrib_lattice
• Given an instance of is_simple_order, we provide the following definitions. These are not made global instances as they contain data :
• is_simple_order.boolean_algebra
• is_simple_order.complete_lattice
• is_simple_order.complete_boolean_algebra

## Main results #

• is_atom_dual_iff_is_coatom and is_coatom_dual_iff_is_atom express the (definitional) duality of is_atom and is_coatom.
• is_simple_order_iff_is_atom_top and is_simple_order_iff_is_coatom_bot express the connection between atoms, coatoms, and simple lattices
• is_compl.is_atom_iff_is_coatom and is_compl.is_coatom_if_is_atom: In a modular bounded lattice, a complement of an atom is a coatom and vice versa.
• is_atomic_iff_is_coatomic: A modular complemented lattice is atomic iff it is coatomic.
def is_atom {α : Type u_1} [preorder α] [order_bot α] (a : α) :
Prop

An atom of an order_bot is an element with no other element between it and ⊥, which is not ⊥.

Equations
theorem is_atom.Iic {α : Type u_1} [preorder α] [order_bot α] {a x : α} (ha : is_atom a) (hax : a x) :
is_atom a, hax⟩
theorem is_atom.of_is_atom_coe_Iic {α : Type u_1} [preorder α] [order_bot α] {x : α} {a : (set.Iic x)} (ha : is_atom a) :
theorem is_atom_iff {α : Type u_1} [preorder α] [order_bot α] {a : α} :
a (b : α), b b a a b
theorem is_atom.lt_iff {α : Type u_1} [order_bot α] {a x : α} (h : is_atom a) :
x < a x =
theorem is_atom.le_iff {α : Type u_1} [order_bot α] {a x : α} (h : is_atom a) :
x a x = x = a
theorem is_atom.Iic_eq {α : Type u_1} [order_bot α] {a : α} (h : is_atom a) :
= {, a}
@[simp]
theorem bot_covby_iff {α : Type u_1} [order_bot α] {a : α} :
theorem covby.is_atom {α : Type u_1} [order_bot α] {a : α} :

Alias of the forward direction of bot_covby_iff.

theorem is_atom.bot_covby {α : Type u_1} [order_bot α] {a : α} :

Alias of the reverse direction of bot_covby_iff.

def is_coatom {α : Type u_1} [preorder α] [order_top α] (a : α) :
Prop

A coatom of an order_top is an element with no other element between it and ⊤, which is not ⊤.

Equations
@[simp]
theorem is_coatom_dual_iff_is_atom {α : Type u_1} [preorder α] [order_bot α] {a : α} :
@[simp]
theorem is_atom_dual_iff_is_coatom {α : Type u_1} [preorder α] [order_top α] {a : α} :
theorem is_atom.dual {α : Type u_1} [preorder α] [order_bot α] {a : α} :

Alias of the reverse direction of is_coatom_dual_iff_is_atom.

theorem is_coatom.dual {α : Type u_1} [preorder α] [order_top α] {a : α} :

Alias of the reverse direction of is_atom_dual_iff_is_coatom.

theorem is_coatom.Ici {α : Type u_1} [preorder α] [order_top α] {a x : α} (ha : is_coatom a) (hax : x a) :
is_coatom a, hax⟩
theorem is_coatom.of_is_coatom_coe_Ici {α : Type u_1} [preorder α] [order_top α] {x : α} {a : (set.Ici x)} (ha : is_coatom a) :
theorem is_coatom_iff {α : Type u_1} [preorder α] [order_top α] {a : α} :
a (b : α), b a b b a
theorem is_coatom.lt_iff {α : Type u_1} [order_top α] {a x : α} (h : is_coatom a) :
a < x x =
theorem is_coatom.le_iff {α : Type u_1} [order_top α] {a x : α} (h : is_coatom a) :
a x x = x = a
theorem is_coatom.Ici_eq {α : Type u_1} [order_top α] {a : α} (h : is_coatom a) :
= {, a}
@[simp]
theorem covby_top_iff {α : Type u_1} [order_top α] {a : α} :
theorem covby.is_coatom {α : Type u_1} [order_top α] {a : α} :

Alias of the forward direction of covby_top_iff.

theorem is_coatom.covby_top {α : Type u_1} [order_top α] {a : α} :

Alias of the reverse direction of covby_top_iff.

@[simp]
theorem set.Ici.is_atom_iff {α : Type u_1} {a : α} {b : (set.Ici a)} :
a b
@[simp]
theorem set.Iic.is_coatom_iff {α : Type u_1} {b : α} {a : (set.Iic b)} :
a b
theorem covby_iff_atom_Ici {α : Type u_1} {a b : α} (h : a b) :
a b is_atom b, h⟩
theorem covby_iff_coatom_Iic {α : Type u_1} {a b : α} (h : a b) :
a b is_coatom a, h⟩
theorem is_atom.inf_eq_bot_of_ne {α : Type u_1} [order_bot α] {a b : α} (ha : is_atom a) (hb : is_atom b) (hab : a b) :
a b =
theorem is_atom.disjoint_of_ne {α : Type u_1} [order_bot α] {a b : α} (ha : is_atom a) (hb : is_atom b) (hab : a b) :
b
theorem is_coatom.sup_eq_top_of_ne {α : Type u_1} [order_top α] {a b : α} (ha : is_coatom a) (hb : is_coatom b) (hab : a b) :
a b =
@[class]
structure is_atomic (α : Type u_1) [order_bot α] :
Prop

A lattice is atomic iff every element other than ⊥ has an atom below it.

Instances of this typeclass
theorem is_atomic_iff (α : Type u_1) [order_bot α] :
(b : α), b = (a : α), a b
@[class]
structure is_coatomic (α : Type u_1) [order_top α] :
Prop

A lattice is coatomic iff every element other than ⊤ has a coatom above it.

Instances of this typeclass
theorem is_coatomic_iff (α : Type u_1) [order_top α] :
(b : α), b = (a : α), b a
@[simp]
theorem is_coatomic_dual_iff_is_atomic {α : Type u_1} [order_bot α] :
@[simp]
theorem is_atomic_dual_iff_is_coatomic {α : Type u_1} [order_top α] :
@[protected, instance]
def is_atomic.is_coatomic_dual {α : Type u_1} [order_bot α] [is_atomic α] :
@[protected, instance]
def is_atomic.set.Iic.is_atomic {α : Type u_1} [order_bot α] [is_atomic α] {x : α} :
@[protected, instance]
def is_coatomic.is_coatomic {α : Type u_1} [order_top α] [is_coatomic α] :
@[protected, instance]
def is_coatomic.set.Ici.is_coatomic {α : Type u_1} [order_top α] [is_coatomic α] {x : α} :
theorem is_atomic_iff_forall_is_atomic_Iic {α : Type u_1} [order_bot α] :
(x : α),
theorem is_coatomic_iff_forall_is_coatomic_Ici {α : Type u_1} [order_top α] :
(x : α),
@[class]
structure is_atomistic (α : Type u_1)  :
Prop

A lattice is atomistic iff every element is a Sup of a set of atoms.

Instances of this typeclass
@[class]
structure is_coatomistic (α : Type u_1)  :
Prop

A lattice is coatomistic iff every element is an Inf of a set of coatoms.

Instances of this typeclass
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
def is_atomistic.is_atomic {α : Type u_1} [is_atomistic α] :
@[simp]
theorem Sup_atoms_le_eq {α : Type u_1} [is_atomistic α] (b : α) :
has_Sup.Sup {a : α | a b} = b
@[simp]
theorem Sup_atoms_eq_top {α : Type u_1} [is_atomistic α] :
has_Sup.Sup {a : α | is_atom a} =
theorem le_iff_atom_le_imp {α : Type u_1} [is_atomistic α] {a b : α} :
a b (c : α), c a c b
@[protected, instance]
@[protected, instance]
def is_coatomistic.is_coatomic {α : Type u_1}  :
@[class]
structure is_simple_order (α : Type u_3) [has_le α]  :
Prop
• to_nontrivial :
• eq_bot_or_eq_top : (a : α), a = a =

An order is simple iff it has exactly two elements, ⊥ and ⊤.

Instances of this typeclass
theorem is_simple_order.bot_ne_top {α : Type u_1} [has_le α]  :
@[protected, instance]
def order_dual.is_simple_order {α : Type u_1} [has_le α]  :
@[protected]
def is_simple_order.preorder {α : Type u_1} [has_le α]  :

A simple bounded_order induces a preorder. This is not an instance to prevent loops.

Equations
@[protected]

A simple partial ordered bounded_order induces a linear order. This is not an instance to prevent loops.

Equations
@[simp]
theorem is_atom_top {α : Type u_1}  :
@[simp]
theorem is_coatom_bot {α : Type u_1}  :
theorem bot_covby_top {α : Type u_1}  :
theorem is_simple_order.eq_bot_of_lt {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
a =
theorem is_simple_order.eq_top_of_lt {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
b =
theorem is_simple_order.has_lt.lt.eq_bot {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
a =

Alias of is_simple_order.eq_bot_of_lt.

theorem is_simple_order.has_lt.lt.eq_top {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
b =

Alias of is_simple_order.eq_top_of_lt.

@[protected]
def is_simple_order.lattice {α : Type u_1} [decidable_eq α]  :

A simple partial ordered bounded_order induces a lattice. This is not an instance to prevent loops

Equations
@[protected]
def is_simple_order.distrib_lattice {α : Type u_1} [lattice α]  :

A lattice that is a bounded_order is a distributive lattice. This is not an instance to prevent loops

Equations
@[protected, instance]
def is_simple_order.is_atomic {α : Type u_1} [lattice α]  :
@[protected, instance]
def is_simple_order.is_coatomic {α : Type u_1} [lattice α]  :
@[simp]
theorem is_simple_order.equiv_bool_symm_apply {α : Type u_1} [decidable_eq α] [has_le α] (x : bool) :
@[simp]
theorem is_simple_order.equiv_bool_apply {α : Type u_1} [decidable_eq α] [has_le α] (x : α) :
def is_simple_order.equiv_bool {α : Type u_1} [decidable_eq α] [has_le α]  :

Every simple lattice is isomorphic to bool, regardless of order.

Equations

Every simple lattice over a partial order is order-isomorphic to bool.

Equations
@[protected]

A simple bounded_order is also a boolean_algebra.

Equations
@[protected]
noncomputable def is_simple_order.complete_lattice {α : Type u_1} [lattice α]  :

A simple bounded_order is also complete.

Equations
@[protected]
noncomputable def is_simple_order.complete_boolean_algebra {α : Type u_1} [lattice α]  :

A simple bounded_order is also a complete_boolean_algebra.

Equations
@[protected, instance]
def is_simple_order.is_atomistic {α : Type u_1}  :
@[protected, instance]
theorem set.is_simple_order_Iic_iff_is_atom {α : Type u_1} [order_bot α] {a : α} :
theorem set.is_simple_order_Ici_iff_is_coatom {α : Type u_1} [order_top α] {a : α} :
theorem order_embedding.is_atom_of_map_bot_of_image {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] (f : β ↪o α) (hbot : f = ) {b : β} (hb : is_atom (f b)) :
theorem order_embedding.is_coatom_of_map_top_of_image {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] (f : β ↪o α) (htop : f = ) {b : β} (hb : is_coatom (f b)) :
theorem galois_insertion.is_atom_of_u_bot {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] {l : α β} {u : β α} (gi : u) (hbot : u = ) {b : β} (hb : is_atom (u b)) :
theorem galois_insertion.is_atom_iff {α : Type u_1} {β : Type u_2} [order_bot α] [is_atomic α] [order_bot β] {l : α β} {u : β α} (gi : u) (hbot : u = ) (h_atom : (a : α), u (l a) = a) (a : α) :
is_atom (l a)
theorem galois_insertion.is_atom_iff' {α : Type u_1} {β : Type u_2} [order_bot α] [is_atomic α] [order_bot β] {l : α β} {u : β α} (gi : u) (hbot : u = ) (h_atom : (a : α), u (l a) = a) (b : β) :
is_atom (u b)
theorem galois_insertion.is_coatom_of_image {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] {l : α β} {u : β α} (gi : u) {b : β} (hb : is_coatom (u b)) :
theorem galois_insertion.is_coatom_iff {α : Type u_1} {β : Type u_2} [order_top α] [is_coatomic α] [order_top β] {l : α β} {u : β α} (gi : u) (h_coatom : (a : α), u (l a) = a) (b : β) :
is_coatom (u b)
theorem galois_coinsertion.is_coatom_of_l_top {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] {l : α β} {u : β α} (gi : u) (hbot : l = ) {a : α} (hb : is_coatom (l a)) :
theorem galois_coinsertion.is_coatom_iff {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] [is_coatomic β] {l : α β} {u : β α} (gi : u) (htop : l = ) (h_coatom : (b : β), l (u b) = b) (b : β) :
is_coatom (u b)
theorem galois_coinsertion.is_coatom_iff' {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] [is_coatomic β] {l : α β} {u : β α} (gi : u) (htop : l = ) (h_coatom : (b : β), l (u b) = b) (a : α) :
is_coatom (l a)
theorem galois_coinsertion.is_atom_of_image {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] {l : α β} {u : β α} (gi : u) {a : α} (hb : is_atom (l a)) :
theorem galois_coinsertion.is_atom_iff {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] [is_atomic β] {l : α β} {u : β α} (gi : u) (h_atom : (b : β), l (u b) = b) (a : α) :
is_atom (l a)
@[simp]
theorem order_iso.is_atom_iff {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] (f : α ≃o β) (a : α) :
@[simp]
theorem order_iso.is_coatom_iff {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] (f : α ≃o β) (a : α) :
theorem order_iso.is_simple_order_iff {α : Type u_1} {β : Type u_2} (f : α ≃o β) :
theorem order_iso.is_simple_order {α : Type u_1} {β : Type u_2} [h : is_simple_order β] (f : α ≃o β) :
@[protected]
theorem order_iso.is_atomic_iff {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] (f : α ≃o β) :
@[protected]
theorem order_iso.is_coatomic_iff {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] (f : α ≃o β) :
theorem is_compl.is_atom_iff_is_coatom {α : Type u_1} [lattice α] {a b : α} (hc : b) :
theorem is_compl.is_coatom_iff_is_atom {α : Type u_1} [lattice α] {a b : α} (hc : b) :
theorem is_atomic_iff_is_coatomic {α : Type u_1} [lattice α]  :
theorem set.is_atom_singleton {α : Type u_1} (x : α) :
theorem set.is_atom_iff {α : Type u_1} (s : set α) :
(x : α), s = {x}
theorem set.is_coatom_iff {α : Type u_1} (s : set α) :
(x : α), s = {x}
theorem set.is_coatom_singleton_compl {α : Type u_1} (x : α) :
@[protected, instance]
def set.is_atomistic {α : Type u_1} :
@[protected, instance]
def set.is_coatomistic {α : Type u_1} :