Theorems · Theorem · order theory
lt_add_of_le_of_pos
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b c : α},
b ≤ c → 0 < a → b < c + a- Cited by
- 11 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- add_zeroproof · cited by 2,707
- AddZeroClassstatement and proof · cited by 1,237
- AddLeftStrictMonostatement and proof · cited by 203
- add_lt_add_rightproof · cited by 50
Cited by11
Results whose statement or proof uses this declaration.
- Left.add_pos_of_nonneg_of_posproof · cited by 5
- le_iff_forall_pos_le_addproof · cited by 4
- Polynomial.finiteMultiplicity_of_degree_pos_of_monicproof · cited by 3
- le_iff_forall_pos_lt_addproof · cited by 3
- Rat.AbsoluteValue.eq_one_of_not_dvdproof · cited by 1
- Real.exists_rat_abs_sub_lt_and_lt_of_irrationalproof · cited by 1
- exists_norm_eq_iInf_of_complete_convexproof · cited by 1
- HasCompactSupport.exists_pos_le_normproof · cited by 1
- PythagoreanTriple.ne_zero_of_coprimeproof · cited by 1
- le_iff_forall_pos_lt_add'proof · cited by 0
- HasCompactMulSupport.exists_pos_le_normproof · cited by 0