English
For any linear map f defined on a subspace, there exists an extension g to the whole space such that g ∘ subtype = f.
Русский
Для любого линейного отображения f, заданного на подпомоства, существует продолжение g на всё пространство такое, что g ∘ подпростроение = f.
LaTeX
$$$\exists g : V \to V', \; g \circ p.susbtype = f$$$
Lean4
/-- If `V` and `V'` are nontrivial vector spaces over a field `K`, the space of `K`-linear maps
between them is nontrivial. -/
instance [Nontrivial V] [Nontrivial V'] : Nontrivial (V →ₗ[K] V') :=
by
obtain ⟨v, hv⟩ := exists_ne (0 : V)
obtain ⟨w, hw⟩ := exists_ne (0 : V')
have : v ∉ (⊥ : Submodule K V) := by simp only [mem_bot, hv, not_false_eq_true]
obtain ⟨g, _, hg⟩ := LinearMap.exists_extend_of_notMem (K := K) 0 this w
exact ⟨g, 0, DFunLike.ne_iff.mpr ⟨v, by simp_all⟩⟩
