Ioi_ssubset_Ioi — Mathlib

English

If a < b, then the interval (b, ∞) is strictly contained in (a, ∞).

Русский

Если a < b, то (b, ∞) вложено строго в (a, ∞).

LaTeX

$$$$Ioi(b) \subsetneq Ioi(a)$$$$

Lean4

/-- If `a < b`, then `(b, +∞) ⊂ (a, +∞)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Ioi_ssubset_Ioi_iff`. -/
@[gcongr]
theorem Ioi_ssubset_Ioi (h : a < b) : Ioi b ⊂ Ioi a :=
  (ssubset_iff_of_subset (Ioi_subset_Ioi h.le)).mpr ⟨b, h, lt_irrefl b⟩

Похожие утверждения