Theorems · Theorem · order theory
add_lt_add
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c d : α},
a < b → c < d → a + c < b + dAlias of add_lt_add_of_lt_of_lt.
- Cited by
- 35 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
- AddLeftStrictMonostatement · cited by 203
- AddRightStrictMonostatement · cited by 160
- add_lt_add_of_lt_of_ltproof · cited by 13
Cited by35
Results whose statement or proof uses this declaration.
- CauSeq.abv_pos_of_not_limZeroproof · cited by 6
- CauSeq.add_limZeroproof · cited by 6
- multipliable_one_add_of_summableproof · cited by 4
- uniformContinuous_distproof · cited by 4
- rieszContentAux_sup_leproof · cited by 3
- IsCauSeq.cauchy₂proof · cited by 3
- cauchySeq_bddproof · cited by 3
- StrictConvexOn.addproof · cited by 2
- Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSetproof · cited by 2
- IsCauSeq.of_abv_leproof · cited by 2
- Metric.PiNatEmbed.separationproof · cited by 2
- tendsto_tsum_of_dominated_convergenceproof · cited by 2