ExistsOfLE

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

Statistics

Metric	Count
Definitions ExistsAddOfLE, ExistsMulOfLE	2
Theorems existsAddOfLE, exists_add_of_le, exists_mul_of_le, existsMulOfLE, exists_nonneg_add_of_le, exists_one_le_mul_of_le, exists_one_lt_mul_of_lt', exists_pos_add_of_lt', le_iff_exists_nonneg_add, le_iff_exists_one_le_mul, le_iff_forall_one_lt_le_mul, le_iff_forall_one_lt_lt_mul', le_iff_forall_pos_le_add, le_iff_forall_pos_lt_add', le_of_forall_one_lt_le_mul, le_of_forall_one_lt_lt_mul', le_of_forall_pos_le_add, le_of_forall_pos_lt_add', lt_iff_exists_one_lt_mul, lt_iff_exists_pos_add	20
Total	22

AddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsAddOfLE 📖	mathematical	—	ExistsAddOfLE AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid toSubNegMonoid	—	add_neg_cancel_left

ExistsAddOfLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_add_of_le 📖	—	—	—	—	—

ExistsMulOfLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mul_of_le 📖	—	—	—	—	—

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsMulOfLE 📖	mathematical	—	ExistsMulOfLE MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid toDivInvMonoid	—	mul_inv_cancel_left

(root)

Definitions

Name	Category	Theorems
ExistsAddOfLE 📖	CompData	11 math math: WithZero.instExistsAddOfLE, Additive.existsAddOfLe, Ordinal.existsAddOfLE, Multiset.instExistsAddOfLE, WithTop.existsAddOfLE, CanonicallyOrderedAdd.toExistsAddOfLE, Filter.Germ.instExistsAddOfLE, Prod.instExistsAddOfLE, AddGroup.existsAddOfLE, StarOrderedRing.toExistsAddOfLE, Nonneg.existsAddOfLE
ExistsMulOfLE 📖	CompData	5 math math: CanonicallyOrderedMul.toExistsMulOfLE, Prod.instExistsMulOfLE, Filter.Germ.instExistsMulOfLE, Group.existsMulOfLE, Multiplicative.existsMulOfLe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nonneg_add_of_le 📖	mathematical	Preorder.toLE	AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd	—	ExistsAddOfLE.exists_add_of_le nonneg_of_le_add_right
exists_one_le_mul_of_le 📖	mathematical	Preorder.toLE	MulOne.toOne MulOneClass.toMulOne MulOne.toMul	—	ExistsMulOfLE.exists_mul_of_le one_le_of_le_mul_right
exists_one_lt_mul_of_lt' 📖	mathematical	Preorder.toLT	MulOne.toOne MulOneClass.toMulOne MulOne.toMul	—	ExistsMulOfLE.exists_mul_of_le LT.lt.le one_lt_of_lt_mul_right
exists_pos_add_of_lt' 📖	mathematical	Preorder.toLT	AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd	—	ExistsAddOfLE.exists_add_of_le LT.lt.le pos_of_lt_add_right
le_iff_exists_nonneg_add 📖	mathematical	—	Preorder.toLE AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd	—	exists_nonneg_add_of_le le_add_of_nonneg_right
le_iff_exists_one_le_mul 📖	mathematical	—	Preorder.toLE MulOne.toOne MulOneClass.toMulOne MulOne.toMul	—	exists_one_le_mul_of_le le_mul_of_one_le_right'
le_iff_forall_one_lt_le_mul 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	LT.lt.le lt_mul_of_le_of_one_lt le_of_forall_one_lt_le_mul
le_iff_forall_one_lt_lt_mul' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	lt_mul_of_le_of_one_lt le_of_forall_one_lt_lt_mul'
le_iff_forall_pos_le_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	LT.lt.le lt_add_of_le_of_pos le_of_forall_pos_le_add
le_iff_forall_pos_lt_add' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	lt_add_of_le_of_pos le_of_forall_pos_lt_add'
le_of_forall_one_lt_le_mul 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—	le_of_forall_gt_imp_ge_of_dense ExistsMulOfLE.exists_mul_of_le LT.lt.le one_lt_of_lt_mul_right
le_of_forall_one_lt_lt_mul' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	Preorder.toLE	—	le_of_forall_one_lt_le_mul LT.lt.le
le_of_forall_pos_le_add 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—	le_of_forall_gt_imp_ge_of_dense ExistsAddOfLE.exists_add_of_le LT.lt.le pos_of_lt_add_right
le_of_forall_pos_lt_add' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	Preorder.toLE	—	le_of_forall_pos_le_add LT.lt.le
lt_iff_exists_one_lt_mul 📖	mathematical	—	Preorder.toLT MulOne.toOne MulOneClass.toMulOne MulOne.toMul	—	exists_one_lt_mul_of_lt' lt_mul_of_one_lt_right'
lt_iff_exists_pos_add 📖	mathematical	—	Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd	—	exists_pos_add_of_lt' lt_add_of_pos_right

---

← Back to Index