exists_extend — Mathlib

English

Any linear map f defined on a subspace p can be extended to a linear map on the whole space.

Русский

Любое линейное отображение f, заданное на подплощине p, можно продолжить до линейного отображения на всю пространство.

LaTeX

$$$\exists g : V \to P',\; g \circ p.\mathrm{subtype} = f$$$

Lean4

/-- Any linear map `f : p →ₗ[K] V'` defined on a subspace `p` can be extended to the whole
space. -/
theorem exists_extend {p : Submodule K V} (f : p →ₗ[K] V') : ∃ g : V →ₗ[K] V', g.comp p.subtype = f :=
  let ⟨g, hg⟩ := p.subtype.exists_leftInverse_of_injective p.ker_subtype
  ⟨f.comp g, by rw [LinearMap.comp_assoc, hg, f.comp_id]⟩

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