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_1}
[inst : DecidableEq α]
[inst : LE α]
[inst : BoundedOrder α]
[inst : IsSimpleOrder α]
:
Fintype α
Equations
- IsSimpleOrder.instFintype = Fintype.ofEquiv Bool (Equiv.symm IsSimpleOrder.equivBool)
theorem
Fintype.IsSimpleOrder.univ
{α : Type u_1}
[inst : PartialOrder α]
[inst : BoundedOrder α]
[inst : IsSimpleOrder α]
[inst : DecidableEq α]
:
theorem
Fintype.IsSimpleOrder.card
{α : Type u_1}
[inst : PartialOrder α]
[inst : BoundedOrder α]
[inst : IsSimpleOrder α]
[inst : DecidableEq α]
:
Fintype.card α = 2
Equations
- One or more equations did not get rendered due to their size.
instance
Finite.to_isCoatomic
{α : Type u_1}
[inst : PartialOrder α]
[inst : OrderTop α]
[inst : Finite α]
:
instance
Finite.to_isAtomic
{α : Type u_1}
[inst : PartialOrder α]
[inst : OrderBot α]
[inst : Finite α]
:
IsAtomic α