Ico_union_Ico' — Mathlib

English

Let h1: min a b ≤ max c d and h2: min c d ≤ max a b. Then Ico a b ∪ Ico c d = Ico (min a c) (max b d).

Русский

Пусть mín(a,b) ≤ máx(c,d) и mín(c,d) ≤ máx(a,b). Тогда Ico(a,b) ∪ Ico(c,d) = Ico(min(a,c), max(b,d)).

LaTeX

$$$ (\min(a,b) \le \max(c,d)) \land (\min(c,d) \le \max(a,b)) \implies Ico(a,b) \cup Ico(c,d) = Ico(\min(a,c), \max(b,d)). $$$

Lean4

theorem Ico_union_Ico' (h₁ : c ≤ b) (h₂ : a ≤ d) : Ico a b ∪ Ico c d = Ico (min a c) (max b d) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Ico, min_le_iff, lt_max_iff]
  by_cases hc : c ≤ x <;> by_cases hd : x < d
  · tauto
  · have hax : a ≤ x := h₂.trans (le_of_not_gt hd)
    tauto
  · have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
    tauto
  · tauto

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