English
The coinduced (final) topology on M from a family of continuous linear maps f_i : (X_i) → M is the finest topology on M for which all maps f_i are continuous and such that M becomes a topological module.
Русский
Коиндукционная (финальная) топология на M относительно семейства непрерывных линейных отображений f_i : (X_i) → M является наисверхней топологией на M, делающей все f_i непрерывными и превращающей M в топологический модуль.
LaTeX
$$$\\tau_{coind} = \\inf_i \\bigl( (X_i).topologicalSpace.coinduced (f_i) \\bigr) \\\\text{ and } \\ \\text{ContinuousAdd}(M, \\tau_{coind}), \\ \\text{ContinuousSMul}(R,M,\\tau_{coind}).$$$
Lean4
/-- The coinduced topology on `M` from a family of continuous linear maps into `M`, which is the
finest topology that makes it into a topological module and makes every map continuous. -/
def coinduced : TopModuleCat R :=
letI : TopologicalSpace M :=
sInf {t | @ContinuousSMul R M _ _ t ∧ @ContinuousAdd M t _ ∧ ∀ i, (X i).topologicalSpace.coinduced (f i) ≤ t}
have : ContinuousAdd M := continuousAdd_sInf fun _ hs ↦ hs.2.1
have : ContinuousSMul R M := continuousSMul_sInf fun _ hs ↦ hs.1
.of R M
