OAI/Analysis/CircleDomains/Selection/FirstUncountableRecursion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The first uncountable well-order has countable strict initial segments. This is the precise index set for retaining every earlier path law.

  1. abbrev OAI.CircleDomainRigidity.FirstUncountable line 15
  2. theorem OAI.CircleDomainRigidity.firstUncountable_not_countable line 17
  3. instance OAI.CircleDomainRigidity.(instance at line 21) line 21
  4. theorem OAI.CircleDomainRigidity.exists_injective_firstUncountable line 33