Theorems · Theorem · general topology

TopologicalSpace.exists_isInducing_l_infty

∀ (X : Type u_1) [inst : TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X], ∃ f, Topology.IsInducing f

For a regular topological space with second countable topology, there exists an inducing map to l^∞ = ℕ →ᵇ ℝ.

Defined in

Mathlib.Topology.Metrizable.Urysohn

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceRegularSpaceSecondCountableTopology