Theorems · Theorem · order theory
lt_add_of_pos_of_le
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b c : α},
0 < a → b ≤ c → b < a + c- Cited by
- 6 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
- zero_addproof · cited by 2,366
- AddZeroClassstatement and proof · cited by 1,237
- AddRightStrictMonostatement and proof · cited by 160
- add_lt_add_leftproof · cited by 47
Cited by6
Results whose statement or proof uses this declaration.
- SchwartzMap.eLpNorm_le_seminormproof · cited by 2
- PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_posproof · cited by 1
- MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_topproof · cited by 1
- Right.add_pos_of_pos_of_nonnegproof · cited by 1
- PythagoreanTriple.ne_zero_of_coprimeproof · cited by 1
- Complex.HadamardThreeLines.norm_lt_sSupNormIm_epsproof · cited by 1