English
If a locally convex space F is equipped with a topology and there is a linear map f: E → F, then E, with the induced topology from f, is locally convex over 𝕜.
Русский
Если F — локально выпуклое пространство с некоторой топологией и имеется линейное отображение f: E → F, то E, оснащённое индуцированной топологией через f, локально выпукло над 𝕜.
LaTeX
$$$\text{LocallyConvexSpace } 𝕜 F \Rightarrow f: E \to F \Rightarrow \text{LocallyConvexSpace } 𝕜 E\, (t\text{.induced } f)$$$
Lean4
protected theorem induced {t : TopologicalSpace F} [LocallyConvexSpace 𝕜 F] (f : E →ₗ[𝕜] F) :
@LocallyConvexSpace 𝕜 E _ _ _ _ (t.induced f) :=
by
letI : TopologicalSpace E := t.induced f
refine
LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f) (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s)
(fun x => ?_) fun x s ⟨_, hs⟩ => hs.linear_preimage f
rw [nhds_induced]
exact (LocallyConvexSpace.convex_basis <| f x).comap f
