Theorems · Theorem · general topology

Metric.PiNatEmbed.toPiNatHomeo_apply_ofPiNat

∀ {ι : 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] [inst_3 : CompactSpace X]
  (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun x y => ∃ i, f i x ≠ f i y) (ofPiNat : X),
  ((Metric.PiNatEmbed.toPiNatHomeo X Y f continuous_f separating_f) ofPiNat).ofPiNat = ofPiNat

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

0 results in Mathlib

Foundations

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

Assumes

EncodableMetricSpaceTopologicalSpaceCompactSpace