coe_mk — Mathlib

English

The function constructed from a finite support and values has the same pointwise values as the original function.

Русский

Функция, построенная из конечной опоры и значений, совпадает по точкам с исходной функцией.

LaTeX

$$$\\big(\\\\langle s,f,h \\\\rangle : α \\to_0 M\\\\big) = f$$$

Lean4

@[simp, norm_cast]
theorem coe_mk (f : α → M) (s : Finset α) (h : ∀ a, a ∈ s ↔ f a ≠ 0) : ⇑(⟨s, f, h⟩ : α →₀ M) = f :=
  rfl

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