OAI/Analysis/CircleDomains/Topology/SubarcGenericLevels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Generic prior levels survive measurable subarc selection and the factor-two compact conditioning used for terminal arc laws. The free set need not be measurable: finite Borel count inequalities carry the statement.

  1. theorem OAI.CircleDomainRigidity.subarc_generic_levels line 19
  2. theorem OAI.CircleDomainRigidity.IsSubarcLawReduction.generic_levels line 80