OAI/Analysis/CircleDomains/Probability/GDeltaPolish.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A G-delta subset of a Polish space is Polish. It embeds as the closed set of compatible tuples in the product of its open supersets.

  1. lemma OAI.CircleDomainRigidity.polishSpace_of_isGDelta line 12