OAI/Geometry/NodalSets/Elliptic/RealCubeCellPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Geometry.realCubeCell line 11
  2. lemma OAI.Yau.Geometry.realCubeCell_closedBall line 14
  3. lemma OAI.Yau.Geometry.realCubeCell_isCompact line 21
  4. lemma OAI.Yau.Geometry.realCubeCell_subset line 24
  5. theorem OAI.Yau.Geometry.realCubeCell_cover line 35
  6. lemma OAI.Yau.Geometry.real_closedBall_ae_ball line 45
  7. lemma OAI.Yau.Geometry.realCubeCell_pairwise_aedisjoint line 50
  8. theorem OAI.Yau.Geometry.realCubeCell_integral_sum line 58
  9. lemma OAI.Yau.Geometry.realCubeCell_mass line 67