mk_apply_of_notMem — Mathlib

English

If n is in the index set s, the value of mk β s f at n equals f at the corresponding index.

Русский

Если n принадлежит множеству индексов s, то mk β s f n = f ⟨n, hn⟩.

LaTeX

$$$n\\in s \\Rightarrow (DirectSum.mk\\;β\\;s\\;f)\\;n = f\\;⟨n,\\,hn⟩$$$

Lean4

theorem mk_apply_of_notMem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∉ s) : mk β s f n = 0 :=
  by
  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
  rw [dif_neg hn]

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