OAI/Geometry/PrescribedPotential/NormalizedPathCompactness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalized Path Compactness.

  1. lemma OAI.GlobalElliptic.RealSmooth.source_ofReal line 26
  2. lemma OAI.GlobalElliptic.Localizers.real_source_value_tendsto line 34
  3. theorem OAI.GlobalElliptic.GluingData.normalized_path_sequence_compact line 51