mk'_apply — Mathlib

English

Let f be a function with a linearity proof lin. Then the evaluation of the constructed linear map mk' f lin at x equals f(x).

Русский

Пусть f — функция с доказательством линейности lin. Тогда значение построенного линейного отображения mk' f lin в точке x равно f(x).

LaTeX

$$$(\mathrm{mk'}(f,\mathrm{lin}))(x) = f(x)$$$

Lean4

@[simp]
theorem mk'_apply {f : M → M₂} (lin : IsLinearMap R f) (x : M) : mk' f lin x = f x :=
  rfl

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