induced — Mathlib

English

There are canonical maps from the induced topology to each X_i, given by the original maps f_i.

Русский

Существуют канонические отображения из возведённой (induced) топологии к каждому X_i, задаваемые отображениями f_i.

LaTeX

$$$\\text{fromInduced}(i) : \\mathrm{induced}(f) \\to X_i$ for each i.$$

Lean4

/-- The induced topology on `M` from a family of continuous linear maps from `M`, which is the
coarsest topology that makes every map continuous. -/
def induced : TopModuleCat R :=
  letI : TopologicalSpace M := ⨅ i, (X i).topologicalSpace.induced (f i)
  have : ContinuousAdd M := continuousAdd_iInf fun _ ↦ continuousAdd_induced _
  have : ContinuousSMul R M := continuousSMul_iInf fun _ ↦ continuousSMul_induced _
  .of R M

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