Iio_union_Ioo — Mathlib

English

Let α be a linearly ordered set and min{c,d} < b. Then Iio(b) ∪ Ioo(c,d) = Iio(max{b,d}).

Русский

Пусть α — линейно упорядочено. Пусть min{c,d} < b. Тогда Iio(b) ∪ Ioo(c,d) = Iio(max{b,d}).

LaTeX

$$$ \min(c,d) < b \implies Iio(b) \cup Ioo(c,d) = Iio(\max(b,d)). $$$

Lean4

theorem Iio_union_Ioo (h : min c d < b) : Iio b ∪ Ioo c d = Iio (max b d) :=
  by
  rcases le_total c d with hcd | hcd
  · simp only [hcd, inf_of_le_left] at h; exact Iio_union_Ioo' h
  · rw [max_comm]
    simp_all [max_eq_right_of_lt]

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