Iio_union_Ioo' — Mathlib

English

If c < b, then Iio(b) ∪ Ioo(c,d) = Iio(max{b,d}).

Русский

Если c < b, то Iio(b) ∪ Ioo(c,d) = Iio(max(b,d)).

LaTeX

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

Lean4

theorem Iio_union_Ioo' (h₁ : c < b) : Iio b ∪ Ioo c d = Iio (max b d) :=
  by
  ext x
  rcases lt_or_ge x b with hba | hba
  · simp [hba]
  · simp only [mem_Iio, mem_union, mem_Ioo, lt_max_iff]
    refine or_congr Iff.rfl ⟨And.right, ?_⟩
    exact fun h₂ => ⟨h₁.trans_le hba, h₂⟩

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