piecewise_single_erase — Mathlib

English

Let x ∈ ∏ i β i. The function obtained by placing at i the value x i and using x.erase i elsewhere equals x.

Русский

Пусть x ∈ ∏ i β i. Функция, задаваемая на i-ом месте значением x i, а в остальных местах равная x.erase i, равна x.

LaTeX

$$$ (\\\\mathrm{single} i (x i)).\\\\mathrm{piecewise} (x \\\\mathrm{erase} i) = x $$$

Lean4

theorem piecewise_single_erase (x : Π₀ i, β i) (i : ι) : (single i (x i)).piecewise (x.erase i) { i } = x :=
  by
  ext j; rw [piecewise_apply]; split_ifs with h
  · rw [(id h : j = i), single_eq_same]
  · exact erase_ne h

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