English
If f: X → Y and g: Z → W induce topologies on X and Z, then the product topology on X × Z is induced by the product map (f,g).
Русский
Если f: X→Y и g: Z→W индуцируют топологии на X и Z, то топология произведения X×Z индуцируется по произведению отображений (f,g).
LaTeX
$$$$\text{TopProd}(X,Z;\operatorname{induced} f,\operatorname{induced} g) = \operatorname{induced}(\lambda p:(X\times Z)\mapsto (f(p.1), g(p.2))).$$$$
Lean4
/-- A product of induced topologies is induced by the product map -/
theorem prod_induced_induced {X Z} (f : X → Y) (g : Z → W) :
@instTopologicalSpaceProd X Z (induced f ‹_›) (induced g ‹_›) =
induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd :=
by
delta instTopologicalSpaceProd
simp_rw [induced_inf, induced_compose]
rfl
