Ico_succ_right_eq_insert_Ico — Mathlib

English

For all natural numbers a ≤ b, the interval Ico(a, b+1) equals insert b into Ico(a, b).

Русский

Пусть a ≤ b. Тогда Ico(a, b+1) равно вставке b в Ico(a, b).

LaTeX

$$$Ico(a, b+1) = \\mathrm{insert}\, b (Ico(a, b))$$$

Lean4

@[deprecated Finset.insert_Ico_right_eq_Ico_succ_right (since := "2025-04-24")]
theorem Ico_succ_right_eq_insert_Ico (h : a ≤ b) : Ico a (b + 1) = insert b (Ico a b) := by
  rw [Ico_succ_right, ← Ico_insert_right h]

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