Theorems · Theorem · general topology

ContinuousMap.compactOpen_eq_generateFrom

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set (Set X)}
  {T : Set (Set Y)},
  (∀ K ∈ S, IsCompact K) →
    TopologicalSpace.IsTopologicalBasis T →
      (∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) →
        ContinuousMap.compactOpen =
          TopologicalSpace.generateFrom
            (Set.image2 (fun K t => {f | Set.MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T})

Defined in

Mathlib.Topology.ContinuousMap.SecondCountableSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace