OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/DetectorBumpMass.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A height-one injection has mass at most the area of its support square.
- theorem
OAI.ForcedComputation.VelocityDetector.detectorBump_massline 11