English
Let X be a space and f : X → ∏_{i} A_i. The topology on X that makes f continuous into the product topology on ∏ A_i is the infimum of the initial topologies induced by each coordinate map f · i : X → A_i. In particular, Induced(f, ∏ A_i) = ⨅ i, Induced(f · i, A_i).
Русский
Пусть X — пространство, и f: X → ∏_{i} A_i. Топология на X, делающая f непрерывной относительно произведения сверху ∏ A_i, есть наименьшая из начальних топологий, задаваемых каждой координатной картой f_i: X → A_i. Иными словами, Induced(f, ∏ A_i) = ⨅ i, Induced(f · i, A_i).
LaTeX
$$$\\operatorname{Induced}(f, \\Pi_{i} A_i) = \\bigwedge_{i} \\operatorname{Induced}(f \\cdot i, A_i)$$$
Lean4
theorem induced_to_pi {X : Type*} (f : X → ∀ i, A i) :
induced f Pi.topologicalSpace = ⨅ i, induced (f · i) inferInstance := by
simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp_def]
