Theorems · Theorem · order theory
lt_add_iff_pos_right
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) {b : α},
a < a + b ↔ 0 < b- Cited by
- 13 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.
Cites5
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
- AddLeftReflectLTstatement and proof · cited by 33
- add_lt_add_iff_leftproof · cited by 30
Cited by13
Results whose statement or proof uses this declaration.
- Real.sigmoid_lt_oneproof · cited by 3
- image_le_of_liminf_slope_right_le_deriv_boundaryproof · cited by 2
- Complex.abs_re_lt_normproof · cited by 2
- AddSubmonoid.closure_image_isAddIndecomposable_baseOfproof · cited by 2
- Set.nonempty_inter_of_le_ncard_add_ncardproof · cited by 1
- ENNReal.exists_upcrossings_of_not_bounded_underproof · cited by 1
- Pell.Solution₁.exists_pos_of_not_isSquareproof · cited by 1
- tendsto_div_of_monotone_of_exists_subseq_tendsto_divproof · cited by 1
- ArchimedeanClass.pos_of_pos_of_mk_ltproof · cited by 1
- denseRange_zsmul_iff_surjectiveproof · cited by 1
- Set.nonempty_inter_of_lt_ncard_add_ncardproof · cited by 0