Theorems · Theorem · convex and discrete geometry
ConvexOn.exists_lipschitzOnWith_of_isBounded
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {r r' : ℝ},
ConvexOn ℝ (Metric.ball x₀ r) f →
r' < r → Bornology.IsBounded (f '' Metric.ball x₀ r) → ∃ K, LipschitzOnWith K f (Metric.ball x₀ r')- Defined in
- Mathlib.Analysis.Convex.Continuous
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Set.imagestatement and proof · cited by 5,609
- NNRealstatement and proof · cited by 4,310
- LT.lt.leproof · cited by 2,189
- absproof · cited by 1,814
- Dist.distproof · cited by 1,539
- Metric.ballstatement and proof · cited by 735
- Bornology.IsBoundedstatement and proof · cited by 293
- Real.toNNRealproof · cited by 267
- ConvexOnstatement and proof · cited by 232
Cited by2
Results whose statement or proof uses this declaration.
- ConvexOn.continuousOn_tfaeproof · cited by 3
- ConcaveOn.exists_lipschitzOnWith_of_isBoundedproof · cited by 0