domRestrict_apply — Mathlib

English

If x in the restricted domain corresponds to y in dom(f) with the same underlying point, then the restricted map evaluates to f(y).

Русский

Если элемент x в ограниченной области соответствуют y в dom(f) с тем же базовым вектором, то ограниченное отображение равно f(y).

LaTeX

$$$f\!\downarrow_S(x) = f(y) \quad\text{whenever } (x:E)=y \text{ and } x\in S\cap\operatorname{dom}(f).$$$

Lean4

theorem domRestrict_apply {f : E →ₗ.[R] F} {S : Submodule R E} ⦃x : ↥(S ⊓ f.domain)⦄ ⦃y : f.domain⦄ (h : (x : E) = y) :
    f.domRestrict S x = f y :=
  by
  have : Submodule.inclusion (by simp) x = y := by
    ext
    simp [h]
  rw [← this]
  exact LinearPMap.mk_apply _ _ _

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