mathlib3 documentation


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 #

@[protected, instance]
@[protected, instance]
def finite.to_is_coatomic {α : Type u_1} [partial_order α] [order_top α] [finite α] :
@[protected, instance]
def finite.to_is_atomic {α : Type u_1} [partial_order α] [order_bot α] [finite α] :