Iio_ssubset_Iio — Mathlib

English

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

Русский

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

LaTeX

$$$$Iio(a) \subsetneq Iio(b)$$$$

Lean4

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

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