Iio_union_Ico' — Mathlib

English

For any b, c, d with c ≤ b, we have (−∞, b) ∪ [c,d) = (−∞, max(b,d)).

Русский

Для любых b, c, d с c ≤ b выполняется (−∞, b) ∪ [c,d) = (−∞, max(b,d)).

LaTeX

$$$(-\infty, b) \cup [c,d) = (-\infty, \max(b,d)) \quad (c \le b).$$

Lean4

theorem Iio_union_Ico' (h₁ : c ≤ b) : Iio b ∪ Ico c d = Iio (max b d) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Iio, mem_Ico, lt_max_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
    tauto

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