Icc_union_Ico_eq_Ico — Mathlib

English

If a ≤ b and b < c, then Icc a b ∪ Ico b c = Ico a c.

Русский

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

LaTeX

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

Lean4

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

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