support_update_ne_zero — Mathlib

English

If updating at i with a nonzero value b, the new support is the insertion of i into the old support.

Русский

Если обновлять i-й координатой значением b ≠ 0, новая опора есть вставка i в старую опору.

LaTeX

$$$\\operatorname{support}(\\mathrm{f}.\\mathrm{update}\\ i\\ b) = \\operatorname{insert} i\, f.{\\mathrm{support}}$$$

Lean4

theorem support_update_ne_zero (f : Π₀ i, β i) (i : ι) {b : β i} (h : b ≠ 0) :
    support (f.update i b) = insert i f.support := by
  ext j
  rcases eq_or_ne i j with (rfl | hi)
  · simp [h]
  · simp [hi.symm]

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