ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : AntitoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : AntitoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : AntitoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r < f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Monotone f<VAR>r : β<GOAL>Convex 𝕜 {x | f x ≤ r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Monotone f<VAR>r : β<GOAL>Convex 𝕜 {x | r ≤ f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Antitone f<VAR>r : β<GOAL>Convex 𝕜 {x | f x ≤ r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Antitone f<VAR>r : β<GOAL>Convex 𝕜 {x | f x < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Antitone f<VAR>r : β<GOAL>Convex 𝕜 {x | r ≤ f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>f : E → β<VAR>hf : Antitone f<VAR>r : β<GOAL>Convex 𝕜 {x | r < f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>c : 𝕜<GOAL>Convex 𝕜 (c • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>c : 𝕜<GOAL>Convex 𝕜 ((fun z => c • z) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>z : E<VAR>c : 𝕜<GOAL>Convex 𝕜 ((fun x => z + c • x) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>StrictOrderedCommSemiring 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b : E<GOAL>Convex 𝕜 (openSegment 𝕜 a b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>a : E<GOAL>Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Icc 0 1<GOAL>x + t • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Icc 0 1<GOAL>t • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>Set.MapsTo (⇑(AffineMap.lineMap x y)) (Set.Icc 0 1) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Icc 0 1<GOAL>(AffineMap.lineMap x y) t ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Set.Icc 0 1<GOAL>x + t • (y - x) ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Q : AffineSubspace 𝕜 E<GOAL>Convex 𝕜 ↑Q
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ᵃ[𝕜] F<VAR>s : Set F<VAR>hs : Convex 𝕜 s<GOAL>Convex 𝕜 (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set E<VAR>f : E →ᵃ[𝕜] F<VAR>hs : Convex 𝕜 s<GOAL>Convex 𝕜 (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<GOAL>Convex 𝕜 (-s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (s - t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>f : E → 𝕜<VAR>hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y<VAR>hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x<VAR>B : 𝕜<GOAL>Convex 𝕜 {x | f x ≤ B}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x : E<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht : 1 ≤ t<GOAL>x ∈ t • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>p q : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<GOAL>∃ z ∈ s, (p + q) • z = p • x + q • y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h_conv : Convex 𝕜 s<VAR>p q : 𝕜<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<GOAL>(p + q) • s = p • s + q • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.OrdConnected<VAR>h : IsChain (fun x x_1 => x ≤ x_1) s<GOAL>Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.OrdConnected<GOAL>Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<GOAL>Convex 𝕜 s ↔ s.OrdConnected
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>Convex 𝕜 ↑K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>StarConvex 𝕜 0 ↑K
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<GOAL>stdSimplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<GOAL>Convex 𝕜 (stdSimplex 𝕜 ι)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<VAR>Subsingleton 𝕜<GOAL>stdSimplex 𝕜 ι = Set.univ
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<VAR>IsEmpty ι<VAR>Nontrivial 𝕜<GOAL>stdSimplex 𝕜 ι = ∅
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<VAR>Unique ι<GOAL>stdSimplex 𝕜 ι = {fun x => 1}
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<GOAL>Pi.single i 1 ∈ stdSimplex 𝕜 ι
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<GOAL>(fun x => if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>OrderedSemiring 𝕜<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i j : ι<GOAL>[Pi.single i 1-[𝕜]Pi.single j 1] ⊆ stdSimplex 𝕜 ι
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<GOAL>stdSimplex 𝕜 (Fin 2) = [Pi.single 0 1-[𝕜]Pi.single 1 1]
<VAR>𝕜 : Type u_1<VAR>OrderedRing 𝕜<VAR>f : ↑(stdSimplex 𝕜 (Fin 2))<GOAL>↑((stdSimplexEquivIcc 𝕜) f) = ↑f 0
<VAR>𝕜 : Type u_1<VAR>OrderedRing 𝕜<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑((stdSimplexEquivIcc 𝕜).symm x) = ![↑x, 1 - ↑x]
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<VAR>i j : n<GOAL>‖U i j‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>U : Matrix n n 𝕜<VAR>hU : U ∈ Matrix.unitaryGroup n 𝕜<GOAL>‖U‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<GOAL>↑(Matrix.toEuclideanCLM A) = Matrix.toEuclideanLin A
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>x : n → 𝕜<GOAL>(Matrix.toEuclideanCLM A) ((WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)).symm x) = (WithLp.equiv 2 (n → 𝕜)).symm ((Matrix.toLin' A) x)
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>x : EuclideanSpace 𝕜 n<GOAL>(WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) ((Matrix.toEuclideanCLM A) x) = (Matrix.toLin' A) ((WithLp.equiv 2 (n → 𝕜)) x)
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<GOAL>‖A‖ = ‖(Matrix.toEuclideanLin ≪≫ₗ LinearMap.toContinuousLinearMap) A‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<GOAL>‖A‖₊ = ‖(Matrix.toEuclideanLin ≪≫ₗ LinearMap.toContinuousLinearMap) A‖₊
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>DecidableEq m<VAR>A : Matrix m n 𝕜<GOAL>‖Aᴴ‖ = ‖A‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>DecidableEq m<VAR>A : Matrix m n 𝕜<GOAL>‖Aᴴ‖₊ = ‖A‖₊
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<GOAL>‖Aᴴ * A‖ = ‖A‖ * ‖A‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<GOAL>‖Aᴴ * A‖₊ = ‖A‖₊ * ‖A‖₊
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<VAR>x : EuclideanSpace 𝕜 n<GOAL>‖(EuclideanSpace.equiv m 𝕜).symm (A *ᵥ x)‖ ≤ ‖A‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<VAR>x : EuclideanSpace 𝕜 n<GOAL>‖(EuclideanSpace.equiv m 𝕜).symm (A *ᵥ x)‖₊ ≤ ‖A‖₊ * ‖x‖₊
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>Fintype l<VAR>DecidableEq l<VAR>A : Matrix m n 𝕜<VAR>B : Matrix n l 𝕜<GOAL>‖A * B‖ ≤ ‖A‖ * ‖B‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>RCLike 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>Fintype l<VAR>DecidableEq l<VAR>A : Matrix m n 𝕜<VAR>B : Matrix n l 𝕜<GOAL>‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<GOAL>‖A‖ = ‖Matrix.toEuclideanCLM A‖
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<GOAL>‖A‖₊ = ‖Matrix.toEuclideanCLM A‖₊
<VAR>𝕜 : Type u_1<VAR>n : Type u_3<VAR>RCLike 𝕜<VAR>Fintype n<VAR>DecidableEq n<GOAL>CstarRing (Matrix n n 𝕜)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s t : Set E<VAR>x : E<GOAL>gaugeRescale s t x = (gauge s x / gauge t x) • x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s t : Set E<GOAL>gaugeRescale s t 0 = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s t : Set E<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>x : E<GOAL>gaugeRescale s t (c • x) = c • gaugeRescale s t x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>s : Set E<VAR>hsa : Absorbent ℝ s<VAR>hsb : Bornology.IsVonNBounded ℝ s<VAR>x : E<GOAL>gaugeRescale s s x = x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>s : Set E<VAR>hsa : Absorbent ℝ s<VAR>hsb : Bornology.IsVonNBounded ℝ s<GOAL>gaugeRescale s s = id
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>t : Set E<VAR>x : E<VAR>hx : gauge t x ≠ 0<GOAL>gauge t (gaugeRescale s t x) = gauge s x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>s : Set E<VAR>t : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : Bornology.IsVonNBounded ℝ t<VAR>x : E<GOAL>gauge t (gaugeRescale s t x) = gauge s x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s t : Set E<VAR>x : E<GOAL>gauge t (gaugeRescale s t x) ≤ gauge s x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>s t u : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : Bornology.IsVonNBounded ℝ t<VAR>x : E<GOAL>gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>h₀ : t ∈ 𝓝 0<VAR>hc : Convex ℝ t<GOAL>Set.MapsTo (gaugeRescale s t) (interior s) (interior t)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>htc : Convex ℝ t<VAR>ht₀ : 0 ∈ t<VAR>hta : Absorbent ℝ t<GOAL>Set.MapsTo (gaugeRescale s t) (closure s) (closure t)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>hs : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ht : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : Bornology.IsVonNBounded ℝ t<GOAL>Continuous (gaugeRescale s t)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>hsb : Bornology.IsVonNBounded ℝ s<VAR>htc : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : Bornology.IsVonNBounded ℝ t<GOAL>⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' interior s = interior t
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>hsc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>hsb : Bornology.IsVonNBounded ℝ s<VAR>htc : Convex ℝ t<VAR>ht₀ : t ∈ 𝓝 0<VAR>htb : Bornology.IsVonNBounded ℝ t<GOAL>⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s = closure t
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T1Space E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>hsc : Convex ℝ s<VAR>hsne : (interior s).Nonempty<VAR>hsb : Bornology.IsVonNBounded ℝ s<VAR>hst : Convex ℝ t<VAR>htne : (interior t).Nonempty<VAR>htb : Bornology.IsVonNBounded ℝ t<GOAL>∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure s = closure t ∧ ⇑e '' frontier s = frontier t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>hc : Convex ℝ s<VAR>hne : (interior s).Nonempty<VAR>hb : Bornology.IsBounded s<GOAL>∃ h, ⇑h '' interior s = Metric.ball 0 1 ∧ ⇑h '' closure s = Metric.closedBall 0 1 ∧ ⇑h '' frontier s = Metric.sphere 0 1
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>ι : Type u_8<VAR>Fintype ι<VAR>f : ι → Type u_9<VAR>(i : ι) → NormedAddCommGroup (f i)<VAR>(i : ι) → InnerProductSpace 𝕜 (f i)<VAR>x y : PiLp 2 f<GOAL>⟪x, y⟫_𝕜 = ∑ i : ι, ⟪x i, y i⟫_𝕜
<VAR>𝕜 : Type u_8<VAR>RCLike 𝕜<VAR>n : Type u_9<VAR>Fintype n<VAR>x : EuclideanSpace 𝕜 n<GOAL>‖x‖₊ = NNReal.sqrt (∑ i : n, ‖x i‖₊ ^ 2)
<VAR>𝕜 : Type u_8<VAR>RCLike 𝕜<VAR>n : Type u_9<VAR>Fintype n<VAR>x : EuclideanSpace 𝕜 n<GOAL>‖x‖ = √(∑ i : n, ‖x i‖ ^ 2)
<VAR>𝕜 : Type u_8<VAR>RCLike 𝕜<VAR>n : Type u_9<VAR>Fintype n<VAR>x y : EuclideanSpace 𝕜 n<GOAL>dist x y = √(∑ i : n, dist (x i) (y i) ^ 2)
<VAR>𝕜 : Type u_8<VAR>RCLike 𝕜<VAR>n : Type u_9<VAR>Fintype n<VAR>x y : EuclideanSpace 𝕜 n<GOAL>nndist x y = NNReal.sqrt (∑ i : n, nndist (x i) (y i) ^ 2)
<VAR>𝕜 : Type u_8<VAR>RCLike 𝕜<VAR>n : Type u_9<VAR>Fintype n<VAR>x y : EuclideanSpace 𝕜 n<GOAL>edist x y = (∑ i : n, edist (x i) (y i) ^ 2) ^ (1 / 2)
<VAR>n : Type u_8<VAR>Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>Metric.ball 0 r = {x | ∑ i : n, x i ^ 2 < r ^ 2}
<VAR>n : Type u_8<VAR>Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>Metric.closedBall 0 r = {x | ∑ i : n, x i ^ 2 ≤ r ^ 2}
<VAR>n : Type u_8<VAR>Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>Metric.sphere 0 r = {x | ∑ i : n, x i ^ 2 = r ^ 2}
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Fintype ι<GOAL>FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>n : ℕ<GOAL>FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Fintype ι<VAR>x y : EuclideanSpace 𝕜 ι<GOAL>⟪x, y⟫_𝕜 = Matrix.dotProduct (star ((WithLp.equiv 2 (ι → 𝕜)) x)) ((WithLp.equiv 2 (ι → 𝕜)) y)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Fintype ι<VAR>x y : ι → 𝕜<GOAL>⟪(WithLp.equiv 2 (ι → 𝕜)).symm x, (WithLp.equiv 2 (ι → 𝕜)).symm y⟫_𝕜 = Matrix.dotProduct (star x) y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : DirectSum.IsInternal V<VAR>hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>w : PiLp 2 fun i => ↥(V i)<GOAL>(hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i : ι, ↑(w i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>i : ι<GOAL>∀ (a : WithLp 2 (ι → 𝕜)), (EuclideanSpace.projₗ i) a = a i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>i : ι<GOAL>↑(EuclideanSpace.proj i) = EuclideanSpace.projₗ i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>i : ι<GOAL>∀ (a : WithLp 2 (ι → 𝕜)), (EuclideanSpace.proj i) a = a i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>i : ι<VAR>a : 𝕜<GOAL>(WithLp.equiv 2 ((i : ι) → (fun x => 𝕜) i)) (EuclideanSpace.single i a) = Pi.single i a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>i : ι<VAR>a : 𝕜<GOAL>(WithLp.equiv 2 (ι → 𝕜)).symm (Pi.single i a) = EuclideanSpace.single i a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>i : ι<VAR>a : 𝕜<VAR>j : ι<GOAL>EuclideanSpace.single i a j = if j = i then a else 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>i : ι<VAR>a : 𝕜<VAR>v : EuclideanSpace 𝕜 ι<GOAL>⟪EuclideanSpace.single i a, v⟫_𝕜 = (starRingEnd 𝕜) a * v i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>i : ι<VAR>a : 𝕜<VAR>v : EuclideanSpace 𝕜 ι<GOAL>⟪v, EuclideanSpace.single i a⟫_𝕜 = a * (starRingEnd ((fun x => 𝕜) i)) (v i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>i : ι<VAR>a : 𝕜<GOAL>‖EuclideanSpace.single i a‖ = ‖a‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>i : ι<VAR>a : 𝕜<GOAL>‖EuclideanSpace.single i a‖₊ = ‖a‖₊
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>i : ι<VAR>a b : 𝕜<GOAL>dist (EuclideanSpace.single i a) (EuclideanSpace.single i b) = dist a b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>i : ι<VAR>a b : 𝕜<GOAL>nndist (EuclideanSpace.single i a) (EuclideanSpace.single i b) = nndist a b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>i : ι<VAR>a b : 𝕜<GOAL>edist (EuclideanSpace.single i a) (EuclideanSpace.single i b) = edist a b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<GOAL>Orthonormal 𝕜 fun i => EuclideanSpace.single i 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>DecidableEq ι<VAR>Fintype ι<VAR>ι' : Type u_8<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>e : ι' ≃ ι<VAR>i' : ι'<VAR>v : 𝕜<GOAL>(LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) (EuclideanSpace.single i' v) = EuclideanSpace.single (e i') v
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<GOAL>Function.Injective OrthonormalBasis.repr
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι<GOAL>⇑{ repr := e } = fun i => e.symm (EuclideanSpace.single i 1)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>i : ι<GOAL>b.repr.symm (EuclideanSpace.single i 1) = b i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>i : ι<GOAL>b.repr (b i) = EuclideanSpace.single i 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>v : E<VAR>i : ι<GOAL>b.repr v i = ⟪b i, v⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<GOAL>Orthonormal 𝕜 ⇑b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<GOAL>⇑b.toBasis = ⇑b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<GOAL>b.toBasis.equivFun = b.repr.toLinearEquiv
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<VAR>i : ι<GOAL>(b.toBasis.repr x) i = b.repr x i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<GOAL>∑ i : ι, b.repr x i • b i = x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x : E<GOAL>∑ i : ι, ⟪b i, x⟫_𝕜 • b i = x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>v : EuclideanSpace 𝕜 ι<GOAL>∑ i : ι, v i • b i = b.repr.symm v
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>x y : E<GOAL>∑ i : ι, ⟪x, b i⟫_𝕜 * ⟪b i, y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>U : Submodule 𝕜 E<VAR>CompleteSpace ↥U<VAR>b : OrthonormalBasis ι 𝕜 ↥U<VAR>x : E<GOAL>(orthogonalProjection U) x = ∑ i : ι, ⟪↑(b i), x⟫_𝕜 • b i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>G : Type u_8<VAR>NormedAddCommGroup G<VAR>InnerProductSpace 𝕜 G<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>L : E ≃ₗᵢ[𝕜] G<VAR>i : ι<GOAL>(b.map L) i = L (b i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>G : Type u_8<VAR>NormedAddCommGroup G<VAR>InnerProductSpace 𝕜 G<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>L : E ≃ₗᵢ[𝕜] G<GOAL>(b.map L).toBasis = b.toBasis.map L.toLinearEquiv
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<GOAL>⇑(v.toOrthonormalBasis hv).repr = ⇑v.equivFun