mathlib documentation

order.atoms

Atoms, Coatoms, and Simple Lattices #

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 #

Atomic and Atomistic Lattices #

Simple Lattices #

Main results #

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 eq_bot_or_eq_of_le_atom {α : Type u_1} [partial_order α] [order_bot α] {a b : α} (ha : is_atom a) (hab : b a) :
b = b = a
theorem is_atom.Iic {α : Type u_1} [partial_order α] [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} [partial_order α] [order_bot α] {x : α} {a : (set.Iic x)} (ha : is_atom a) :
@[simp]
theorem bot_covby_iff {α : Type u_1} [partial_order α] [order_bot α] {a : α} :
theorem covby.is_atom {α : Type u_1} [partial_order α] [order_bot α] {a : α} :
ais_atom a

Alias of the forward direction of bot_covby_iff`.

theorem is_atom.bot_covby {α : Type u_1} [partial_order α] [order_bot α] {a : α} :
is_atom a 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
theorem eq_top_or_eq_of_coatom_le {α : Type u_1} [partial_order α] [order_top α] {a b : α} (ha : is_coatom a) (hab : a b) :
b = b = a
theorem is_coatom.Ici {α : Type u_1} [partial_order α] [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} [partial_order α] [order_top α] {x : α} {a : (set.Ici x)} (ha : is_coatom a) :
@[simp]
theorem covby_top_iff {α : Type u_1} [partial_order α] [order_top α] {a : α} :
theorem covby.is_coatom {α : Type u_1} [partial_order α] [order_top α] {a : α} :
a is_coatom a

Alias of the forward direction of covby_top_iff`.

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

Alias of the reverse direction of covby_top_iff`.

theorem is_atom.inf_eq_bot_of_ne {α : Type u_1} [semilattice_inf α] [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} [semilattice_inf α] [order_bot α] {a b : α} (ha : is_atom a) (hb : is_atom b) (hab : a b) :
theorem is_coatom.sup_eq_top_of_ne {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} (ha : is_coatom a) (hb : is_coatom b) (hab : a b) :
a b =
@[simp]
theorem is_coatom_dual_iff_is_atom {α : Type u_1} [preorder α] {a : α} [order_bot α] :
@[simp]
theorem is_atom_dual_iff_is_coatom {α : Type u_1} [preorder α] {a : α} [order_top α] :
@[class]
structure is_atomic (α : Type u_1) [partial_order α] [order_bot α] :
Prop

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

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

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

Instances of this typeclass
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
def is_atomic.set.Iic.is_atomic {α : Type u_1} [partial_order α] [order_bot α] [is_atomic α] {x : α} :
@[protected, instance]
@[protected, instance]
def is_coatomic.set.Ici.is_coatomic {α : Type u_1} [partial_order α] [order_top α] [is_coatomic α] {x : α} :
theorem is_atomic_iff_forall_is_atomic_Iic {α : Type u_1} [partial_order α] [order_bot α] :
is_atomic α ∀ (x : α), is_atomic (set.Iic x)
@[class]
structure is_atomistic (α : Type u_1) [complete_lattice α] :
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) [complete_lattice α] :
Prop

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
def is_atomistic.is_atomic {α : Type u_1} [complete_lattice α] [is_atomistic α] :
@[simp]
theorem Sup_atoms_le_eq {α : Type u_1} [complete_lattice α] [is_atomistic α] (b : α) :
has_Sup.Sup {a : α | is_atom a a b} = b
@[simp]
theorem Sup_atoms_eq_top {α : Type u_1} [complete_lattice α] [is_atomistic α] :
has_Sup.Sup {a : α | is_atom a} =
theorem le_iff_atom_le_imp {α : Type u_1} [complete_lattice α] [is_atomistic α] {a b : α} :
a b ∀ (c : α), is_atom cc ac b
@[protected, instance]
@[protected, instance]
@[class]
structure is_simple_order (α : Type u_2) [has_le α] [bounded_order α] :
Prop

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 α] [bounded_order α] [is_simple_order α] :
@[protected, instance]
@[protected]
def is_simple_order.preorder {α : Type u_1} [has_le α] [bounded_order α] [is_simple_order α] :

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} [partial_order α] [bounded_order α] [is_simple_order α] :
@[simp]
theorem is_coatom_bot {α : Type u_1} [partial_order α] [bounded_order α] [is_simple_order α] :
theorem bot_covby_top {α : Type u_1} [partial_order α] [bounded_order α] [is_simple_order α] :
theorem is_simple_order.eq_bot_of_lt {α : Type u_1} [preorder α] [bounded_order α] [is_simple_order α] {a b : α} (h : a < b) :
a =
theorem is_simple_order.eq_top_of_lt {α : Type u_1} [preorder α] [bounded_order α] [is_simple_order α] {a b : α} (h : a < b) :
b =
theorem has_lt.lt.eq_bot {α : Type u_1} [preorder α] [bounded_order α] [is_simple_order α] {a b : α} (h : a < b) :
a =

Alias of is_simple_order.eq_bot_of_lt`.

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

Alias of is_simple_order.eq_top_of_lt`.

@[protected]

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

Equations
@[protected]

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 α] [bounded_order α] [is_simple_order α] :
@[protected, instance]
def is_simple_order.equiv_bool {α : Type u_1} [decidable_eq α] [has_le α] [bounded_order α] [is_simple_order α] :

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, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem order_iso.is_atom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [order_bot α] [partial_order β] [order_bot β] (f : α ≃o β) (a : α) :
@[simp]
theorem order_iso.is_coatom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [order_top α] [partial_order β] [order_top β] (f : α ≃o β) (a : α) :
theorem order_iso.is_simple_order_iff {α : Type u_1} {β : Type u_2} [partial_order α] [bounded_order α] [partial_order β] [bounded_order β] (f : α ≃o β) :
theorem order_iso.is_simple_order {α : Type u_1} {β : Type u_2} [partial_order α] [bounded_order α] [partial_order β] [bounded_order β] [h : is_simple_order β] (f : α ≃o β) :
theorem order_iso.is_atomic_iff {α : Type u_1} {β : Type u_2} [partial_order α] [order_bot α] [partial_order β] [order_bot β] (f : α ≃o β) :
theorem order_iso.is_coatomic_iff {α : Type u_1} {β : Type u_2} [partial_order α] [order_top α] [partial_order β] [order_top β] (f : α ≃o β) :
theorem is_compl.is_atom_iff_is_coatom {α : Type u_1} [lattice α] [bounded_order α] [is_modular_lattice α] {a b : α} (hc : is_compl a b) :
theorem is_compl.is_coatom_iff_is_atom {α : Type u_1} [lattice α] [bounded_order α] [is_modular_lattice α] {a b : α} (hc : is_compl a b) :
@[protected, instance]
def fintype.to_is_coatomic {α : Type u_1} [partial_order α] [order_top α] [fintype α] :
@[protected, instance]
def fintype.to_is_atomic {α : Type u_1} [partial_order α] [order_bot α] [fintype α] :