OAI/Analysis/CircleDomains/Selection/FixedRealExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed source real barrier gives an open exclusion of conformal maps. The neighborhood retains only compact source traces; later model limits may use different core exhaustions.

  1. theorem OAI.CircleDomainRigidity.exists_open_fixed_core_real_exclusion line 15