Ioc_union_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioc_union_Ioc (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) : Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d) :=
  by
  rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;> simp [*] at h₁ h₂
  · exact Ioc_union_Ioc' h₂ h₁
  all_goals simp [*]

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