Atoms, Coatoms, Simple Lattices, and Finiteness

This module contains some results on atoms and simple lattices in the finite context.

Main results

• Finite.to_isAtomic, Finite.to_isCoatomic: Finite partial orders with bottom resp. top are atomic resp. coatomic.

@[instance_reducible]

def IsSimpleOrder.instFintypeOfDecidableEq {α : Type u_1} [LE α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α] : Fintype α

It is important that IsSimpleOrder is the last type-class argument of this instance, so that type-class inference fails quickly if it doesn't apply.

Note that as of 2025-08-13, this is false. Could someone investigate?

Equations

• IsSimpleOrder.instFintypeOfDecidableEq = Fintype.ofEquiv Bool IsSimpleOrder.equivBool.symm

theorem IsSimpleOrder.instFinite {α : Type u_1} [LE α] [BoundedOrder α] [IsSimpleOrder α] : Finite α

theorem Fintype.IsSimpleOrder.univ {α : Type u_1} [LE α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α] : Finset.univ = {⊤, ⊥}

theorem Fintype.IsSimpleOrder.card {α : Type u_1} [LE α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α] : Fintype.card α = 2

instance Bool.instIsSimpleOrder : IsSimpleOrder Bool

@[instance 100]

instance Finite.to_isCoatomic {α : Type u_1} [PartialOrder α] [OrderTop α] [Finite α] : IsCoatomic α

@[instance 100]

instance Finite.to_isAtomic {α : Type u_1} [PartialOrder α] [OrderBot α] [Finite α] : IsAtomic α

instance instIsStronglyAtomic {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] : IsStronglyAtomic α

instance instIsStronglyCoatomic {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] : IsStronglyCoatomic α

theorem exists_covby_infinite_Ici_of_infinite_Ici {α : Type u_1} [PartialOrder α] {a : α} [IsStronglyAtomic α] (ha : (Set.Ici a).Infinite) (hfin : {x : α | a ⋖ x}.Finite) : ∃ (b : α), a ⋖ b ∧ (Set.Ici b).Infinite

theorem exists_covby_infinite_Iic_of_infinite_Iic {α : Type u_1} [PartialOrder α] {a : α} [IsStronglyCoatomic α] (ha : (Set.Iic a).Infinite) (hfin : {x : α | x ⋖ a}.Finite) : ∃ (b : α), b ⋖ a ∧ (Set.Iic b).Infinite