case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ↑(continuousLinearMapOfBilin B)
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
no goals
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ↑(continuousLinearMapOfBilin B)
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
exact antilipschitz.isClosed_range B♯.uniformContinuous