ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>LinearMap.ker (orthogonalProjection K) = Kᗮ
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>HasOrthogonalProjection p<VAR>HasOrthogonalProjection (Submodule.map f.toLinearMap p)<VAR>x : E<GOAL>f ↑((orthogonalProjection p) x) = ↑((orthogonalProjection (Submodule.map f.toLinearMap p)) (f x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 E'<VAR>f : E →ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>HasOrthogonalProjection p<VAR>HasOrthogonalProjection (Submodule.map f p)<VAR>x : E<GOAL>f ↑((orthogonalProjection p) x) = ↑((orthogonalProjection (Submodule.map f p)) (f x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>HasOrthogonalProjection p<VAR>x : E'<GOAL>↑((orthogonalProjection (Submodule.map (↑f.toLinearEquiv) p)) x) = f ↑((orthogonalProjection p) (f.symm x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>orthogonalProjection ⊥ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>‖orthogonalProjection K‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : E<VAR>w : E<GOAL>↑(‖v‖ ^ 2) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : E<VAR>w : E<GOAL>↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<GOAL>↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>p : E<GOAL>(reflection K) p = 2 • ↑((orthogonalProjection K) p) - p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>(reflection K).symm = reflection K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>(reflection K)⁻¹ = reflection K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>p : E<GOAL>(reflection K) ((reflection K) p) = p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>Function.Involutive ⇑(reflection K)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>(reflection K).trans (reflection K) = LinearIsometryEquiv.refl 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>reflection K * reflection K = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>(reflection Kᗮ) v = -(reflection K) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>reflection Kᗮ = (reflection K).trans (LinearIsometryEquiv.neg 𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>u v : E<GOAL>(reflection (Submodule.span 𝕜 {u})) v = 2 • (⟪u, v⟫_𝕜 / ↑‖u‖ ^ 2) • u - v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>x : E<GOAL>(reflection K) x = x ↔ x ∈ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>x : E<VAR>hx : x ∈ K<GOAL>(reflection K) x = x
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>x : E'<GOAL>(reflection (Submodule.map (↑f.toLinearEquiv) K)) x = f ((reflection K) (f.symm x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup E'<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>reflection (Submodule.map (↑f.toLinearEquiv) K) = f.symm.trans ((reflection K).trans f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>reflection ⊥ = LinearIsometryEquiv.neg 𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K₁ K₂ : Submodule 𝕜 E<VAR>h : K₁ ≤ K₂<VAR>HasOrthogonalProjection K₁<GOAL>K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>K ⊔ Kᗮ = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<GOAL>∃ y ∈ K, ∃ z ∈ Kᗮ, v = y + z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>Kᗮᗮ = K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>CompleteSpace E<GOAL>Kᗮᗮ = K.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>IsCompl K Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K L : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>HasOrthogonalProjection L<GOAL>Kᗮ = Lᗮ ↔ K = L
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>Kᗮ = ⊥ ↔ K = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<VAR>hv : v ∈ Kᗮ<GOAL>(orthogonalProjection K) v = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>HasOrthogonalProjection U<VAR>h : U ⟂ V<GOAL>(orthogonalProjection U).comp V.subtypeL = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>HasOrthogonalProjection U<GOAL>(orthogonalProjection U).comp V.subtypeL = 0 ↔ U ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>x : E<GOAL>(orthogonalProjection K) x = (K.linearProjOfIsCompl Kᗮ ⋯) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>↑(orthogonalProjection K) = K.linearProjOfIsCompl Kᗮ ⋯
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<VAR>hv : v ∈ Kᗮ<GOAL>(reflection K) v = -v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection Kᗮ<VAR>v : E<VAR>hv : v ∈ K<GOAL>(orthogonalProjection Kᗮ) v = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>HasOrthogonalProjection U<VAR>HasOrthogonalProjection V<VAR>h : U ≤ V<VAR>x : E<GOAL>(orthogonalProjection U) ↑((orthogonalProjection V) x) = (orthogonalProjection U) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>ι : Type u_4<VAR>SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>∀ (i : ι), CompleteSpace ↥(U i)<VAR>hU : Monotone U<VAR>x : E<GOAL>Filter.Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) Filter.atTop (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>ι : Type u_4<VAR>SemilatticeSup ι<VAR>U : ι → Submodule 𝕜 E<VAR>∀ (t : ι), CompleteSpace ↥(U t)<VAR>hU : Monotone U<VAR>x : E<VAR>hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure<GOAL>Filter.Tendsto (fun t => ↑((orthogonalProjection (U t)) x)) Filter.atTop (𝓝 x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>CompleteSpace E<GOAL>Kᗮᗮᗮ = Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>CompleteSpace E<GOAL>K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>x : E<VAR>hK : Dense ↑K<VAR>h : ∀ (v : ↥K), ⟪x, ↑v⟫_𝕜 = 0<GOAL>x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>x : E<VAR>hK : Dense ↑K<VAR>h : x ∈ Kᗮ<GOAL>x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>hK : Dense ↑K<VAR>h : x - y ∈ Kᗮ<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>hK : Dense ↑K<VAR>h : ∀ (v : ↥K), ⟪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>K : Submodule 𝕜 E<VAR>x y : E<VAR>hK : Dense ↑K<VAR>h : ∀ (v : ↥K), ⟪↑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>K : Submodule 𝕜 E<VAR>x : E<VAR>hK : Dense ↑K<VAR>h : ∀ (v : ↥K), ⟪↑v, x⟫_𝕜 = 0<GOAL>x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>v : E<VAR>hv : v ∈ K<GOAL>(reflection Kᗮ) v = -v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : E<GOAL>(orthogonalProjection (Submodule.span 𝕜 {v})ᗮ) v = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : E<GOAL>(reflection (Submodule.span 𝕜 {v})ᗮ) v = -v
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>v w : F<VAR>h : ‖v‖ = ‖w‖<GOAL>(reflection (Submodule.span ℝ {v - w})ᗮ) v = w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>w : E<GOAL>↑((orthogonalProjection K) w) + ↑((orthogonalProjection Kᗮ) w) = w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>x : E<VAR>S : Submodule 𝕜 E<VAR>HasOrthogonalProjection S<GOAL>‖x‖ ^ 2 = ‖(orthogonalProjection S) x‖ ^ 2 + ‖(orthogonalProjection Sᗮ) x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>ContinuousLinearMap.id 𝕜 E = K.subtypeL.comp (orthogonalProjection K) + Kᗮ.subtypeL.comp (orthogonalProjection Kᗮ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u : ↥K<VAR>v : E<GOAL>⟪(orthogonalProjection K) v, u⟫_𝕜 = ⟪v, ↑u⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u : ↥K<VAR>v : E<GOAL>⟪u, (orthogonalProjection K) v⟫_𝕜 = ⟪↑u, v⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<VAR>u v : E<GOAL>⟪↑((orthogonalProjection K) u), v⟫_𝕜 = ⟪u, ↑((orthogonalProjection K) v)⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>HasOrthogonalProjection K<GOAL>(↑(K.subtypeL.comp (orthogonalProjection K))).IsSymmetric
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K₁ K₂ : Submodule 𝕜 E<VAR>FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<GOAL>FiniteDimensional.finrank 𝕜 ↥K₁ + FiniteDimensional.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = FiniteDimensional.finrank 𝕜 ↥K₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K₁ K₂ : Submodule 𝕜 E<VAR>FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>n : ℕ<VAR>h_dim : FiniteDimensional.finrank 𝕜 ↥K₁ + n = FiniteDimensional.finrank 𝕜 ↥K₂<GOAL>FiniteDimensional.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>FiniteDimensional.finrank 𝕜 ↥K + FiniteDimensional.finrank 𝕜 ↥Kᗮ = FiniteDimensional.finrank 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>n : ℕ<VAR>h_dim : FiniteDimensional.finrank 𝕜 ↥K + n = FiniteDimensional.finrank 𝕜 E<GOAL>FiniteDimensional.finrank 𝕜 ↥Kᗮ = n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>n : ℕ<VAR>_i : Fact (FiniteDimensional.finrank 𝕜 E = n + 1)<VAR>v : E<VAR>hv : v ≠ 0<GOAL>FiniteDimensional.finrank 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ = n
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>n : ℕ<VAR>φ : F ≃ₗᵢ[ℝ] F<VAR>hn : FiniteDimensional.finrank ℝ ↥(LinearMap.ker (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤ n<GOAL>∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>φ : F ≃ₗᵢ[ℝ] F<GOAL>∃ l, l.length ≤ FiniteDimensional.finrank ℝ F ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>FiniteDimensional ℝ F<GOAL>Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {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 : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>hc : IsComplete ↑(iSup V)<GOAL>DirectSum.IsInternal V ↔ (iSup 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>FiniteDimensional 𝕜 E<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<GOAL>DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥
<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 : ι → Submodule 𝕜 E<VAR>∀ (i : ι), CompleteSpace ↥(V i)<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>x : E<VAR>hx : x ∈ iSup V<GOAL>∑ i : ι, ↑((orthogonalProjection (V i)) x) = 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>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>x : DirectSum ι fun i => ↥(V i)<VAR>i : ι<VAR>CompleteSpace ↥(V i)<GOAL>(orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : Set E<VAR>hv : Orthonormal 𝕜 Subtype.val<GOAL>(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ (Submodule.span 𝕜 v)ᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : Set E<VAR>FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<GOAL>(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ⇑b = Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>DecidableEq E<VAR>t : Finset E<VAR>h : ¬AffineIndependent 𝕜 Subtype.val<VAR>x : E<VAR>m : x ∈ (convexHull 𝕜) ↑t<GOAL>∃ y, x ∈ (convexHull 𝕜) ↑(t.erase ↑y)
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>↑(Caratheodory.minCardFinsetOfMemConvexHull hx) ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>x ∈ (convexHull 𝕜) ↑(Caratheodory.minCardFinsetOfMemConvexHull hx)
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>(Caratheodory.minCardFinsetOfMemConvexHull hx).Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<VAR>t : Finset E<VAR>ht₁ : ↑t ⊆ s<VAR>ht₂ : x ∈ (convexHull 𝕜) ↑t<GOAL>(Caratheodory.minCardFinsetOfMemConvexHull hx).card ≤ t.card
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>AffineIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<GOAL>StrictConvex 𝕜 s ↔ s.Pairwise fun x y => openSegment 𝕜 x y ⊆ interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x y : E<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>h : x ≠ y<GOAL>openSegment 𝕜 x y ⊆ interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>StrictConvex 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>StrictConvex 𝕜 Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x y : E<VAR>a b : 𝕜<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>h : a • x + b • y ∉ interior s<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>ht : StrictConvex 𝕜 t<GOAL>StrictConvex 𝕜 (s ∩ t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>ι : Sort u_6<VAR>s : ι → Set E<VAR>hdir : Directed (fun x x_1 => x ⊆ x_1) s<VAR>hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)<GOAL>StrictConvex 𝕜 (⋃ i, s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S : Set (Set E)<VAR>hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S<VAR>hS : ∀ s ∈ S, StrictConvex 𝕜 s<GOAL>StrictConvex 𝕜 (⋃₀ S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<GOAL>Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : IsOpen s<VAR>hs : Convex 𝕜 s<GOAL>StrictConvex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : IsOpen s<GOAL>StrictConvex 𝕜 s ↔ Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>c : E<GOAL>StrictConvex 𝕜 {c}
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : s.Subsingleton<GOAL>StrictConvex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set E<VAR>Semiring 𝕝<VAR>Module 𝕝 E<VAR>Module 𝕝 F<VAR>LinearMap.CompatibleSMul E F 𝕜 𝕝<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ₗ[𝕝] F<VAR>hf : IsOpenMap ⇑f<GOAL>StrictConvex 𝕜 (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>f : E → F<VAR>h : IsLinearMap 𝕜 f<VAR>hf : IsOpenMap f<GOAL>StrictConvex 𝕜 (f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set F<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ₗ[𝕜] F<VAR>hf : Continuous ⇑f<VAR>hfinj : Function.Injective ⇑f<GOAL>StrictConvex 𝕜 (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set F<VAR>hs : StrictConvex 𝕜 s<VAR>f : E → F<VAR>h : IsLinearMap 𝕜 f<VAR>hf : Continuous f<VAR>hfinj : Function.Injective f<GOAL>StrictConvex 𝕜 (f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>s : Set β<VAR>hs : s.OrdConnected<GOAL>StrictConvex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>StrictConvex 𝕜 (Set.Iic r)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>StrictConvex 𝕜 (Set.Ici r)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>StrictConvex 𝕜 (Set.Iio r)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>StrictConvex 𝕜 (Set.Ioi r)