OAI/Geometry/WeakHessian/Sobolev/AddConst.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.add_const line 54
2. lemma OAI.WeakHessian.IsMinimalLocalWeakUpperGradient.add_const line 61
3. lemma OAI.WeakHessian.weakGradient_add_const_of_exists line 68
4. lemma OAI.WeakHessian.LocalSobolev.add_const line 74
5. lemma OAI.WeakHessian.Sobolev.add_const line 83
6. lemma OAI.WeakHessian.Sobolev.normalContraction line 88