linearProjOfIsCompl_apply_left

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#Submodule.linearProjOfIsCompl_apply_left

English

If x ∈ p, then linearProjOfIsCompl p q h x = x.

Русский

Если x ∈ p, тогда линейная проекция возвращает x.

LaTeX

$$$\text{If } x \in p,\; \text{linearProjOfIsCompl } p q h(x) = x$$$

Lean4

@[simp]
theorem linearProjOfIsCompl_apply_left (h : IsCompl p q) (x : p) : linearProjOfIsCompl p q h x = x := by
  simp [linearProjOfIsCompl]

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

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

Разделы

Аффилиация

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