OAI/Analysis/CircleDomains/Selection/CountableMarks.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite mandatory mark sets that eventually contain every mark.

  1. theorem OAI.CircleDomainRigidity.exists_increasing_finite_marks line 12
  2. theorem OAI.CircleDomainRigidity.exists_increasing_finite_marks_inhabited line 26