OAI/Analysis/CircleDomains/Selection/CompleteEmbeddingGDelta.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A completely metrizable subspace of a metrizable space is a G-delta. The open sets below bound the diameter of their inverse images. A sequence approaching a point in all these sets is Cauchy in the complete source metric.

  1. lemma OAI.CircleDomainRigidity.isGDelta_range_embedding line 14