Theorems · Theorem · general topology

Metric.PiNatEmbed.isHomeomorph_toPiNat

∀ {ι : 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) → IsHomeomorph Metric.PiNatEmbed.toPiNat

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

0 results in Mathlib

Foundations

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

Assumes

EncodableMetricSpaceTopologicalSpaceCompactSpace