OAI/Analysis/CircleDomains/Selection/InnerMeanCoordinateExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Select the integration curve before its enclosing inner period mask. The disk coordinate is used only inside its genuine outer Jordan disk.

  1. theorem OAI.CircleDomainRigidity.exists_gated_small_inner_mean_exclusion line 21