Theorems · Theorem · order theory
add_pos_of_pos_of_nonneg
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, 0 < a → 0 ≤ b → 0 < a + bAlias of Left.add_pos_of_pos_of_nonneg.
- Cited by
- 63 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
- AddZeroClassstatement · cited by 1,237
- AddLeftMonostatement · cited by 687
- Left.add_pos_of_pos_of_nonnegproof · cited by 6
Cited by63
Results whose statement or proof uses this declaration.
- Real.smoothTransition.pos_denomproof · cited by 8
- Real.rpowIntegrand₀₁_eq_pow_divproof · cited by 6
- InnerProductSpace.HarmonicOnNhd.circleAverage_eqproof · cited by 5
- Real.cosh_arcoshproof · cited by 3
- Function.hasTemperateGrowth_iff_isBigOproof · cited by 3
- Function.hasTemperateGrowth_norm_sqproof · cited by 3
- TemperedDistribution.besselPotential_besselPotential_applyproof · cited by 3
- Polynomial.finiteMultiplicity_of_degree_pos_of_monicproof · cited by 3
- Real.rpow_add_of_nonnegproof · cited by 3
- integrable_rpow_neg_one_add_norm_sqproof · cited by 2
- unitInterval.add_posproof · cited by 2
- Real.convexOn_Gammaproof · cited by 2