Ico_pred_right_eq_insert — Mathlib

English

For a ≤ b, the half-open interval (pred a, b] equals {a} ∪ (a, b].

Русский

При a ≤ b полупрозрачный интервал (pred a, b] равен {a} ∪ (a, b].

LaTeX

$$$ Ioc(\\mathrm{pred}\\ a)\\ b = \\mathrm{insert}\\ a\\ (Ioc\\ a\\ b) \\quad \\text{for } a \\le b $$$

Lean4

theorem Ico_pred_right_eq_insert (h : a ≤ b) : Ioc (pred a) b = insert a (Ioc a b) := by
  simp_rw [← Ioi_inter_Iic, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iic.2 h)]

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