OAI/Geometry/IsometricImmersion/Estimates/ActualQMomentPositive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Pulse.exists_actual_Q_moment_positive_lower line 11