English
Let φ: ι' → ι. The induced topology by precomposition with φ on the full function space equals the infimum of the induced topologies via eval(φ i') with TopologicalSpace Y.
Русский
Пусть φ: ι' → ι. Индукцированная топология по предкомпозиции с φ на пространстве всех функций равна пересечению топологий, индуцированных eval(φ i') на ‹TopologicalSpace Y›.
LaTeX
$$$\\operatorname{induced}(\\cdot \\circ \\phi)\\,\\Pi^{top} = \\bigwedge_{i'}\\;\\operatorname{induced}(\\mathrm{eval}(\\phi(i')))\\,\\langle \\text{TopologicalSpace } Y\\rangle$$$
Lean4
theorem induced_precomp [TopologicalSpace Y] {ι' : Type*} (φ : ι' → ι) :
induced (· ∘ φ) Pi.topologicalSpace = ⨅ i', induced (eval (φ i')) ‹TopologicalSpace Y› :=
induced_precomp' φ
