Mathlib Map

Theorems · Theorem · functional analysis

Convex.lipschitz_gauge

∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s → s ∈ nhds 0 → ∃ K, LipschitzWith K (gauge s)
Defined in
Mathlib.Analysis.Convex.Gauge
Cited by
1 results in Mathlib
Foundations
Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedAddCommGroupNormedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Convex.uniformContinuous_gauge · cited by 0Convex.uniformContinuous_…Set · cited by 53352SetReal · cited by 25697RealNormedSpace · cited by 12499NormedSpaceFilter · cited by 8121Filternhds · cited by 5554nhdsNNReal · cited by 4310NNRealSeminormedAddCommGroup · cited by 2671SeminormedAddCommGroupLT.lt.le · cited by 2189lt.leMetric.ball · cited by 735Metric.ballConvex · cited by 551ConvexLipschitzWith · cited by 316LipschitzWithgauge · cited by 85gaugeMetric.mem_nhds_iff · cited by 26Metric.mem_nhds_iffConvex.lipschitzWith_gauge · cited by 1Convex.lipschitzWith_gaugeConvex.lipschitz_gaugeCITED BYCITES

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Realstatement and proof · cited by 25,697
  • NormedSpacestatement and proof · cited by 12,499
  • Filterstatement · cited by 8,121
  • nhdsstatement and proof · cited by 5,554
  • NNRealstatement and proof · cited by 4,310
  • SeminormedAddCommGroupstatement and proof · cited by 2,671
  • LT.lt.leproof · cited by 2,189
  • Metric.ballproof · cited by 735
  • Convexstatement and proof · cited by 551
  • LipschitzWithstatement and proof · cited by 316
  • gaugestatement and proof · cited by 85

Cited by1

Results whose statement or proof uses this declaration.