ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ RCLike.re ⟪x, x⟫_𝕜 * RCLike.re ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>‖x‖ = √(RCLike.re ⟪x, x⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>RCLike.re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>√(InnerProductSpace.Core.normSq x) = ‖x‖
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>(starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x, y⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>RCLike.im ⟪x, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y z : E<GOAL>⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y z : E<GOAL>⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.re ⟪x, y⟫_𝕜 = RCLike.re ⟪y, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.im ⟪x, y⟫_𝕜 = -RCLike.im ⟪y, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>r : 𝕜<GOAL>⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<VAR>r : ℝ<GOAL>⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>r : ℝ<GOAL>⟪↑r • x, y⟫_𝕜 = r • ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>r : 𝕜<GOAL>⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<VAR>r : ℝ<GOAL>⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>r : ℝ<GOAL>⟪x, ↑r • y⟫_𝕜 = r • ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>m y : E<GOAL>(sesqFormOfInner m) y = ⟪y, m⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>m : F<GOAL>∀ (m_1 : F), (bilinFormOfRealInner m) m_1 = ⟪m, m_1⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → E<VAR>x : E<GOAL>⟪∑ i ∈ s, f i, x⟫_𝕜 = ∑ i ∈ s, ⟪f i, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → E<VAR>x : E<GOAL>⟪x, ∑ i ∈ s, f i⟫_𝕜 = ∑ i ∈ s, ⟪x, f i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>l : ι →₀ 𝕜<VAR>v : ι → E<VAR>x : E<GOAL>⟪l.sum fun i a => a • v i, x⟫_𝕜 = l.sum fun i a => (starRingEnd 𝕜) a • ⟪v i, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>l : ι →₀ 𝕜<VAR>v : ι → E<VAR>x : E<GOAL>⟪x, l.sum fun i a => a • v i⟫_𝕜 = l.sum fun i a => a • ⟪x, v i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>α : ι → Type u_5<VAR>(i : ι) → AddZeroClass (α i)<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → α i → E<VAR>l : Π₀ (i : ι), α i<VAR>x : E<GOAL>⟪l.sum f, x⟫_𝕜 = l.sum fun i a => ⟪f i a, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>α : ι → Type u_5<VAR>(i : ι) → AddZeroClass (α i)<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → α i → E<VAR>l : Π₀ (i : ι), α i<VAR>x : E<GOAL>⟪x, l.sum f⟫_𝕜 = l.sum fun i a => ⟪x, f i a⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>⟪0, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>RCLike.re ⟪0, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>⟪x, 0⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>RCLike.re ⟪x, 0⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>0 ≤ RCLike.re ⟪x, x⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<GOAL>0 ≤ ⟪x, x⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>↑(RCLike.re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>⟪x, x⟫_𝕜 = ↑‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>RCLike.re ⟪x, x⟫_𝕜 = ‖⟪x, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>↑‖⟪x, x⟫_𝕜‖ = ⟪x, x⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<GOAL>|⟪x, x⟫_ℝ| = ⟪x, x⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>⟪x, x⟫_𝕜 = 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>⟪x, x⟫_𝕜 ≠ 0 ↔ x ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>RCLike.re ⟪x, x⟫_𝕜 ≤ 0 ↔ x = 0
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<GOAL>⟪x, x⟫_ℝ ≤ 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪-x, -y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>(starRingEnd 𝕜) ⟪x, x⟫_𝕜 = ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y z : E<GOAL>⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y z : E<GOAL>⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : E), ⟪v, x⟫_𝕜 = ⟪v, y⟫_𝕜<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : E), ⟪x, v⟫_𝕜 = ⟪y, v⟫_𝕜<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x + y, x + y⟫_𝕜 + ⟪x - y, x - y⟫_𝕜 = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ RCLike.re ⟪x, x⟫_𝕜 * RCLike.re ⟪y, y⟫_𝕜
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hz : ∀ (i : ι), v i ≠ 0<VAR>ho : Pairwise fun i j => ⟪v i, v j⟫_𝕜 = 0<GOAL>LinearIndependent 𝕜 v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>v : ι → E<GOAL>Orthonormal 𝕜 v ↔ ∀ (i j : ι), ⟪v i, v j⟫_𝕜 = if i = j then 1 else 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>DecidableEq E<VAR>s : Set E<GOAL>Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫_𝕜 = if v = w then 1 else 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι →₀ 𝕜<VAR>i : ι<GOAL>⟪v i, (Finsupp.total ι E 𝕜 v) l⟫_𝕜 = l i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι → 𝕜<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>⟪v i, ∑ i ∈ s, l i • v i⟫_𝕜 = l i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>Fintype ι<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι → 𝕜<VAR>i : ι<GOAL>⟪v i, ∑ i : ι, l i • v i⟫_𝕜 = l i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι →₀ 𝕜<VAR>i : ι<GOAL>⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = (starRingEnd 𝕜) (l i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι → 𝕜<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>⟪∑ i ∈ s, l i • v i, v i⟫_𝕜 = (starRingEnd 𝕜) (l i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>Fintype ι<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι → 𝕜<VAR>i : ι<GOAL>⟪∑ i : ι, l i • v i, v i⟫_𝕜 = (starRingEnd 𝕜) (l i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι →₀ 𝕜<GOAL>⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₁.sum fun i y => (starRingEnd 𝕜) y * l₂ i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι →₀ 𝕜<GOAL>⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₂.sum fun i y => (starRingEnd 𝕜) (l₁ i) * y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι → 𝕜<VAR>s : Finset ι<GOAL>⟪∑ i ∈ s, l₁ i • v i, ∑ i ∈ s, l₂ i • v i⟫_𝕜 = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>a : ι → ι → 𝕜<GOAL>∑ i ∈ s, ∑ j ∈ s, a i j • ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, a k k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>LinearIndependent 𝕜 v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>f : ι' → ι<VAR>hf : Function.Injective f<GOAL>Orthonormal 𝕜 (v ∘ f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Function.Injective v<GOAL>Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>Orthonormal 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>l : ι →₀ 𝕜<VAR>hl : l ∈ Finsupp.supported 𝕜 𝕜 s<GOAL>⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v w : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>hw : ∀ (i : ι), w i = v i ∨ w i = -v i<GOAL>Orthonormal 𝕜 w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>Orthonormal 𝕜 fun x => ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>η : Type u_5<VAR>s : η → Set E<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x<GOAL>Orthonormal 𝕜 fun x => ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>s : Set (Set E)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, Orthonormal 𝕜 fun x => ↑x<GOAL>Orthonormal 𝕜 fun x => ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>s : Set E<VAR>hs : Orthonormal 𝕜 Subtype.val<GOAL>∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>i : ι<GOAL>v i ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>Fintype ι<VAR>Nonempty ι<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>card_eq : Fintype.card ι = FiniteDimensional.finrank 𝕜 E<GOAL>⇑(basisOfOrthonormalOfCardEqFinrank hv card_eq) = v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>‖x‖ = √(RCLike.re ⟪x, x⟫_𝕜)
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<GOAL>‖x‖ = √⟪x, x⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>RCLike.re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<GOAL>RCLike.re ⟪x, x⟫_𝕜 = ‖x‖ ^ 2
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<GOAL>⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<GOAL>⟪x, x⟫_ℝ = ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖⟪x, y⟫_𝕜‖₊ ≤ ‖x‖₊ * ‖y‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.re ⟪x, y⟫_𝕜 ≤ ‖x‖ * ‖y‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>|⟪x, y⟫_ℝ| ≤ ‖x‖ * ‖y‖
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ ≤ ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>RCLike.im ⟪x, y⟫_𝕜 = (‖x - RCLike.I • y‖ * ‖x - RCLike.I • y‖ - ‖x + RCLike.I • y‖ * ‖x + RCLike.I • y‖) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>⟪x, y⟫_𝕜 = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - RCLike.I • y‖ ^ 2 - ↑‖x + RCLike.I • y‖ ^ 2) * RCLike.I) / 4
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>R : ℝ<GOAL>dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y
<VAR>V : Type u_4<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℂ V<VAR>T : V →ₗ[ℂ] V<VAR>x y : V<GOAL>⟪T y, x⟫_ℂ = (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ - Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) / 4
<VAR>V : Type u_4<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℂ V<VAR>T : V →ₗ[ℂ] V<VAR>x y : V<GOAL>⟪T x, y⟫_ℂ = (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ - Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ + Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) / 4
<VAR>V : Type u_4<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℂ V<VAR>T : V →ₗ[ℂ] V<GOAL>(∀ (x : V), ⟪T x, x⟫_ℂ = 0) ↔ T = 0
<VAR>V : Type u_4<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℂ V<VAR>S T : V →ₗ[ℂ] V<GOAL>(∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →ₗᵢ[𝕜] E'<VAR>x y : E<GOAL>⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>x y : E<GOAL>⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>x : E<VAR>y : E'<GOAL>⟪f x, y⟫_𝕜 = ⟪x, f.symm y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →ₗ[𝕜] E'<VAR>h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜<GOAL>⇑(f.isometryOfInner h) = ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →ₗ[𝕜] E'<VAR>h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜<GOAL>(f.isometryOfInner h).toLinearMap = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗ[𝕜] E'<VAR>h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜<GOAL>⇑(f.isometryOfInner h) = ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗ[𝕜] E'<VAR>h : ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜<GOAL>(f.isometryOfInner h).toLinearEquiv = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>F : Type u_9<VAR>FunLike F E E'<VAR>LinearMapClass F 𝕜 E E'<VAR>f : F<GOAL>(∀ (x : E), ‖f x‖ = ‖x‖) ↔ ∀ (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>v : ι → E<VAR>f : E →ₗᵢ[𝕜] E'<GOAL>Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>f : E →ₗᵢ[𝕜] E'<GOAL>Orthonormal 𝕜 (⇑f ∘ v)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>f : E ≃ₗᵢ[𝕜] E'<GOAL>Orthonormal 𝕜 (⇑f ∘ v)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>f : E ≃ₗᵢ[𝕜] E'<GOAL>Orthonormal 𝕜 ⇑(v.map f.toLinearEquiv)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →ₗ[𝕜] E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)<GOAL>⇑(f.isometryOfOrthonormal hv hf) = ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →ₗ[𝕜] E'<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)<GOAL>(f.isometryOfOrthonormal hv hf).toLinearMap = f