Ioc_union_Ioc' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioc_union_Ioc' (h₁ : c ≤ b) (h₂ : a ≤ d) : Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Ioc, min_lt_iff, le_max_iff]
  by_cases hc : c < x <;> by_cases hd : x ≤ d
  · tauto
  · have hax : a < x := h₂.trans_lt (lt_of_not_ge hd)
    tauto
  · have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
    tauto
  · tauto

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