Theorems · Theorem · functional analysis

IsCoercive.antilipschitz

∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ},
  IsCoercive B → ∃ C, 0 < C ∧ AntilipschitzWith C ⇑(InnerProductSpace.continuousLinearMapOfBilin B)

Defined in

Mathlib.Analysis.InnerProductSpace.LaxMilgram

Cited by

2 results in Mathlib

Foundations

Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace