Ioc_union_Ioo_eq_Ioo — Mathlib

English

If a ≤ b and b < c, then Ioc(a,b) ∪ Ioo(b,c) = Ioo(a,c).

Русский

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

LaTeX

$$$ a \le b \land b < c \implies Ioc(a,b) \cup Ioo(b,c) = Ioo(a,c). $$$

Lean4

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

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