exists_isCompl — Mathlib

English

If a linear map f: V → V' is injective, there exists a linear map g: V' → V such that g ∘ f = id_V.

Русский

Если линейное отображение f инъективно, существует линейное отображение g: V' → V такое, что g ∘ f = id_V.

LaTeX

$$$\exists g : V' →_R V, g \circ f = \mathrm{id}_V$$$

Lean4

theorem exists_isCompl (p : Submodule K V) : ∃ q : Submodule K V, IsCompl p q :=
  let ⟨f, hf⟩ := p.subtype.exists_leftInverse_of_injective p.ker_subtype
  ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| LinearMap.ext_iff.1 hf⟩

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