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
  • =
Equations
  • =
Equations
  • =
theorem exists_covby_infinite_Ici_of_infinite_Ici {α : Type u_1} [PartialOrder α] {a : α} [IsStronglyAtomic α] (ha : (Set.Ici a).Infinite) (hfin : {x : α | a x}.Finite) :
∃ (b : α), a b (Set.Ici b).Infinite
theorem exists_covby_infinite_Iic_of_infinite_Iic {α : Type u_1} [PartialOrder α] {a : α} [IsStronglyCoatomic α] (ha : (Set.Iic a).Infinite) (hfin : {x : α | x a}.Finite) :
∃ (b : α), b a (Set.Iic b).Infinite