Theorems · Theorem · general topology

Continuous.mapPullback

∀ {X₁ : Type u_1} {X₂ : Type u_2} {Y₁ : Sort u_3} {Y₂ : Sort u_4} {Z₁ : Type u_5} {Z₂ : Type u_6}
  [inst : TopologicalSpace X₁] [inst_1 : TopologicalSpace X₂] [inst_2 : TopologicalSpace Z₁]
  [inst_3 : TopologicalSpace Z₂] {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂} {mapX : X₁ → X₂},
  Continuous mapX →
    ∀ {mapY : Y₁ → Y₂} {mapZ : Z₁ → Z₂},
      Continuous mapZ →
        ∀ {commX : f₂ ∘ mapX = mapY ∘ f₁} {commZ : g₂ ∘ mapZ = mapY ∘ g₁},
          Continuous (Function.mapPullback mapX mapY mapZ commX commZ)

Defined in

Mathlib.Topology.SeparatedMap

Cited by

3 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpace