Ioo_subset_Iio_self — Mathlib

English

Let α be a preorder. Then for all a, b in α, the open-closed interval (a, b) is contained in the open interval (−∞, b). In symbols: Ioo(a, b) ⊆ Iio(b).

Русский

Пусть α имеет предпорядок. Тогда для всех a, b ∈ α промежуток (a, b) включён в (-∞, b). То есть Ioo(a, b) ⊆ Iio(b).

LaTeX

$$$$Ioo(a,b) \subseteq Iio(b)$$$$

Lean4

theorem Ioo_subset_Iio_self : Ioo a b ⊆ Iio b := fun _ => And.right

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