OAI/Geometry/Borsuk/SphereGeometry/IntegralLift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BorsukNine.integralLift line 16
  2. lemma OAI.BorsukNine.Admissible.integrand_continuous line 21
  3. lemma OAI.BorsukNine.Admissible.integrand_integrable line 26
  4. lemma OAI.BorsukNine.Admissible.integralLift_nonneg line 32
  5. lemma OAI.BorsukNine.Admissible.integralLift_sum line 36
  6. lemma OAI.BorsukNine.Admissible.integralLift_pos_iff_sphere line 44
  7. lemma OAI.BorsukNine.Admissible.integralLift_continuous line 63
  8. lemma OAI.BorsukNine.Admissible.integralLift_pos_iff line 78
  9. lemma OAI.BorsukNine.Admissible.integralLift_support line 94
  10. lemma OAI.BorsukNine.Admissible.integralLift_orthogonal line 112
  11. lemma OAI.BorsukNine.integralLift_smul_nonneg line 126