We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 01cceef commit 3eac587Copy full SHA for 3eac587
1 file changed
Mathlib/Analysis/Convex/Continuous.lean
@@ -223,10 +223,10 @@ protected lemma ConcaveOn.locallyLipschitz (hf : ConcaveOn ℝ univ f) : Locally
223
224
-- Commented out since `intrinsicInterior` is not imported (but should be once these are proved)
225
-- proof_wanted ConvexOn.locallyLipschitzOn_intrinsicInterior (hf : ConvexOn ℝ C f) :
226
--- ContinuousOn f (intrinsicInterior ℝ C)
+-- LocallyLipschitzOn (intrinsicInterior ℝ C) f
227
228
-- proof_wanted ConcaveOn.locallyLipschitzOn_intrinsicInterior (hf : ConcaveOn ℝ C f) :
229
230
231
-- proof_wanted ConvexOn.continuousOn_intrinsicInterior (hf : ConvexOn ℝ C f) :
232
-- ContinuousOn f (intrinsicInterior ℝ C)
0 commit comments