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