Order structures on finite types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides order instances on fintypes.
Computable instances #
On a fintype, we can construct
- an
order_botfromsemilattice_inf. - an
order_topfromsemilattice_sup. - a
bounded_orderfromlattice.
Those are marked as def to avoid defeqness issues.
Completion instances #
Those instances are noncomputable because the definitions of Sup and Inf use set.to_finset and
set membership is undecidable in general.
On a fintype, we can promote:
- a
latticeto acomplete_lattice. - a
distrib_latticeto acomplete_distrib_lattice. - a
linear_orderto acomplete_linear_order. - a
boolean_algebrato acomplete_boolean_algebra.
Those are marked as def to avoid typeclass loops.
Concrete instances #
We provide a few instances for concrete types:
@[reducible]
Constructs the ⊥ of a finite nonempty semilattice_inf.
Equations
- fintype.to_order_bot α = {bot := finset.univ.inf' finset.univ_nonempty id, bot_le := _}
@[reducible]
Constructs the ⊤ of a finite nonempty semilattice_sup
Equations
- fintype.to_order_top α = {top := finset.univ.sup' finset.univ_nonempty id, le_top := _}
@[reducible]
Constructs the ⊤ and ⊥ of a finite nonempty lattice.
Equations
- fintype.to_bounded_order α = {top := order_top.top (fintype.to_order_top α), le_top := _, bot := order_bot.bot (fintype.to_order_bot α), bot_le := _}
@[reducible]
noncomputable
def
fintype.to_complete_lattice
(α : Type u_2)
[fintype α]
[lattice α]
[bounded_order α] :
A finite bounded lattice is complete.
Equations
- fintype.to_complete_lattice α = {sup := lattice.sup _inst_3, le := lattice.le _inst_3, lt := lattice.lt _inst_3, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf _inst_3, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set α), s.to_finset.sup id, le_Sup := _, Sup_le := _, Inf := λ (s : set α), s.to_finset.inf id, Inf_le := _, le_Inf := _, top := bounded_order.top _inst_4, bot := bounded_order.bot _inst_4, le_top := _, bot_le := _}
@[reducible]
noncomputable
def
fintype.to_complete_distrib_lattice
(α : Type u_2)
[fintype α]
[distrib_lattice α]
[bounded_order α] :
A finite bounded distributive lattice is completely distributive.
Equations
- fintype.to_complete_distrib_lattice α = {sup := complete_lattice.sup (fintype.to_complete_lattice α), le := complete_lattice.le (fintype.to_complete_lattice α), lt := complete_lattice.lt (fintype.to_complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (fintype.to_complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (fintype.to_complete_lattice α), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (fintype.to_complete_lattice α), Inf_le := _, le_Inf := _, top := complete_lattice.top (fintype.to_complete_lattice α), bot := complete_lattice.bot (fintype.to_complete_lattice α), le_top := _, bot_le := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}
@[reducible]
noncomputable
def
fintype.to_complete_linear_order
(α : Type u_2)
[fintype α]
[linear_order α]
[bounded_order α] :
A finite bounded linear order is complete.
Equations
- fintype.to_complete_linear_order α = {sup := complete_lattice.sup (fintype.to_complete_lattice α), le := complete_lattice.le (fintype.to_complete_lattice α), lt := complete_lattice.lt (fintype.to_complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (fintype.to_complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (fintype.to_complete_lattice α), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (fintype.to_complete_lattice α), Inf_le := _, le_Inf := _, top := complete_lattice.top (fintype.to_complete_lattice α), bot := complete_lattice.bot (fintype.to_complete_lattice α), le_top := _, bot_le := _, le_total := _, decidable_le := linear_order.decidable_le _inst_3, decidable_eq := linear_order.decidable_eq _inst_3, decidable_lt := linear_order.decidable_lt _inst_3, max_def := _, min_def := _}
@[reducible]
noncomputable
def
fintype.to_complete_boolean_algebra
(α : Type u_2)
[fintype α]
[boolean_algebra α] :
A finite boolean algebra is complete.
Equations
- fintype.to_complete_boolean_algebra α = {sup := complete_distrib_lattice.sup (fintype.to_complete_distrib_lattice α), le := complete_distrib_lattice.le (fintype.to_complete_distrib_lattice α), lt := complete_distrib_lattice.lt (fintype.to_complete_distrib_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_distrib_lattice.inf (fintype.to_complete_distrib_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := boolean_algebra.compl _inst_3, sdiff := boolean_algebra.sdiff _inst_3, himp := boolean_algebra.himp _inst_3, top := complete_distrib_lattice.top (fintype.to_complete_distrib_lattice α), bot := complete_distrib_lattice.bot (fintype.to_complete_distrib_lattice α), inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _, Sup := complete_distrib_lattice.Sup (fintype.to_complete_distrib_lattice α), le_Sup := _, Sup_le := _, Inf := complete_distrib_lattice.Inf (fintype.to_complete_distrib_lattice α), Inf_le := _, le_Inf := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}
@[reducible]
noncomputable
def
fintype.to_complete_lattice_of_nonempty
(α : Type u_2)
[fintype α]
[nonempty α]
[lattice α] :
A nonempty finite lattice is complete. If the lattice is already a bounded_order, then use
fintype.to_complete_lattice instead, as this gives definitional equality for ⊥ and ⊤.
@[reducible]
noncomputable
def
fintype.to_complete_linear_order_of_nonempty
(α : Type u_2)
[fintype α]
[nonempty α]
[linear_order α] :
A nonempty finite linear order is complete. If the linear order is already a bounded_order,
then use fintype.to_complete_linear_order instead, as this gives definitional equality for ⊥ and
⊤.
Equations
- fintype.to_complete_linear_order_of_nonempty α = {sup := complete_lattice.sup (fintype.to_complete_lattice_of_nonempty α), le := complete_lattice.le (fintype.to_complete_lattice_of_nonempty α), lt := complete_lattice.lt (fintype.to_complete_lattice_of_nonempty α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (fintype.to_complete_lattice_of_nonempty α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (fintype.to_complete_lattice_of_nonempty α), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (fintype.to_complete_lattice_of_nonempty α), Inf_le := _, le_Inf := _, top := complete_lattice.top (fintype.to_complete_lattice_of_nonempty α), bot := complete_lattice.bot (fintype.to_complete_lattice_of_nonempty α), le_top := _, bot_le := _, le_total := _, decidable_le := linear_order.decidable_le _inst_4, decidable_eq := linear_order.decidable_eq _inst_4, decidable_lt := linear_order.decidable_lt _inst_4, max_def := _, min_def := _}
Concrete instances #
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]