Theorems · Theorem · order theory
lt_add_of_pos_right
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftStrictMono α] (a : α) {b : α}, 0 < b → a < a + b- Cited by
- 51 results in Mathlib
- Foundations
- Depth 6 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.
- 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 by51
Results whose statement or proof uses this declaration.
- lt_add_oneproof · cited by 105
- zsmul_left_strictMonoproof · cited by 8
- BoxIntegral.unitPartition.tag_memproof · cited by 4
- gauge_add_leproof · cited by 4
- MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnormproof · cited by 4
- nsmul_left_strictMonoproof · cited by 4
- exists_lt_rieszContentAux_add_posproof · cited by 4
- QuotientAddGroup.exists_norm_mk_ltproof · cited by 3
- Nat.Partrec.Code.encode_lt_pairproof · cited by 3
- Real.strictMono_eulerMascheroniSeqproof · cited by 3
- AddCommGroup.tfae_modEqproof · cited by 3
- Metric.cthickening_eq_iInter_cthickening'proof · cited by 3