OAI/Analysis/CircleDomains/Selection/CountableDeletions.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite increasing deletions exhausting a prescribed countable mark set.

  1. theorem OAI.CircleDomainRigidity.exists_finite_deletions line 14
  2. theorem OAI.CircleDomainRigidity.exists_countable_enumeration_with_default line 31