OAI/Geometry/CylinderCovering/Ruled/BoundaryCertificates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RuledApproximation.HyperbolicBoundaryCertificates.physical_weight_integrable line 10
2. theorem OAI.RuledApproximation.HyperbolicBoundaryCertificates.physical_weight_integral_pos_iff line 17
3. theorem OAI.RuledApproximation.HyperbolicBoundaryCertificates.physical_weight_integral_eq_zero_iff line 29
4. theorem OAI.RuledApproximation.HyperbolicBoundaryCertificates.empty_labels_zero_count line 46
5. theorem OAI.RuledApproximation.HyperbolicBoundaryCertificates.null_labels_physical_cover line 55
6. theorem OAI.RuledApproximation.HyperbolicBoundaryCertificates.strict_physical_cover line 64
7. theorem OAI.RuledApproximation.HyperbolicBoundaryCertificates.strict_physical_cover_with_residual line 80