mem_iff_map_id

Mathlib.LinearAlgebra.Projection

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

English

For a projection f with IsProj m f, x belongs to m if and only if f x = x.

Русский

Пусть f — проекция на m; тогда x ∈ m тогда и только тогда, когда f(x)=x.

LaTeX

$$$x \in m \iff f x = x.$$$

Lean4

theorem mem_iff_map_id {f : M →ₗ[S] M} (hf : IsProj m f) {x : M} : x ∈ m ↔ f x = x :=
  ⟨hf.map_id x, fun h ↦ h ▸ hf.map_mem x⟩

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

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

Разделы

Аффилиация

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