Theorems · Theorem · order theory
le_iff_exists_add
∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] {a b : α}, a ≤ b ↔ ∃ c, b = a + c- Cited by
- 16 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- AddLECanonicallyOrderedAdd
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CanonicallyOrderedAddstatement and proof · cited by 229
- le_self_addproof · cited by 68
- ExistsAddOfLE.exists_add_of_leproof · cited by 42
Cited by16
Results whose statement or proof uses this declaration.
- le_iff_exists_add'proof · cited by 7
- Finset.HasAntidiagonal.antidiagonal.fst_leproof · cited by 6
- Finset.HasAntidiagonal.antidiagonal.snd_leproof · cited by 3
- Polynomial.resultant_mul_rightproof · cited by 3
- MeasureTheory.extend_monoproof · cited by 2
- add_tsub_cancel_iff_leproof · cited by 2
- Finsupp.exists_le_degree_eqproof · cited by 1
- Finsupp.degree_preimage_addproof · cited by 1
- Nat.range_mul_addproof · cited by 1
- lt_iff_exists_addproof · cited by 1
- PowerSeries.HasSubst.eventually_coeff_pow_eq_zeroproof · cited by 1
- nsmul_eq_nsmul_of_modEqproof · cited by 0