Ioc_union_Ioc_eq_Ioc — Mathlib

English

For any a,b,c,d, if c ≤ b and a ≤ d, then Ico a b ∪ Ico c d = Ico(min a c, max b d).

Русский

Для любых a,b,c,d, если c ≤ b и a ≤ d, то Ico(a,b) ∪ Ico(c,d) = Ico(min a c, max b d).

LaTeX

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

Lean4

@[simp]
theorem Ioc_union_Ioc_eq_Ioc {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Ioc a b ∪ Ioc b c = Ioc a c := by
  rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]

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