Documentation

Mathlib.Order.Atoms.Finite

Atoms, Coatoms, Simple Lattices, and Finiteness #

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

Main results #

instance IsSimpleOrder.instFintype {α : Type u_1} [inst : DecidableEq α] [inst : LE α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] :
Equations
theorem Fintype.IsSimpleOrder.univ {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] [inst : DecidableEq α] :
Finset.univ = {, }
theorem Fintype.IsSimpleOrder.card {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : IsSimpleOrder α] [inst : DecidableEq α] :
instance Finite.to_isAtomic {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] [inst : Finite α] :
Equations