MinMax

📁 Source: Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean

Statistics

Metric	Count
Definitions	0
Theorems add_lt_add_iff_of_le_of_le, fn_max_add_fn_min, fn_max_mul_fn_min, fn_min_add_fn_max, fn_min_mul_fn_max, le_or_le_of_add_le_add, le_or_le_of_mul_le_mul, le_or_lt_of_add_le_add, le_or_lt_of_mul_le_mul, lt_or_le_of_add_le_add, lt_or_le_of_mul_le_mul, lt_or_lt_of_add_lt_add, lt_or_lt_of_mul_lt_mul, max_add_add_left, max_add_add_right, max_add_min, max_le_add_of_nonneg, max_le_mul_of_one_le, max_mul_min, max_mul_mul_left, max_mul_mul_right, min_add_add_left, min_add_add_right, min_add_max, min_le_add_of_nonneg_left, min_le_add_of_nonneg_right, min_le_mul_of_one_le_left, min_le_mul_of_one_le_right, min_mul_max, min_mul_mul_left, min_mul_mul_right, mul_lt_mul_iff_of_le_of_le	32
Total	32

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_lt_add_iff_of_le_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT	—	lt_or_lt_of_add_lt_add add_lt_add_of_lt_of_le add_lt_add_of_le_of_lt
fn_max_add_fn_min 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—
fn_max_mul_fn_min 📖	mathematical	—	CommMagma.toMul CommSemigroup.toCommMagma SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—
fn_min_add_fn_max 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
fn_min_mul_fn_max 📖	mathematical	—	CommMagma.toMul CommSemigroup.toCommMagma SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
le_or_le_of_add_le_add 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	Mathlib.Tactic.Contrapose.contrapose₁ not_le add_lt_add_of_lt_of_lt
le_or_le_of_mul_le_mul 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	Mathlib.Tactic.Contrapose.contrapose₁ mul_lt_mul_of_lt_of_lt
le_or_lt_of_add_le_add 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT	—	Mathlib.Tactic.Contrapose.contrapose₁ not_le not_lt add_lt_add_of_lt_of_le
le_or_lt_of_mul_le_mul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT	—	Mathlib.Tactic.Contrapose.contrapose₁ mul_lt_mul_of_lt_of_le
lt_or_le_of_add_le_add 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT	—	Mathlib.Tactic.Contrapose.contrapose₁ not_lt not_le add_lt_add_of_le_of_lt
lt_or_le_of_mul_le_mul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT	—	Mathlib.Tactic.Contrapose.contrapose₁ mul_lt_mul_of_le_of_lt
lt_or_lt_of_add_lt_add 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	Mathlib.Tactic.Contrapose.contrapose₁ not_lt add_le_add
lt_or_lt_of_mul_lt_mul 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	Mathlib.Tactic.Contrapose.contrapose₁ mul_le_mul'
max_add_add_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_max Monotone.const_add monotone_id
max_add_add_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_max Monotone.add_const monotone_id
max_add_min 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	fn_max_add_fn_min
max_le_add_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero	SemilatticeSup.toMax Lattice.toSemilatticeSup AddZero.toAdd	—	max_le_iff le_add_of_nonneg_right le_add_of_nonneg_left
max_le_mul_of_one_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne	SemilatticeSup.toMax Lattice.toSemilatticeSup MulOne.toMul	—	max_le_iff le_mul_of_one_le_right' le_mul_of_one_le_left'
max_mul_min 📖	mathematical	—	CommMagma.toMul CommSemigroup.toCommMagma SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	fn_max_mul_fn_min
max_mul_mul_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_max Monotone.const_mul' monotone_id
max_mul_mul_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_max Monotone.mul_const' monotone_id
min_add_add_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_min Monotone.const_add monotone_id
min_add_add_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_min Monotone.add_const monotone_id
min_add_max 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	fn_min_add_fn_max
min_le_add_of_nonneg_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero	SemilatticeInf.toMin AddZero.toAdd	—	min_le_iff le_add_of_nonneg_left
min_le_add_of_nonneg_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero	SemilatticeInf.toMin AddZero.toAdd	—	min_le_iff le_add_of_nonneg_right
min_le_mul_of_one_le_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne	SemilatticeInf.toMin MulOne.toMul	—	min_le_iff le_mul_of_one_le_left'
min_le_mul_of_one_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne	SemilatticeInf.toMin MulOne.toMul	—	min_le_iff le_mul_of_one_le_right'
min_mul_max 📖	mathematical	—	CommMagma.toMul CommSemigroup.toCommMagma SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	fn_min_mul_fn_max
min_mul_mul_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_min Monotone.const_mul' monotone_id
min_mul_mul_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Monotone.map_min Monotone.mul_const' monotone_id
mul_lt_mul_iff_of_le_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT	—	lt_or_lt_of_mul_lt_mul mul_lt_mul_of_lt_of_le mul_lt_mul_of_le_of_lt

---

← Back to Index