extendWith_zero — Mathlib

English

ExtendWith x 0 on the zero part yields the dfinsupp with none mapped to x.

Русский

ExtendWith x 0 применяем к нулевой части даёт dfinsupp с none, отображённой в x.

LaTeX

$$$\\mathrm{extendWith}\\, x\\, 0 = \\mathrm{single}\\, \\mathrm{none} \\; x$$$

Lean4

@[simp]
theorem extendWith_zero [DecidableEq ι] [∀ i, Zero (α i)] (x : α none) :
    (0 : Π₀ i, α (some i)).extendWith x = single none x :=
  by
  ext (_ | j)
  · rw [extendWith_none, single_eq_same]
  · rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]

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