OAI/Geometry/PrescribedPotential/CompletedRealification.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Completed Realification.

  1. def OAI.GlobalElliptic.GluingData.completedRealify line 30
  2. lemma OAI.GlobalElliptic.GluingData.completedRealify_embed line 33
  3. lemma OAI.GlobalElliptic.GluingData.completedRealify_mem line 37
  4. def OAI.GlobalElliptic.GluingData.realProjection line 46
  5. lemma OAI.GlobalElliptic.GluingData.completedRealify_of_real line 49
  6. lemma OAI.GlobalElliptic.GluingData.realProjection_of_real line 59
  7. lemma OAI.GlobalElliptic.GluingData.completedRealify_lower line 62
  8. lemma OAI.GlobalElliptic.GluingData.mem_real_of_lower line 77
  9. lemma OAI.GlobalElliptic.GluingData.mem_real_of_lower_eq line 87