Theorems · Inductive type · order theory
ExistsAddOfLE
(α : Type u) → [Add α] → [LE α] → Prop
An ordered additive monoid with one-sided 'subtraction' in the sense that
if a ≤ b, then there is some c for which a + c = b. This is a weaker version
of the condition on canonical orderings defined by CanonicallyOrderedAdd.
- Cited by
- 330 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by334
Results whose statement or proof uses this declaration.
- tsub_add_cancel_of_lestatement and proof · cited by 112
- sq_nonnegstatement and proof · cited by 106
- Even.pow_nonnegstatement and proof · cited by 94
- add_tsub_cancel_of_lestatement and proof · cited by 79
- mul_nonneg_of_nonpos_of_nonposstatement and proof · cited by 45
- ExistsAddOfLE.exists_add_of_lestatement and proof · cited by 42
- mul_pos_of_neg_of_negstatement and proof · cited by 40
- mul_self_nonnegstatement and proof · cited by 35
- tsub_add_eq_add_tsubstatement and proof · cited by 23
- tendsto_pow_atTop_atTop_of_one_ltstatement and proof · cited by 22
- tendsto_pow_atTop_nhds_zero_of_lt_onestatement and proof · cited by 18
- mul_self_posstatement and proof · cited by 17
Showing the 200 most cited of 334.