𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
⊢ ∀ (v_1 : E), inner f v_1 = inner (↑B♯ v) v_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
⊢ f = ↑B♯ v
refine' ext_inner_right 𝕜 _
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = inner (↑B♯ v) w
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
⊢ ∀ (v_1 : E), inner f v_1 = inner (↑B♯ v) v_1
intro w
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = ↑(↑B v) w
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = inner (↑B♯ v) w
rw [continuousLinearMapOfBilin_apply]
no goals
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = ↑(↑B v) w
exact is_lax_milgram w