English
Let ι' be a type and φ: ι' → ι. The topology on the space of all families (∀ i, A_i) induced by precomposition with φ equals the infimum over i' of the topologies induced by eval(φ i').
Русский
Пусть φ: ι' → ι. Топология на пространстве всех семейств ∀ i, A_i, индуцированная предварительным композиционным отображением f ↦ f ∘ φ, равна пересечению (iInf) топологий, индуцированных eval(φ i') на T(φ i').
LaTeX
$$$TopologicalSpace.induced(\\lambda f\\, j\\;\\mapsto f(\\phi j))\\; \\Pi_{top} = \\bigwedge_{i'}\\!\\;TopologicalSpace.induced(\\mathrm{eval}(\\phi(i')))\\,(T(\\phi(i')))$$$
Lean4
theorem induced_precomp' {ι' : Type*} (φ : ι' → ι) :
induced (fun (f : (∀ i, A i)) (j : ι') ↦ f (φ j)) Pi.topologicalSpace = ⨅ i', induced (eval (φ i')) (T (φ i')) := by
simp [Pi.topologicalSpace, induced_iInf, induced_compose, comp_def]
