Ioi_subset_Ioi — Mathlib

English

If a ≤ b, then the interval (b, ∞) is contained in (a, ∞). In symbols: Ioi(b) ⊆ Ioi(a).

Русский

Если a ≤ b, то (b, ∞) ⊆ (a, ∞). То есть Ioi(b) ⊆ Ioi(a).

LaTeX

$$$$Ioi(b) \subseteq 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_subset_Ioi_iff`. -/
@[gcongr]
theorem Ioi_subset_Ioi (h : a ≤ b) : Ioi b ⊆ Ioi a := fun _ hx => h.trans_lt hx

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