DenselyOrdered

📁 Source: Mathlib/Algebra/Order/Group/DenselyOrdered.lean

Statistics

Metric	Count
Definitions	0
Theorems add_le_of_forall_lt, exists_lt_nsmul_of_neg, exists_lt_pow_of_lt_one, exists_nsmul_lt_of_pos, exists_pow_lt_of_one_lt, le_add_of_forall_lt, le_iff_forall_lt_one_mul_le, le_iff_forall_neg_add_le, le_mul_of_forall_lt, le_of_forall_lt_one_mul_le, le_of_forall_neg_add_le, le_of_forall_one_lt_div_le, le_of_forall_pos_sub_le, mul_le_of_forall_lt	14
Total	14

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_le_of_forall_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	le_of_forall_lt_imp_le_of_dense IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono LE.le.trans LT.lt.le
exists_lt_nsmul_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	exists_nsmul_lt_of_pos AddGroup.existsAddOfLE neg_pos_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid neg_neg_of_pos neg_nsmul lt_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add
exists_lt_pow_of_lt_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Monoid.toPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	exists_pow_lt_of_one_lt Group.existsMulOfLE one_lt_inv_of_inv IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid inv_lt_one_of_one_lt inv_pow IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_mul_of_covariant_mul
exists_nsmul_lt_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoid.toNSMul	—	zero_nsmul one_nsmul exists_between LT.lt.trans_le' nsmul_left_monotone IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid LT.lt.le mul_nsmul nsmul_le_nsmul_right covariant_swap_add_of_covariant_add
exists_pow_lt_of_one_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Monoid.toPow	—	pow_zero pow_one exists_between LT.lt.trans_le' pow_right_monotone IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid LT.lt.le pow_mul pow_le_pow_left' covariant_swap_mul_of_covariant_mul
le_add_of_forall_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	le_of_forall_gt_imp_ge_of_dense IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono LE.le.trans LT.lt.le
le_iff_forall_lt_one_mul_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	le_iff_forall_one_lt_le_mul OrderDual.denselyOrdered Group.existsMulOfLE OrderDual.mulLeftReflectLT contravariant_lt_of_covariant_le OrderDual.mulLeftStrictMono IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE Group.covconv
le_iff_forall_neg_add_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	le_iff_forall_pos_le_add OrderDual.denselyOrdered AddGroup.existsAddOfLE OrderDual.addLeftReflectLT contravariant_lt_of_covariant_le OrderDual.addLeftStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv
le_mul_of_forall_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	le_of_forall_gt_imp_ge_of_dense IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT instIsLeftCancelMulOfMulLeftReflectLE Group.covconv contravariant_lt_of_covariant_le covariant_swap_mul_of_covariant_mul IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LE.le.trans LT.lt.le
le_of_forall_lt_one_mul_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_of_forall_one_lt_le_mul OrderDual.denselyOrdered Group.existsMulOfLE OrderDual.mulLeftReflectLT contravariant_lt_of_covariant_le
le_of_forall_neg_add_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_of_forall_pos_le_add OrderDual.denselyOrdered AddGroup.existsAddOfLE OrderDual.addLeftReflectLT contravariant_lt_of_covariant_le
le_of_forall_one_lt_div_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv Group.toDivInvMonoid	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_of_forall_lt_one_mul_le div_eq_mul_inv inv_inv Left.one_lt_inv_iff IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE Group.covconv
le_of_forall_pos_sub_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_of_forall_neg_add_le sub_eq_add_neg neg_neg Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv
mul_le_of_forall_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	le_of_forall_lt_imp_le_of_dense IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT instIsLeftCancelMulOfMulLeftReflectLE Group.covconv contravariant_lt_of_covariant_le covariant_swap_mul_of_covariant_mul IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LE.le.trans LT.lt.le

---

← Back to Index