Theorems · Definition · general topology

Metric.PiNatEmbed.toPiNatHomeo

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

Homeomorphism between X and its embedding into ∀ i, Y i induced by a separating family of continuous functions f i : X → Y i.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

3 results in Mathlib

Foundations

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

Assumes

EncodableMetricSpaceTopologicalSpaceCompactSpace