range_cons — Mathlib

English

For any x ∈ α and b : Fin n → α, the range of Fin.cons x b is the insert of x into the range of b.

Русский

Для любого x ∈ α и b: Fin n → α, образ Fin.cons x b равен добавлению x в образ b: Set.range (Fin.cons x b) = insert x (Set.range b).

LaTeX

$$$\\mathrm{Set.range}(\\mathrm{Fin.cons}\\, x\\, b) = \\mathrm{Set.insert}\\, x\\bigl(\\mathrm{Set.range}\\, b\\bigr).$$$

Lean4

@[simp]
theorem range_cons {α} {n : ℕ} (x : α) (b : Fin n → α) :
    Set.range (Fin.cons x b : Fin n.succ → α) = insert x (Set.range b) := by rw [range_fin_succ, cons_zero, tail_cons]

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