isCompl

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#LinearMap.IsIdempotentElem.isCompl

English

If f is idempotent, then range f and ker f form a decomposition of the space.

Русский

Если f идемпотентно, то образ f и ядро f образуют разложение пространства.

LaTeX

$$IsCompl( range f, ker f )$$

Lean4

theorem isCompl {f : E →ₗ[R] E} (hf : IsIdempotentElem f) : IsCompl (range f) (ker f) :=
  hf.isProj_range.isCompl

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

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

Разделы

Аффилиация

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