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_3} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] :
Equations
theorem Fintype.IsSimpleOrder.univ {α : Type u_1} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α] :
Finset.univ = {, }
instance Finite.to_isCoatomic {α : Type u_1} [PartialOrder α] [OrderTop α] [Finite α] :
Equations
instance Finite.to_isAtomic {α : Type u_1} [PartialOrder α] [OrderBot α] [Finite α] :
Equations