OAI/Analysis/CircleDomains/Selection/ContinuousScalarRepresentative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual weak scalar has a continuous representative on the sphere. The representative uses the source quotient on every matched end.

  1. def OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar line 20
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_continuous line 23
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_unit line 29
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_on_image line 32
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_eq_imageScalar line 38
  6. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.eq_continuedScalar_ae line 45