OAI/Analysis/CircleDomains/Reflection/LocalBoundaryExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local continuous extensions provide a single canonical extension to the closure. This glues boundary values without choosing compatible values by hand.

  1. lemma OAI.CircleDomainRigidity.tendsto_of_local_extension line 13
  2. lemma OAI.CircleDomainRigidity.continuousOn_extendFrom_of_local_extensions line 21
  3. lemma OAI.CircleDomainRigidity.extendFrom_eq_local_extension line 31