OAI/Analysis/CircleDomains/Selection/ScalarRegionLowerRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Lower range propagation for the same actual weak scalar.

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