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.

ink

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)

ink

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

ink

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

ink

instance Bool.instIsSimpleOrderBoolToLEToPreorderToPartialOrderToSemilatticeInfToLatticeToGeneralizedCoheytingAlgebraToCoheytingAlgebraToBiheytingAlgebraInstBooleanAlgebraBoolBoundedOrder : IsSimpleOrder Bool

Equations

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

ink

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

Equations

• @Finite.to_isCoatomic = @Finite.to_isCoatomic.proof_1

ink

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

Equations

• @Finite.to_isAtomic = @Finite.to_isAtomic.proof_1