MinMax

📁 Source: Mathlib/Order/MinMax.lean

Statistics

Metric	Count
Definitions	0
Theorems map_max, map_min, map_max, map_min, left_comm, right_comm, map_max, map_min, map_max, map_min, instAssociativeMax, instAssociativeMin, instCommutativeMax, instCommutativeMin, instLawfulOrderInf_mathlib, instLawfulOrderSup_mathlib, le_max_iff, le_max_of_le_left, le_max_of_le_right, le_min_iff, le_of_le_min_left, le_of_le_min_right, le_of_max_le_left, le_of_max_le_right, lt_max_iff, lt_max_of_lt_left, lt_max_of_lt_right, lt_min_iff, max_cases, max_choice, max_eq_iff, max_eq_left_iff, max_eq_right_iff, max_idem, max_le_iff, max_le_max, max_le_max_left, max_le_max_right, max_left_commutative, max_lt_iff, max_lt_max, max_lt_max_left_iff, max_lt_max_right_iff, max_min_distrib_left, max_min_distrib_right, max_right_comm, min_cases, min_choice, min_eq_iff, min_eq_left_iff, min_eq_right_iff, min_idem, min_le_iff, min_le_max, min_le_min, min_le_min_left, min_le_min_right, min_le_of_left_le, min_le_of_right_le, min_left_commutative, min_lt_iff, min_lt_max, min_lt_min, min_lt_min_left_iff, min_lt_min_right_iff, min_lt_of_left_lt, min_lt_of_right_lt, min_max_distrib_left, min_max_distrib_right, min_right_comm	70
Total	70

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_max 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	le_total sup_of_le_right inf_of_le_right sup_of_le_left inf_of_le_left
map_min 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total inf_of_le_right sup_of_le_right inf_of_le_left sup_of_le_left

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_max 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	MonotoneOn.map_max dual_right
map_min 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	MonotoneOn.map_min dual_right

Max

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
left_comm 📖	mathematical	—	LinearOrder.toMax	—	max_left_comm
right_comm 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max_right_comm

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_max 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_total sup_of_le_right sup_of_le_left
map_min 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_total inf_of_le_right inf_of_le_left

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_max 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_total max_eq_right max_eq_left
map_min 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_total min_eq_right min_eq_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAssociativeMax 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max_assoc
instAssociativeMin 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	min_assoc
instCommutativeMax 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max_comm
instCommutativeMin 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	min_comm
instLawfulOrderInf_mathlib 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup	—	le_min_iff
instLawfulOrderSup_mathlib 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	max_le_iff
le_max_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_sup_iff
le_max_of_le_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_sup_of_le_left
le_max_of_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_sup_of_le_right
le_min_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	le_inf_iff
le_of_le_min_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	ge_trans min_le_left
le_of_le_min_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	ge_trans min_le_right
le_of_max_le_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_trans le_max_left
le_of_max_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_trans le_max_right
lt_max_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	lt_sup_iff
lt_max_of_lt_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	LT.lt.trans_le le_max_left
lt_max_of_lt_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	LT.lt.trans_le le_max_right
lt_min_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	lt_inf_iff
max_cases 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Preorder.toLT	—	—
max_choice 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_total sup_of_le_left sup_of_le_right
max_eq_iff 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	—
max_eq_left_iff 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	sup_eq_left
max_eq_right_iff 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	sup_eq_right
max_idem 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max_self
max_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax	—	sup_le_iff
max_le_max 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_le_sup
max_le_max_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_le_sup_left
max_le_max_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_le_sup_right
max_left_commutative 📖	mathematical	—	LeftCommutative SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max_left_comm
max_lt_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax	—	sup_lt_iff
max_lt_max 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	max_lt lt_max_of_lt_left lt_max_of_lt_right
max_lt_max_left_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax	—	—
max_lt_max_right_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax	—	—
max_min_distrib_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	sup_inf_left
max_min_distrib_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	sup_inf_right
max_right_comm 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	max_assoc max_comm
min_cases 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Preorder.toLT	—	—
min_choice 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_total inf_of_le_left inf_of_le_right
min_eq_iff 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	—
min_eq_left_iff 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	inf_eq_left
min_eq_right_iff 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	—	inf_eq_right
min_idem 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	min_self
min_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_le_iff
min_le_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_trans min_le_left le_max_left
min_le_min 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_le_inf
min_le_min_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_le_inf_left
min_le_min_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_le_inf_right
min_le_of_left_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_le_of_left_le
min_le_of_right_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_le_of_right_le
min_left_commutative 📖	mathematical	—	LeftCommutative SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	min_left_comm
min_lt_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_lt_iff
min_lt_max 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_lt_sup
min_lt_min 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	lt_min min_lt_of_left_lt min_lt_of_right_lt
min_lt_min_left_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	—
min_lt_min_right_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	—
min_lt_of_left_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	LT.lt.trans_le' min_le_left
min_lt_of_right_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	LT.lt.trans_le' min_le_right
min_max_distrib_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_sup_left
min_max_distrib_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_sup_right
min_right_comm 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	min_assoc min_comm

---

← Back to Index