OAI/Analysis/CircleDomains/Selection/ScalarLocalizedRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local range principle applied to the actual scalar weak limit.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.le_on_cutoff_plateau line 21