OAI/Geometry/Relativity/CKS/CompactMetricCoercivity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularGeometry.quadratic3_vector_smul line 11
  2. lemma OAI.CKSAngularGeometry.quadratic3_positive line 18
  3. lemma OAI.CKSAngularGeometry.quadratic3_continuous_euclidean line 23
  4. theorem OAI.CKSAngularGeometry.compact_positive_quadratic_lower line 28
  5. lemma OAI.CKSAngularGeometry.background_positive line 60
  6. theorem OAI.CKSAngularGeometry.compact_background_lower line 64