Ioc_union_Ioc_eq_Ioc — Mathlib

English

If a ≤ b ≤ c, then Ioc a b ∪ Ioc b c = Ioc a c.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioc_union_Ioc_eq_Ioc (h₁ : a ≤ b) (h₂ : b ≤ c) : Ioc a b ∪ Ioc b c = Ioc a c :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx => ⟨hx.1, hx.2.trans h₂⟩) fun hx => ⟨h₁.trans_lt hx.1, hx.2⟩)
    Ioc_subset_Ioc_union_Ioc

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