Icc_union_Icc' — Mathlib

English

If c ≤ b and a ≤ d, then Icc a b ∪ Icc c d = Icc (min a c) (max b d).

Русский

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

LaTeX

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

Lean4

theorem Icc_union_Icc' (h₁ : c ≤ b) (h₂ : a ≤ d) : Icc a b ∪ Icc c d = Icc (min a c) (max b d) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Icc, min_le_iff, le_max_iff]
  by_cases hc : c ≤ x <;> by_cases hd : x ≤ d
  · tauto
  · have hax : a ≤ x := h₂.trans (le_of_not_ge hd)
    tauto
  · have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
    tauto
  · tauto

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