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 200]

instance IsSimpleOrder.instFintypeOfDecidableEq {α : Type u_3} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] : Fintype α

Equations

• IsSimpleOrder.instFintypeOfDecidableEq = 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.instIsSimpleOrder : IsSimpleOrder Bool

Equations

• Bool.instIsSimpleOrder = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯