codRestrict_apply

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#LinearMap.IsProj.codRestrict_apply

English

For x in M, the image under codRestrict equals f(x) regarded in p.

Русский

Для каждого элемента x из M образ под codRestrict совпадает с f(x) в p.

LaTeX

$$$\uparrow( h.\text{codRestrict } x) = f x.$$$

Lean4

@[simp]
theorem codRestrict_apply {f : M →ₗ[S] M} (h : IsProj m f) (x : M) : ↑(h.codRestrict x) = f x :=
  f.codRestrict_apply m x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru