Theorems · Theorem · general topology

Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating

∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} [Encodable ι] [inst : (i : ι) → MetricSpace (Y i)]
  [inst_1 : TopologicalSpace X] [CompactSpace X] (f : (i : ι) → X → Y i),
  (∀ (i : ι), Continuous (f i)) → (Pairwise fun x y => ∃ i, f i x ≠ f i y) → TopologicalSpace.MetrizableSpace X

If X is compact, and there exists a sequence of continuous functions f i : X → Y i to metric spaces Y i that separate points on X, then X is metrizable.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

1 results in Mathlib

Foundations

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

Assumes

EncodableMetricSpaceTopologicalSpaceCompactSpace