embDomain_apply — Mathlib

English

For an embedding f and a finsupp v, embDomain f v evaluated at f(a) equals v(a).

Русский

Для вложения f и функции с конечной опорой v, embDomain f v при аргументе f(a) даёт v(a).

LaTeX

$$embDomain f v (f a) = v a$$

Lean4

@[simp]
theorem embDomain_apply (f : α ↪ β) (v : α →₀ M) (a : α) : embDomain f v (f a) = v a := by
  classical
  simp_rw [embDomain, coe_mk, mem_map']
  split_ifs with h
  · refine congr_arg (v : α → M) (f.inj' ?_)
    exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
  · exact (notMem_support_iff.1 h).symm

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