OAI/Analysis/CircleDomains/Selection/UncountableChoice.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Countable collar and arc choices can be made uniform on an uncountable set.

  1. theorem OAI.CircleDomainRigidity.exists_uncountable_common_choice line 14
  2. theorem OAI.CircleDomainRigidity.exists_lt_of_uncountable line 26
  3. theorem OAI.CircleDomainRigidity.exists_common_four_circle_arcs line 35