Atoms, Coatoms, Simple Lattices, and Finiteness #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This module contains some results on atoms and simple lattices in the finite context.
Main results #
finite.to_is_atomic,finite.to_is_coatomic: Finite partial orders with bottom resp. top are atomic resp. coatomic.
@[protected, instance]
def
is_simple_order.fintype
{α : Type u_1}
[decidable_eq α]
[has_le α]
[bounded_order α]
[is_simple_order α] :
fintype α
theorem
fintype.is_simple_order.univ
{α : Type u_1}
[partial_order α]
[bounded_order α]
[is_simple_order α]
[decidable_eq α] :
finset.univ = {⊤, ⊥}
theorem
fintype.is_simple_order.card
{α : Type u_1}
[partial_order α]
[bounded_order α]
[is_simple_order α]
[decidable_eq α] :
fintype.card α = 2
@[protected, instance]
@[protected, instance]