range_snoc — Mathlib

English

The range of the snoc-constructed function equals inserting the new last element into the range of the original function: Set.range (snoc f x) = insert x (Set.range f).

Русский

Образ диапазона функции, полученной через snoc, равен вставке нового последнего элемента в диапазон исходной функции.

LaTeX

$$$\\mathrm{Set.range}(\\mathrm{snoc}\\ f\\ x) = \\mathrm{Set.insert}\\ x (\\mathrm{Set.range}\\ f)$$$

Lean4

@[simp]
theorem range_snoc {α : Type*} (f : Fin n → α) (x : α) : Set.range (snoc f x) = insert x (Set.range f) := by ext;
  simp [Fin.exists_fin_succ', or_comm, eq_comm]

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