Theorems · Theorem · general topology

IsOpenMap.piMap

∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i},
  (∀ (i : ι), IsOpenMap (f i)) → (∀ᶠ (i : ι) in Filter.cofinite, Function.Surjective (f i)) → IsOpenMap (Pi.map f)

Defined in

Mathlib.Topology.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace