OAI/Geometry/PrescribedPotential/GlobalPartition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Global Partition.

  1. def OAI.GlobalElliptic.Smooth.ofReal line 20
  2. lemma OAI.GlobalElliptic.Smooth.ofReal_apply line 26
  3. lemma OAI.GlobalElliptic.Smooth.ofReal_tsupport line 29
  4. structure OAI.GlobalElliptic.Localizers line 37
  5. def OAI.GlobalElliptic.Localizers.coordinates line 47
  6. lemma OAI.GlobalElliptic.Localizers.coordinates_injective line 64
  7. def OAI.GlobalElliptic.Localizers.closedSpace line 87
  8. abbrev OAI.GlobalElliptic.Localizers.Sobolev line 90
  9. instance OAI.GlobalElliptic.Localizers.(instance at line 92) line 92
  10. def OAI.GlobalElliptic.Localizers.embed line 96
  11. lemma OAI.GlobalElliptic.Localizers.embed_injective line 100
  12. lemma OAI.GlobalElliptic.Localizers.embed_dense line 105
  13. theorem OAI.GlobalElliptic.exists_patch_localizers line 115