Theorems · Theorem · general topology

ContinuousMap.secondCountableTopology

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SecondCountableTopology Y],
  (∃ S,
      S.Countable ∧
        (∀ K ∈ S, IsCompact K) ∧
          ∀ (f : C(X, Y)) (V : Set Y), IsOpen V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) →
    SecondCountableTopology C(X, Y)

A version of instSecondCountableTopology with a technical assumption instead of [SecondCountableTopology X] [LocallyCompactSpace X]. It is here as a reminder of what could be an intermediate goal, if someone tries to weaken the assumptions in the instance (e.g., from [LocallyCompactSpace X] to [LocallyCompactPair X Y] - not sure if it's true).

Defined in

Mathlib.Topology.ContinuousMap.SecondCountableSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceSecondCountableTopology