codRestrict_apply — Mathlib

English

If g = f.codRestrict P h is the restricted map, then its value on any m is exactly f(m) (viewed in N).

Русский

Если g = f.codRestrict P h — ограниченное отображение, то для любого m равно f(m) (считая как элемент N).

LaTeX

$$(f.codRestrict P h)(m) = f(m)$$

Lean4

@[simp]
theorem codRestrict_apply (P : LieSubmodule R L N) (f : M →ₗ⁅R,L⁆ N) (h : ∀ m, f m ∈ P) (m : M) :
    (f.codRestrict P h m : N) = f m :=
  rfl

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