English
If maps X₁→Y₁, Z₁→Y₁, X₂→Y₂, Z₂→Y₂ form a commutative square with continuous maps mapX and mapZ, then the induced mapPullback is continuous.
Русский
Если карты образуют коммутативную квадратную схему и mapX, mapZ непрерывны, тогда сопряжённая карта mapPullback непрерывна.
LaTeX
$$$$\\text{Continuous}(\\mathrm{Function.mapPullback}(mapX,mapY,mapZ,commX,commZ)).$$$$
Lean4
theorem mapPullback {X₁ X₂ Y₁ Y₂ Z₁ Z₂} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z₁]
[TopologicalSpace Z₂] {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂} {mapX : X₁ → X₂}
(contX : Continuous mapX) {mapY : Y₁ → Y₂} {mapZ : Z₁ → Z₂} (contZ : Continuous mapZ)
{commX : f₂ ∘ mapX = mapY ∘ f₁} {commZ : g₂ ∘ mapZ = mapY ∘ g₁} :
Continuous (Function.mapPullback mapX mapY mapZ commX commZ) := by
refine continuous_induced_rng.mpr (.prodMk ?_ ?_) <;>
apply_rules [continuous_fst, continuous_snd, continuous_subtype_val, Continuous.comp]
