Ioo_union_Ioo' — Mathlib

English

If c < b and a < d, then Ioo a b ∪ Ioo c d = Ioo(min(a,c), max(b,d)).

Русский

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

LaTeX

$$$(c < b) \land (a < d) \implies \mathrm{Ioo}(a,b) \cup \mathrm{Ioo}(c,d) = \mathrm{Ioo}(\min(a,c), \max(b,d))$$$

Lean4

theorem Ioo_union_Ioo' (h₁ : c < b) (h₂ : a < d) : Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Ioo, min_lt_iff, lt_max_iff]
  by_cases hc : c < x <;> by_cases hd : x < d
  · tauto
  · have hax : a < x := h₂.trans_le (le_of_not_gt hd)
    tauto
  · have hxb : x < b := (le_of_not_gt hc).trans_lt h₁
    tauto
  · tauto

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