Basic

📁 Source: Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems sup'_eq_zero, sup_eq_zero, range_add_eq_image_Ici, exists_le_add_iff_le_left, exists_le_add_iff_le_right, exists_lt_add_iff_lt_left, exists_lt_add_iff_lt_right, forall_le_add_iff_le_left, forall_le_add_iff_le_right, forall_lt_add_iff_lt_left, forall_lt_add_iff_lt_right, le_add_iff_lt_left_or_exists_le, le_add_iff_lt_right_or_exists_le, lt_add_iff_lt_left_or_exists_lt, lt_add_iff_lt_right_or_exists_lt	15
Total	15

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sup'_eq_zero 📖	mathematical	Nonempty	sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sup'_eq_sup
sup_eq_zero 📖	mathematical	—	sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_add_eq_image_Ici 📖	mathematical	—	range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup image Ici PartialOrder.toPreorder	—	ext self_le_add_left tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE CanonicallyOrderedAdd.toAddLeftMono

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_add_iff_le_left 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	—
exists_le_add_iff_le_right 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd Preorder.toLT	—	—
exists_lt_add_iff_lt_left 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
exists_lt_add_iff_lt_right 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd	—	—
forall_le_add_iff_le_left 📖	—	—	—	—	—
forall_le_add_iff_le_right 📖	mathematical	—	AddCommMagma.toAdd	—	—
forall_lt_add_iff_lt_left 📖	—	—	—	—	—
forall_lt_add_iff_lt_right 📖	mathematical	—	AddCommMagma.toAdd	—	—
le_add_iff_lt_left_or_exists_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	lt_or_ge LE.le.trans LT.lt.le le_self_add ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le
le_add_iff_lt_right_or_exists_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd Preorder.toLT	—	add_comm le_add_iff_lt_left_or_exists_le
lt_add_iff_lt_left_or_exists_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	lt_or_ge LT.lt.trans_le le_self_add ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE covariant_lt_of_contravariant_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT
lt_add_iff_lt_right_or_exists_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd	—	add_comm lt_add_iff_lt_left_or_exists_lt

---

← Back to Index