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 IsSimpleOrder.instFintype {α : Type u_3} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] : Fintype α

Equations

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

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

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

instance Bool.instIsSimpleOrderBoolInstLEBoolBoundedOrder : IsSimpleOrder Bool

Equations

• Bool.instIsSimpleOrderBoolInstLEBoolBoundedOrder = (_ : IsSimpleOrder Bool)

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

Equations

• (_ : IsCoatomic α) = (_ : IsCoatomic α)

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

Equations

• (_ : IsAtomic α) = (_ : IsAtomic α)