OAI/Analysis/CircleDomains/Topology/ScalarCircleModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The null trace-pair hypothesis gives a circle-domain model retaining exactly the prescribed continuous smooth scalar tests.

  1. def OAI.CircleDomainRigidity.RetainedRealCircleModel.select line 18
  2. theorem OAI.CircleDomainRigidity.exists_retained_scalar_circle_model line 33