V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective ↑(continuousLinearMapOfBilin B)
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ker (continuousLinearMapOfBilin B) = ⊥
rw [LinearMapClass.ker_eq_bot]
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)
⊢ Function.Injective ↑(continuousLinearMapOfBilin B)
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective ↑(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)
⊢ Function.Injective ↑(continuousLinearMapOfBilin B)
exact antilipschitz.injective