OAI/Analysis/CircleDomains/Rigidity/ModelPointTrace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The horizontal section and its priority interpolation are continuous at every point end of the actual scalar model. No boundary extension or upper semicontinuity assertion is an extra input.

  1. def OAI.CircleDomainRigidity.CompactScalarModel.horizontalSection line 19
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.horizontalSection_on_domain line 22
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.horizontalSection_point_trace line 30
  4. theorem OAI.CircleDomainRigidity.CompactScalarModel.priority_horizontalSection_point_trace line 55