MinMax

📁 Source: Mathlib/Data/List/MinMax.lean

Statistics

Metric	Count
Definitions argAux, argmax, argmin, maximum, maximum_of_length_pos, minimum, minimum_of_length_pos	7
Theorems maximum_eq, minimum_eq, argAux_self, argmax_concat, argmax_cons, argmax_eq_none, argmax_eq_some_iff, argmax_mem, argmax_nil, argmax_singleton, argmin_concat, argmin_cons, argmin_eq_none, argmin_eq_some_iff, argmin_mem, argmin_nil, argmin_singleton, coe_le_maximum_iff, coe_maximum_of_length_pos, coe_minimum_of_length_pos, foldl_argAux_eq_none, foldr_max_of_ne_nil, foldr_min_of_ne_nil, getD_max?_eq_unbotD_maximum, getD_min?_eq_untopD_minimum, getElem_le_maximum_of_length_pos, index_of_argmax, index_of_argmin, le_max_of_le, le_max_of_le', le_maximum_of_length_pos_iff, le_maximum_of_length_pos_of_mem, le_maximum_of_mem, le_maximum_of_mem', le_min_of_forall_le, le_minimum_of_forall_le, le_of_mem_argmax, le_of_mem_argmin, max_le_of_forall_le, maximum_append, maximum_concat, maximum_cons, maximum_eq_bot, maximum_eq_coe_iff, maximum_le_of_forall_le, maximum_mem, maximum_mono, maximum_ne_bot_of_length_pos, maximum_ne_bot_of_ne_nil, maximum_nil, maximum_of_length_pos_mem, maximum_singleton, mem_argmax_iff, mem_argmin_iff, min_le_of_le, min_le_of_le', minimum_anti, minimum_append, minimum_concat, minimum_cons, minimum_eq_coe_iff, minimum_eq_top, minimum_le_coe_iff, minimum_le_of_mem, minimum_le_of_mem', minimum_mem, minimum_ne_top_of_length_pos, minimum_ne_top_of_ne_nil, minimum_nil, minimum_of_length_pos_le_getElem, minimum_of_length_pos_le_iff, minimum_of_length_pos_le_of_mem, minimum_of_length_pos_mem, minimum_singleton, not_lt_minimum_of_mem, not_lt_minimum_of_mem', not_lt_of_mem_argmax, not_lt_of_mem_argmin, not_maximum_lt_of_mem, not_maximum_lt_of_mem', not_of_mem_foldl_argAux	81
Total	88

List

Definitions

Name	Category	Theorems
argAux 📖	CompOp	2 math math: foldl_argAux_eq_none, argAux_self
argmax 📖	CompOp	7 math math: argmax_cons, argmax_singleton, argmax_eq_some_iff, argmax_nil, argmax_concat, mem_argmax_iff, argmax_eq_none
argmin 📖	CompOp	7 math math: argmin_singleton, mem_argmin_iff, argmin_nil, argmin_eq_some_iff, argmin_concat, argmin_cons, argmin_eq_none
maximum 📖	CompOp	18 math math: getD_max?_eq_unbotD_maximum, maximum_cons, foldr_max_of_ne_nil, coe_maximum_of_length_pos, maximum_singleton, coe_le_maximum_iff, maximum_nil, maximum_eq_bot, maximum_le_of_forall_le, not_maximum_lt_of_mem', le_maximum_of_mem', Perm.maximum_eq, maximum_mono, maximum_eq_coe_iff, le_maximum_of_length_pos_iff, Polynomial.degree_list_sum_le, maximum_concat, maximum_append
maximum_of_length_pos 📖	CompOp	5 math math: coe_maximum_of_length_pos, le_maximum_of_length_pos_of_mem, maximum_of_length_pos_mem, getElem_le_maximum_of_length_pos, le_maximum_of_length_pos_iff
minimum 📖	CompOp	18 math math: minimum_of_length_pos_le_iff, minimum_singleton, minimum_append, minimum_nil, minimum_cons, getD_min?_eq_untopD_minimum, minimum_eq_coe_iff, le_minimum_of_forall_le, minimum_eq_top, minimum_anti, foldr_min_of_ne_nil, minimum_le_of_mem', minimum_concat, minimum_le_coe_iff, coe_minimum_of_length_pos, not_lt_minimum_of_mem', trop_minimum, Perm.minimum_eq
minimum_of_length_pos 📖	CompOp	5 math math: minimum_of_length_pos_le_iff, minimum_of_length_pos_le_of_mem, minimum_of_length_pos_mem, minimum_of_length_pos_le_getElem, coe_minimum_of_length_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
argAux_self 📖	mathematical	—	argAux	—	—
argmax_concat 📖	mathematical	—	argmax Preorder.toLT	—	argmax.eq_1
argmax_cons 📖	mathematical	—	argmax PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLT	—	argmax_concat lt_trans LT.lt.gt_or_lt
argmax_eq_none 📖	mathematical	—	argmax	—	—
argmax_eq_some_iff 📖	mathematical	—	argmax PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLE	—	mem_argmax_iff
argmax_mem 📖	—	argmax	—	—	—
argmax_nil 📖	mathematical	—	argmax	—	—
argmax_singleton 📖	mathematical	—	argmax	—	—
argmin_concat 📖	mathematical	—	argmin Preorder.toLT	—	argmax_concat
argmin_cons 📖	mathematical	—	argmin PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLT	—	argmax_cons
argmin_eq_none 📖	mathematical	—	argmin	—	argmax_eq_none
argmin_eq_some_iff 📖	mathematical	—	argmin PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLE	—	mem_argmin_iff
argmin_mem 📖	—	argmin	—	—	argmax_mem
argmin_nil 📖	mathematical	—	argmin	—	—
argmin_singleton 📖	mathematical	—	argmin	—	—
coe_le_maximum_iff 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.some maximum LinearOrder.toDecidableLT	—	maximum_cons
coe_maximum_of_length_pos 📖	mathematical	—	WithBot.some maximum_of_length_pos maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT	—	WithBot.coe_unbot maximum_ne_bot_of_length_pos
coe_minimum_of_length_pos 📖	mathematical	—	WithTop.some minimum_of_length_pos minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT	—	WithTop.coe_untop maximum_ne_bot_of_length_pos
foldl_argAux_eq_none 📖	mathematical	—	argAux	—	—
foldr_max_of_ne_nil 📖	mathematical	—	WithBot.some SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf maximum LinearOrder.toDecidableLT	—	maximum_cons WithBot.coe_max sup_of_le_left
foldr_min_of_ne_nil 📖	mathematical	—	WithTop.some SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder minimum LinearOrder.toDecidableLT	—	foldr_max_of_ne_nil
getD_max?_eq_unbotD_maximum 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.unbotD maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf LinearOrder.toDecidableLT	—	maximum_eq_bot instIsEmptyFalse maximum_eq_coe_iff le_antisymm
getD_min?_eq_untopD_minimum 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.untopD minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder LinearOrder.toDecidableLT	—	getD_max?_eq_unbotD_maximum
getElem_le_maximum_of_length_pos 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder maximum_of_length_pos	—	le_maximum_of_length_pos_of_mem
index_of_argmax 📖	—	argmax PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLE	—	—	idxOf_of_notMem argmax_cons not_le_of_gt le_refl LT.lt.ne lt_of_lt_of_le
index_of_argmin 📖	—	argmin PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLE	—	—	index_of_argmax
le_max_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup Bot.bot OrderBot.toBot	—	le_max_of_le_left le_max_of_le_right
le_max_of_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_max_of_le_left le_max_of_le_right
le_maximum_of_length_pos_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder maximum_of_length_pos WithBot WithBot.instPreorder WithBot.some maximum LinearOrder.toDecidableLT	—	WithBot.le_unbot_iff maximum_ne_bot_of_length_pos
le_maximum_of_length_pos_of_mem 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder maximum_of_length_pos	—	le_maximum_of_mem'
le_maximum_of_mem 📖	mathematical	maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithBot.some	Preorder.toLE	—	le_of_mem_argmax
le_maximum_of_mem' 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.some maximum LinearOrder.toDecidableLT	—	le_of_not_gt not_maximum_lt_of_mem'
le_min_of_forall_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeInf.toMin Top.top OrderTop.toTop	—	max_le_of_forall_le
le_minimum_of_forall_le 📖	mathematical	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.some	minimum LinearOrder.toDecidableLT	—	minimum_cons
le_of_mem_argmax 📖	mathematical	argmax PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT	Preorder.toLE	—	le_of_not_gt not_lt_of_mem_argmax
le_of_mem_argmin 📖	mathematical	argmin PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT	Preorder.toLE	—	le_of_mem_argmax
max_le_of_forall_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup Bot.bot OrderBot.toBot	—	—
maximum_append 📖	mathematical	—	maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithBot SemilatticeSup.toMax WithBot.semilatticeSup Lattice.toSemilatticeSup	—	sup_of_le_right maximum_cons max_assoc
maximum_concat 📖	mathematical	—	maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithBot SemilatticeSup.toMax WithBot.semilatticeSup Lattice.toSemilatticeSup WithBot.some	—	argmax_concat max_eq_right bot_le max_def_lt
maximum_cons 📖	mathematical	—	maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithBot SemilatticeSup.toMax WithBot.semilatticeSup Lattice.toSemilatticeSup WithBot.some	—	sup_of_le_left maximum_concat max_assoc
maximum_eq_bot 📖	mathematical	—	maximum Bot.bot WithBot WithBot.bot	—	argmax_eq_none
maximum_eq_coe_iff 📖	mathematical	—	maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithBot.some Preorder.toLE	—	maximum.eq_1 WithBot.some_eq_coe argmax_eq_some_iff le_antisymm le_refl
maximum_le_of_forall_le 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.some	maximum LinearOrder.toDecidableLT	—	maximum_cons
maximum_mem 📖	—	maximum WithBot.some	—	—	argmax_mem
maximum_mono 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder maximum LinearOrder.toDecidableLT	—	maximum_le_of_forall_le le_maximum_of_mem'
maximum_ne_bot_of_length_pos 📖	—	—	—	—	maximum_cons
maximum_ne_bot_of_ne_nil 📖	—	—	—	—	maximum_cons
maximum_nil 📖	mathematical	—	maximum Bot.bot WithBot WithBot.bot	—	—
maximum_of_length_pos_mem 📖	mathematical	—	maximum_of_length_pos	—	maximum_mem coe_maximum_of_length_pos
maximum_singleton 📖	mathematical	—	maximum WithBot.some	—	—
mem_argmax_iff 📖	mathematical	—	argmax PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLE	—	argmax_mem le_of_mem_argmax index_of_argmax
mem_argmin_iff 📖	mathematical	—	argmin PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT Preorder.toLE	—	mem_argmax_iff
min_le_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeInf.toMin Top.top OrderTop.toTop	—	le_max_of_le
min_le_of_le' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeInf.toMin	—	le_max_of_le'
minimum_anti 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder minimum LinearOrder.toDecidableLT	—	maximum_mono
minimum_append 📖	mathematical	—	minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithTop SemilatticeInf.toMin WithTop.semilatticeInf	—	maximum_append
minimum_concat 📖	mathematical	—	minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithTop SemilatticeInf.toMin WithTop.semilatticeInf WithTop.some	—	maximum_concat
minimum_cons 📖	mathematical	—	minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithTop SemilatticeInf.toMin WithTop.semilatticeInf WithTop.some	—	maximum_cons
minimum_eq_coe_iff 📖	mathematical	—	minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithTop.some Preorder.toLE	—	maximum_eq_coe_iff
minimum_eq_top 📖	mathematical	—	minimum Top.top WithTop WithTop.top	—	argmin_eq_none
minimum_le_coe_iff 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder minimum LinearOrder.toDecidableLT WithTop.some	—	minimum_cons
minimum_le_of_mem 📖	mathematical	minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT WithTop.some	Preorder.toLE	—	le_of_mem_argmin
minimum_le_of_mem' 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder minimum LinearOrder.toDecidableLT WithTop.some	—	le_of_not_gt not_lt_minimum_of_mem'
minimum_mem 📖	—	minimum WithTop.some	—	—	argmin_mem
minimum_ne_top_of_length_pos 📖	—	—	—	—	maximum_ne_bot_of_length_pos
minimum_ne_top_of_ne_nil 📖	—	—	—	—	maximum_ne_bot_of_ne_nil
minimum_nil 📖	mathematical	—	minimum Top.top WithTop WithTop.top	—	—
minimum_of_length_pos_le_getElem 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder minimum_of_length_pos	—	getElem_le_maximum_of_length_pos
minimum_of_length_pos_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder minimum_of_length_pos WithTop WithTop.instPreorder minimum LinearOrder.toDecidableLT WithTop.some	—	WithTop.untop_le_iff maximum_ne_bot_of_length_pos
minimum_of_length_pos_le_of_mem 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder minimum_of_length_pos	—	le_maximum_of_length_pos_of_mem
minimum_of_length_pos_mem 📖	mathematical	—	minimum_of_length_pos	—	maximum_of_length_pos_mem
minimum_singleton 📖	mathematical	—	minimum WithTop.some	—	—
not_lt_minimum_of_mem 📖	mathematical	minimum WithTop.some	Preorder.toLT	—	not_lt_of_mem_argmin
not_lt_minimum_of_mem' 📖	mathematical	—	WithTop Preorder.toLT WithTop.instPreorder WithTop.some minimum	—	not_lt_minimum_of_mem
not_lt_of_mem_argmax 📖	mathematical	argmax	Preorder.toLT	—	not_of_mem_foldl_argAux lt_irrefl lt_trans
not_lt_of_mem_argmin 📖	mathematical	argmin	Preorder.toLT	—	not_of_mem_foldl_argAux lt_irrefl lt_trans
not_maximum_lt_of_mem 📖	mathematical	maximum WithBot.some	Preorder.toLT	—	not_lt_of_mem_argmax
not_maximum_lt_of_mem' 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder maximum WithBot.some	—	not_maximum_lt_of_mem
not_of_mem_foldl_argAux 📖	—	Transitive argAux	—	—	instIsEmptyFalse foldl_argAux_eq_none argAux.eq_1

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximum_eq 📖	mathematical	—	List.maximum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT	—	—
minimum_eq 📖	mathematical	—	List.minimum PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrder.toDecidableLT	—	—

---

← Back to Index