Iio_subset_Iic_union_Ico — Mathlib

English

Let α be a linearly ordered set. For any a,b ∈ α, the interval (-∞, b) is contained in (-∞, a] ∪ [a, b).

Русский

Пусть α — линейно упорядоченное множество. Для любых a,b ∈ α выполняется Iio b ⊆ Iic a ∪ Ico a b.

LaTeX

$$$Iio(b) \subseteq Iic(a) \cup Ico(a,b)$$$

Lean4

theorem Iio_subset_Iic_union_Ico : Iio b ⊆ Iic a ∪ Ico a b :=
  Subset.trans Iio_subset_Iic_union_Ioo (union_subset_union_right _ Ioo_subset_Ico_self)

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