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 #

IsAtom a indicates that the only element below a is ⊥.
IsCoatom a indicates that the only element above a is ⊤.

Atomic and Atomistic Lattices #

IsAtomic indicates that every element other than ⊥ is above an atom.
IsCoatomic indicates that every element other than ⊤ is below a coatom.
IsAtomistic indicates that every element is the supₛ of a set of atoms.
IsCoatomistic indicates that every element is the infₛ of a set of coatoms.

Simple Lattices #

IsSimpleOrder indicates that an order has only two unique elements, ⊥ and ⊤.
IsSimpleOrder.boundedOrder
IsSimpleOrder.distribLattice
Given an instance of IsSimpleOrder, we provide the following definitions. These are not made global instances as they contain data :

Main results #

isAtom_dual_iff_isCoatom and isCoatom_dual_iff_isAtom express the (definitional) duality of IsAtom and IsCoatom.
isSimpleOrder_iff_isAtom_top and isSimpleOrder_iff_isCoatom_bot express the connection between atoms, coatoms, and simple lattices
IsCompl.isAtom_iff_isCoatom and IsCompl.isCoatom_if_isAtom: In a modular bounded lattice, a complement of an atom is a coatom and vice versa.
isAtomic_iff_isCoatomic: A modular complemented lattice is atomic iff it is coatomic.

source

ink

def IsAtom {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] (a : α) :

Prop

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

Equations

IsAtom a = (a ≠ ⊥ ∧ ∀ (b : α), b < a → b = ⊥)

source

ink

theorem IsAtom.Iic {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} {x : α} (ha : IsAtom a) (hax : a ≤ x) :

IsAtom { val := a, property := hax }

source

ink

theorem IsAtom.of_isAtom_coe_Iic {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {x : α} {a : ↑(Set.Iic x)} (ha : IsAtom a) :

IsAtom ↑a

source

ink

theorem isAtom_iff {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :

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

source

ink

theorem IsAtom.lt_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {x : α} (h : IsAtom a) :

x < a ↔ x = ⊥

source

ink

theorem IsAtom.le_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {x : α} (h : IsAtom a) :

x ≤ a ↔ x = ⊥ ∨ x = a

source

ink

theorem IsAtom.Iic_eq {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} (h : IsAtom a) :

Set.Iic a = {⊥, a}

source

ink

@[simp]

theorem bot_covby_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

⊥ ⋖ a ↔ IsAtom a

source

ink

theorem Covby.is_atom {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

⊥ ⋖ a → IsAtom a

Alias of the forward direction of bot_covby_iff.

source

ink

theorem IsAtom.bot_covby {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

IsAtom a → ⊥ ⋖ a

Alias of the reverse direction of bot_covby_iff.

source

ink

def IsCoatom {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] (a : α) :

Prop

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

Equations

IsCoatom a = (a ≠ ⊤ ∧ ∀ (b : α), a < b → b = ⊤)

source

ink

@[simp]

theorem isCoatom_dual_iff_isAtom {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :

IsCoatom (↑OrderDual.toDual a) ↔ IsAtom a

source

ink

@[simp]

theorem isAtom_dual_iff_isCoatom {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :

IsAtom (↑OrderDual.toDual a) ↔ IsCoatom a

source

ink

theorem IsAtom.dual {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :

IsAtom a → IsCoatom (↑OrderDual.toDual a)

Alias of the reverse direction of isCoatom_dual_iff_isAtom.

source

ink

theorem IsCoatom.dual {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :

IsCoatom a → IsAtom (↑OrderDual.toDual a)

Alias of the reverse direction of isAtom_dual_iff_isCoatom.

source

ink

theorem IsCoatom.Ici {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} {x : α} (ha : IsCoatom a) (hax : x ≤ a) :

IsCoatom { val := a, property := hax }

source

ink

theorem IsCoatom.of_isCoatom_coe_Ici {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {x : α} {a : ↑(Set.Ici x)} (ha : IsCoatom a) :

IsCoatom ↑a

source

ink

theorem isCoatom_iff {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :

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

source

ink

theorem IsCoatom.lt_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {x : α} (h : IsCoatom a) :

a < x ↔ x = ⊤

source

ink

theorem IsCoatom.le_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {x : α} (h : IsCoatom a) :

a ≤ x ↔ x = ⊤ ∨ x = a

source

ink

theorem IsCoatom.Ici_eq {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} (h : IsCoatom a) :

Set.Ici a = {⊤, a}

source

ink

@[simp]

theorem covby_top_iff {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

a ⋖ ⊤ ↔ IsCoatom a

source

ink

theorem Covby.is_coatom {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

a ⋖ ⊤ → IsCoatom a

Alias of the forward direction of covby_top_iff.

source

ink

theorem IsCoatom.covby_top {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

IsCoatom a → a ⋖ ⊤

Alias of the reverse direction of covby_top_iff.

source

ink

@[simp]

theorem Set.Ici.isAtom_iff {α : Type u_1} [inst : PartialOrder α] {a : α} {b : ↑(Set.Ici a)} :

IsAtom b ↔ a ⋖ ↑b

source

ink

@[simp]

theorem Set.Iic.isCoatom_iff {α : Type u_1} [inst : PartialOrder α] {b : α} {a : ↑(Set.Iic b)} :

IsCoatom a ↔ ↑a ⋖ b

source

ink

theorem covby_iff_atom_Ici {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a ⋖ b ↔ IsAtom { val := b, property := h }

source

ink

theorem covby_iff_coatom_Iic {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a ⋖ b ↔ IsCoatom { val := a, property := h }

source

ink

theorem IsAtom.inf_eq_bot_of_ne {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) :

a ⊓ b = ⊥

source

ink

theorem IsAtom.disjoint_of_ne {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) :

Disjoint a b

source

ink

theorem IsCoatom.sup_eq_top_of_ne {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) :

a ⊔ b = ⊤

source

ink

theorem IsAtomic_iff (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] :

IsAtomic α ↔ ∀ (b : α), b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

source

ink

class IsAtomic (α : Type u_1) [inst : PartialOrder α] [inst : OrderBot α] :

Prop

Every element other than ⊥ has an atom below it.
eq_bot_or_exists_atom_le : ∀ (b : α), b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

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

Instances

source

ink

theorem IsCoatomic_iff (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] :

IsCoatomic α ↔ ∀ (b : α), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

source

ink

class IsCoatomic (α : Type u_1) [inst : PartialOrder α] [inst : OrderTop α] :

Prop

Every element other than ⊤ has an atom above it.
eq_top_or_exists_le_coatom : ∀ (b : α), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

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

Instances

source

ink

@[simp]

theorem isCoatomic_dual_iff_isAtomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] :

IsCoatomic αᵒᵈ ↔ IsAtomic α

source

ink

@[simp]

theorem isAtomic_dual_iff_isCoatomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] :

IsAtomic αᵒᵈ ↔ IsCoatomic α

source

ink

instance IsAtomic.isCoatomic_dual {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] [inst : IsAtomic α] :

IsCoatomic αᵒᵈ

Equations

@IsAtomic.isCoatomic_dual = @IsAtomic.isCoatomic_dual.proof_1

source

ink

instance IsAtomic.Set.Iic.isAtomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] [inst : IsAtomic α] {x : α} :

IsAtomic ↑(Set.Iic x)

Equations

@IsAtomic.Set.Iic.isAtomic = @IsAtomic.Set.Iic.isAtomic.proof_1

source

ink

instance IsCoatomic.isCoatomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] [inst : IsCoatomic α] :

IsAtomic αᵒᵈ

Equations

@IsCoatomic.isCoatomic = @IsCoatomic.isCoatomic.proof_1

source

ink

instance IsCoatomic.Set.Ici.isCoatomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] [inst : IsCoatomic α] {x : α} :

IsCoatomic ↑(Set.Ici x)

Equations

@IsCoatomic.Set.Ici.isCoatomic = @IsCoatomic.Set.Ici.isCoatomic.proof_1

source

ink

theorem isAtomic_iff_forall_isAtomic_Iic {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] :

IsAtomic α ↔ ∀ (x : α), IsAtomic ↑(Set.Iic x)

source

ink

theorem isCoatomic_iff_forall_isCoatomic_Ici {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] :

IsCoatomic α ↔ ∀ (x : α), IsCoatomic ↑(Set.Ici x)

source

ink

theorem isAtomic_of_orderBot_wellFounded_lt {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] (h : WellFounded fun x x_1 => x < x_1) :

IsAtomic α

source

ink

theorem isCoatomic_of_orderTop_gt_wellFounded {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] (h : WellFounded fun x x_1 => x > x_1) :

IsCoatomic α

source

ink

class IsAtomistic (α : Type u_1) [inst : CompleteLattice α] :

Prop

Every element is a supₛ of a set of atoms.
eq_supₛ_atoms : ∀ (b : α), ∃ s, b = supₛ s ∧ ∀ (a : α), a ∈ s → IsAtom a

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

Instances

source

ink

class IsCoatomistic (α : Type u_1) [inst : CompleteLattice α] :

Prop

Every element is a infₛ of a set of coatoms.
eq_infₛ_coatoms : ∀ (b : α), ∃ s, b = infₛ s ∧ ∀ (a : α), a ∈ s → IsCoatom a

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

Instances

source

ink

@[simp]

theorem isCoatomistic_dual_iff_isAtomistic {α : Type u_1} [inst : CompleteLattice α] :

IsCoatomistic αᵒᵈ ↔ IsAtomistic α

source

ink

@[simp]

theorem isAtomistic_dual_iff_isCoatomistic {α : Type u_1} [inst : CompleteLattice α] :

IsAtomistic αᵒᵈ ↔ IsCoatomistic α

source

ink

instance IsAtomistic.isCoatomistic_dual {α : Type u_1} [inst : CompleteLattice α] [h : IsAtomistic α] :

IsCoatomistic αᵒᵈ

Equations

@IsAtomistic.isCoatomistic_dual = @IsAtomistic.isCoatomistic_dual.proof_1

source

ink

instance IsAtomistic.instIsAtomicToPartialOrderToCompleteSemilatticeInfToOrderBotToLEToPreorderToBoundedOrder {α : Type u_1} [inst : CompleteLattice α] [inst : IsAtomistic α] :

IsAtomic α

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem supₛ_atoms_le_eq {α : Type u_1} [inst : CompleteLattice α] [inst : IsAtomistic α] (b : α) :

supₛ { a | IsAtom a ∧ a ≤ b } = b

source

ink

@[simp]

theorem supₛ_atoms_eq_top {α : Type u_1} [inst : CompleteLattice α] [inst : IsAtomistic α] :

supₛ { a | IsAtom a } = ⊤

source

ink

theorem le_iff_atom_le_imp {α : Type u_1} [inst : CompleteLattice α] [inst : IsAtomistic α] {a : α} {b : α} :

a ≤ b ↔ ∀ (c : α), IsAtom c → c ≤ a → c ≤ b

source

ink

instance IsCoatomistic.isAtomistic_dual {α : Type u_1} [inst : CompleteLattice α] [h : IsCoatomistic α] :

IsAtomistic αᵒᵈ

Equations

@IsCoatomistic.isAtomistic_dual = @IsCoatomistic.isAtomistic_dual.proof_1

source

ink

instance IsCoatomistic.instIsCoatomicToPartialOrderToCompleteSemilatticeInfToOrderTopToLEToPreorderToBoundedOrder {α : Type u_1} [inst : CompleteLattice α] [inst : IsCoatomistic α] :

IsCoatomic α

Equations

One or more equations did not get rendered due to their size.

source

ink

class IsSimpleOrder (α : Type u_1) [inst : LE α] [inst : BoundedOrder α] extends Nontrivial :

Prop

Every element is either ⊥ or ⊤
eq_bot_or_eq_top : ∀ (a : α), a = ⊥ ∨ a = ⊤

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

Instances

source

ink

theorem isSimpleOrder_iff_isSimpleOrder_orderDual {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] :

IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ

source

ink

theorem IsSimpleOrder.bot_ne_top {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

⊥ ≠ ⊤

source

ink

instance instIsSimpleOrderOrderDualInstLEOrderDualBoundedOrder {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

IsSimpleOrder αᵒᵈ

Equations

@instIsSimpleOrderOrderDualInstLEOrderDualBoundedOrder = @instIsSimpleOrderOrderDualInstLEOrderDualBoundedOrder.proof_1

source

ink

def IsSimpleOrder.preorder {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

Preorder α

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

Equations

IsSimpleOrder.preorder = Preorder.mk (_ : ∀ (a : α), a ≤ a) (_ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)

source

ink

def IsSimpleOrder.linearOrder {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] [inst : DecidableEq α] :

LinearOrder α

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

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem isAtom_top {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

IsAtom ⊤

source

ink

@[simp]

theorem isCoatom_bot {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

IsCoatom ⊥

source

ink

theorem bot_covby_top {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

⊥ ⋖ ⊤

source

ink

theorem IsSimpleOrder.eq_bot_of_lt {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] {a : α} {b : α} (h : a < b) :

a = ⊥

source

ink

theorem IsSimpleOrder.eq_top_of_lt {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] {a : α} {b : α} (h : a < b) :

b = ⊤

source

ink

theorem IsSimpleOrder.LT.lt.eq_bot {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] {a : α} {b : α} (h : a < b) :

a = ⊥

Alias of IsSimpleOrder.eq_bot_of_lt.

source

ink

theorem IsSimpleOrder.LT.lt.eq_top {α : Type u_1} [inst : Preorder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] {a : α} {b : α} (h : a < b) :

b = ⊤

Alias of IsSimpleOrder.eq_top_of_lt.

source

ink

def IsSimpleOrder.lattice {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

Lattice α

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

Equations

IsSimpleOrder.lattice = LinearOrder.toLattice

source

ink

def IsSimpleOrder.distribLattice {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

DistribLattice α

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

Equations

IsSimpleOrder.distribLattice = let src := inferInstance; DistribLattice.mk (_ : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)

source

ink

instance IsSimpleOrder.instIsAtomicToPartialOrderToSemilatticeInfToOrderBotToLEToPreorder {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

IsAtomic α

Equations

@IsSimpleOrder.instIsAtomicToPartialOrderToSemilatticeInfToOrderBotToLEToPreorder = @IsSimpleOrder.instIsAtomicToPartialOrderToSemilatticeInfToOrderBotToLEToPreorder.proof_1

source

ink

instance IsSimpleOrder.instIsCoatomicToPartialOrderToSemilatticeInfToOrderTopToLEToPreorder {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

IsCoatomic α

Equations

@IsSimpleOrder.instIsCoatomicToPartialOrderToSemilatticeInfToOrderTopToLEToPreorder = @IsSimpleOrder.instIsCoatomicToPartialOrderToSemilatticeInfToOrderTopToLEToPreorder.proof_1

source

ink

@[simp]

theorem IsSimpleOrder.equivBool_apply {α : Type u_1} [inst : DecidableEq α] [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] (x : α) :

↑IsSimpleOrder.equivBool x = decide (x = ⊤)

source

ink

@[simp]

theorem IsSimpleOrder.equivBool_symm_apply {α : Type u_1} [inst : DecidableEq α] [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] (x : Bool) :

↑(Equiv.symm IsSimpleOrder.equivBool) x = bif x then ⊤ else ⊥

source

ink

def IsSimpleOrder.equivBool {α : Type u_1} [inst : DecidableEq α] [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

α ≃ Bool

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

Equations

One or more equations did not get rendered due to their size.

source

ink

def IsSimpleOrder.orderIsoBool {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

α ≃o Bool

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

Equations

One or more equations did not get rendered due to their size.

source

ink

def IsSimpleOrder.booleanAlgebra {α : Type u_1} [inst : DecidableEq α] [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

BooleanAlgebra α

A simple BoundedOrder is also a BooleanAlgebra.

Equations

One or more equations did not get rendered due to their size.

source

ink

noncomputable def IsSimpleOrder.completeLattice {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

CompleteLattice α

A simple BoundedOrder is also complete.

Equations

One or more equations did not get rendered due to their size.

source

ink

noncomputable def IsSimpleOrder.completeBooleanAlgebra {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :

CompleteBooleanAlgebra α

A simple BoundedOrder is also a CompleteBooleanAlgebra.

Equations

One or more equations did not get rendered due to their size.

source

ink

instance IsSimpleOrder.instIsAtomistic {α : Type u_1} [inst : CompleteLattice α] [inst : IsSimpleOrder α] :

IsAtomistic α

Equations

@IsSimpleOrder.instIsAtomistic = @IsSimpleOrder.instIsAtomistic.proof_1

source

ink

instance IsSimpleOrder.instIsCoatomistic {α : Type u_1} [inst : CompleteLattice α] [inst : IsSimpleOrder α] :

IsCoatomistic α

Equations

@IsSimpleOrder.instIsCoatomistic = @IsSimpleOrder.instIsCoatomistic.proof_1

source

ink

theorem isSimpleOrder_iff_isAtom_top {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] :

IsSimpleOrder α ↔ IsAtom ⊤

source

ink

theorem isSimpleOrder_iff_isCoatom_bot {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] :

IsSimpleOrder α ↔ IsCoatom ⊥

source

ink

theorem Set.isSimpleOrder_Iic_iff_isAtom {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

IsSimpleOrder ↑(Set.Iic a) ↔ IsAtom a

source

ink

theorem Set.isSimpleOrder_Ici_iff_isCoatom {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

IsSimpleOrder ↑(Set.Ici a) ↔ IsCoatom a

source

ink

theorem OrderEmbedding.isAtom_of_map_bot_of_image {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] (f : β ↪o α) (hbot : ↑f.toEmbedding ⊥ = ⊥) {b : β} (hb : IsAtom (↑f.toEmbedding b)) :

IsAtom b

source

ink

theorem OrderEmbedding.isCoatom_of_map_top_of_image {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] (f : β ↪o α) (htop : ↑f.toEmbedding ⊤ = ⊤) {b : β} (hb : IsCoatom (↑f.toEmbedding b)) :

IsCoatom b

source

ink

theorem GaloisInsertion.isAtom_of_u_bot {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) {b : β} (hb : IsAtom (u b)) :

IsAtom b

source

ink

theorem GaloisInsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : IsAtomic α] [inst : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ (a : α), IsAtom a → u (l a) = a) (a : α) :

IsAtom (l a) ↔ IsAtom a

source

ink

theorem GaloisInsertion.isAtom_iff' {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : IsAtomic α] [inst : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ (a : α), IsAtom a → u (l a) = a) (b : β) :

IsAtom (u b) ↔ IsAtom b

source

ink

theorem GaloisInsertion.isCoatom_of_image {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) {b : β} (hb : IsCoatom (u b)) :

IsCoatom b

source

ink

theorem GaloisInsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : IsCoatomic α] [inst : OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a) (b : β) :

IsCoatom (u b) ↔ IsCoatom b

source

ink

theorem GaloisCoinsertion.isCoatom_of_l_top {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (hbot : l ⊤ = ⊤) {a : α} (hb : IsCoatom (l a)) :

IsCoatom a

source

ink

theorem GaloisCoinsertion.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] [inst : IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b) (b : β) :

IsCoatom (u b) ↔ IsCoatom b

source

ink

theorem GaloisCoinsertion.isCoatom_iff' {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] [inst : IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b) (a : α) :

IsCoatom (l a) ↔ IsCoatom a

source

ink

theorem GaloisCoinsertion.isAtom_of_image {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) {a : α} (hb : IsAtom (l a)) :

IsAtom a

source

ink

theorem GaloisCoinsertion.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] [inst : IsAtomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) (h_atom : ∀ (b : β), IsAtom b → l (u b) = b) (a : α) :

IsAtom (l a) ↔ IsAtom a

source

ink

@[simp]

theorem OrderIso.isAtom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] (f : α ≃o β) (a : α) :

IsAtom (↑(RelIso.toRelEmbedding f).toEmbedding a) ↔ IsAtom a

source

ink

@[simp]

theorem OrderIso.isCoatom_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] (f : α ≃o β) (a : α) :

IsCoatom (↑(RelIso.toRelEmbedding f).toEmbedding a) ↔ IsCoatom a

source

ink