ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.symm = ⇑v.equivFun.symm
<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).toBasis = 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>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<GOAL>⇑(v.toOrthonormalBasis hv) = ⇑v
<VAR>η : Type u_8<VAR>Fintype η<VAR>ι : η → Type u_9<VAR>(i : η) → Fintype (ι i)<VAR>𝕜 : Type u_10<VAR>RCLike 𝕜<VAR>E : η → Type u_11<VAR>(i : η) → NormedAddCommGroup (E i)<VAR>(i : η) → InnerProductSpace 𝕜 (E i)<VAR>B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)<GOAL>(Pi.orthonormalBasis B).toBasis = (Pi.basis fun i => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm
<VAR>η : Type u_8<VAR>Fintype η<VAR>DecidableEq η<VAR>ι : η → Type u_9<VAR>(i : η) → Fintype (ι i)<VAR>𝕜 : Type u_10<VAR>RCLike 𝕜<VAR>E : η → Type u_11<VAR>(i : η) → NormedAddCommGroup (E i)<VAR>(i : η) → InnerProductSpace 𝕜 (E i)<VAR>B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)<VAR>j : (i : η) × ι i<GOAL>(Pi.orthonormalBasis B) j = (WithLp.equiv 2 ((j : η) → E j)).symm (Pi.single j.fst ((B j.fst) j.snd))
<VAR>η : Type u_8<VAR>Fintype η<VAR>ι : η → Type u_9<VAR>(i : η) → Fintype (ι i)<VAR>𝕜 : Type u_10<VAR>RCLike 𝕜<VAR>E : η → Type u_11<VAR>(i : η) → NormedAddCommGroup (E i)<VAR>(i : η) → InnerProductSpace 𝕜 (E i)<VAR>B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)<VAR>x : (i : η) → E i<VAR>j : (i : η) × ι i<GOAL>(Pi.orthonormalBasis B).repr x j = (B j.fst).repr (x j.fst) j.snd
<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 : ι → E<VAR>hon : Orthonormal 𝕜 v<VAR>hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)<GOAL>⇑(OrthonormalBasis.mk hon hsp) = v
<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>DecidableEq E<VAR>v' : ι' → E<VAR>h : Orthonormal 𝕜 v'<VAR>s : Finset ι'<VAR>i : { x // x ∈ s }<GOAL>↑((OrthonormalBasis.span h s) i) = v' ↑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>v : ι → E<VAR>hon : Orthonormal 𝕜 v<VAR>hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥<GOAL>⇑(OrthonormalBasis.mkOfOrthogonalEqBot hon hsp) = v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>Fintype ι'<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>e : ι ≃ ι'<VAR>i' : ι'<GOAL>(b.reindex e) i' = b (e.symm i')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>Fintype ι'<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).toBasis = b.toBasis.reindex e
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>Fintype ι'<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>e : ι ≃ ι'<GOAL>⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>Fintype ι'<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>e : ι ≃ ι'<VAR>x : E<VAR>i' : ι'<GOAL>(b.reindex e).repr x i' = b.repr x (e.symm i')
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<GOAL>(EuclideanSpace.basisFun ι 𝕜) i = EuclideanSpace.single i 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Fintype ι<VAR>x : EuclideanSpace 𝕜 ι<VAR>i : ι<GOAL>(EuclideanSpace.basisFun ι 𝕜).repr x i = x i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>Fintype ι<GOAL>(EuclideanSpace.basisFun ι 𝕜).toBasis = PiLp.basisFun 2 𝕜 ι
<VAR>z : ℂ<GOAL>Complex.orthonormalBasisOneI.repr z = ![z.re, z.im]
<VAR>x : EuclideanSpace ℝ (Fin 2)<GOAL>Complex.orthonormalBasisOneI.repr.symm x = ↑(x 0) + ↑(x 1) * Complex.I
<GOAL>Complex.orthonormalBasisOneI.toBasis = Complex.basisOneI
<GOAL>⇑Complex.orthonormalBasisOneI = ![1, Complex.I]
<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>NormedAddCommGroup F'<VAR>InnerProductSpace ℝ F'<VAR>v : OrthonormalBasis (Fin 2) ℝ F<VAR>f : F ≃ₗᵢ[ℝ] F'<GOAL>Complex.isometryOfOrthonormal (v.map f) = (Complex.isometryOfOrthonormal v).trans f
<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>v : OrthonormalBasis (Fin 2) ℝ F<VAR>f : F<GOAL>(Complex.isometryOfOrthonormal v).symm f = ↑((v.toBasis.coord 0) f) + ↑((v.toBasis.coord 1) f) * Complex.I
<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>v : OrthonormalBasis (Fin 2) ℝ F<VAR>z : ℂ<GOAL>(Complex.isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 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>a b : OrthonormalBasis ι 𝕜 E<GOAL>a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜
<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>a b : OrthonormalBasis ι 𝕜 E<GOAL>‖a.toBasis.det ⇑b‖ = 1
<VAR>ι : Type u_1<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>Fintype ι<VAR>DecidableEq ι<VAR>a b : OrthonormalBasis ι ℝ F<GOAL>a.toBasis.toMatrix ⇑b ∈ Matrix.orthogonalGroup ι ℝ
<VAR>ι : Type u_1<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>Fintype ι<VAR>DecidableEq ι<VAR>a b : OrthonormalBasis ι ℝ F<GOAL>a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -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>A : ι → Submodule 𝕜 E<VAR>DecidableEq ι<VAR>h : DirectSum.IsInternal A<VAR>α : ι → Type u_8<VAR>(i : ι) → Fintype (α i)<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(A i)) fun i => (A i).subtypeₗᵢ<VAR>v : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)<VAR>a : (i : ι) × α i<GOAL>(DirectSum.IsInternal.collectedOrthonormalBasis hV h v) a ∈ A a.fst
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>v : Set E<VAR>FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<GOAL>∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>Fintype ι<VAR>card_ι : FiniteDimensional.finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<GOAL>∃ w b, ⇑b = Subtype.val
<VAR>𝕜 : Type u_8<VAR>RCLike 𝕜<VAR>E : Type u_9<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<GOAL>stdOrthonormalBasis 𝕜 E = let b := Classical.choose ⋯; ⋯.mpr (b.reindex (Fintype.equivFinOfCardEq ⋯))
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>b : OrthonormalBasis ι ℝ ℝ<GOAL>(⇑b = fun x => 1) ∨ ⇑b = fun x => -1
<VAR>ι : Type u_8<VAR>𝕜 : Type u_9<VAR>RCLike 𝕜<VAR>E : Type u_10<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : DirectSum.IsInternal V<VAR>hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<GOAL>DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV' = let b := DirectSum.IsInternal.collectedOrthonormalBasis hV' hV fun i => stdOrthonormalBasis 𝕜 ↥(V i); Fintype.equivFinOfCardEq ⋯
<VAR>ι : Type u_8<VAR>𝕜 : Type u_9<VAR>RCLike 𝕜<VAR>E : Type u_10<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : DirectSum.IsInternal V<VAR>hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<GOAL>DirectSum.IsInternal.subordinateOrthonormalBasis hn hV hV' = (DirectSum.IsInternal.collectedOrthonormalBasis hV' hV fun i => stdOrthonormalBasis 𝕜 ↥(V i)).reindex (DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV')
<VAR>ι : Type u_8<VAR>𝕜 : Type u_9<VAR>RCLike 𝕜<VAR>E : Type u_10<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : DirectSum.IsInternal V<VAR>a : Fin n<VAR>hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<GOAL>DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' = ((DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV').symm a).fst
<VAR>ι : Type u_1<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>Fintype ι<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : DirectSum.IsInternal V<VAR>a : Fin n<VAR>hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<GOAL>(DirectSum.IsInternal.subordinateOrthonormalBasis hn hV hV') a ∈ V (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV')
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>V : Type u_8<VAR>NormedAddCommGroup V<VAR>InnerProductSpace 𝕜 V<VAR>FiniteDimensional 𝕜 V<VAR>S : Submodule 𝕜 V<VAR>L : ↥S →ₗᵢ[𝕜] V<VAR>s : ↥S<GOAL>L.extend ↑s = L s
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<VAR>x : n → 𝕜<GOAL>(Matrix.toEuclideanLin A) ((WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)).symm x) = (WithLp.equiv 2 (m → 𝕜)).symm ((Matrix.toLin' A) x)
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<VAR>x : EuclideanSpace 𝕜 n<GOAL>(WithLp.equiv 2 ((i : m) → (fun x => 𝕜) i)) ((Matrix.toEuclideanLin A) x) = (Matrix.toLin' A) ((WithLp.equiv 2 (n → 𝕜)) x)
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n 𝕜<VAR>v : EuclideanSpace 𝕜 n<GOAL>(Matrix.toEuclideanLin M) v = (WithLp.equiv 2 (m → 𝕜)).symm (M.mulVec ((WithLp.equiv 2 (n → 𝕜)) v))
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n 𝕜<VAR>v : EuclideanSpace 𝕜 n<GOAL>(WithLp.equiv 2 (m → 𝕜)) ((Matrix.toEuclideanLin M) v) = M.mulVec ((WithLp.equiv 2 (n → 𝕜)) v)
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n 𝕜<VAR>v : n → 𝕜<GOAL>(Matrix.toEuclideanLin M) ((WithLp.equiv 2 (n → 𝕜)).symm v) = (WithLp.equiv 2 (m → 𝕜)).symm (M.mulVec v)
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>DecidableEq n<VAR>Finite m<GOAL>Matrix.toEuclideanLin = Matrix.toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 m)
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>DecidableEq n<VAR>Fintype m<GOAL>Matrix.toEuclideanLin = Matrix.toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype n<VAR>A B : Matrix m n 𝕜<VAR>i j : m<GOAL>⟪(WithLp.equiv 2 (n → 𝕜)).symm (A i), (WithLp.equiv 2 (n → 𝕜)).symm (B j)⟫_𝕜 = (B * A.conjTranspose) j i
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>m : Type u_8<VAR>n : Type u_9<VAR>Fintype m<VAR>A B : Matrix m n 𝕜<VAR>i j : n<GOAL>⟪(WithLp.equiv 2 (m → 𝕜)).symm (A.transpose i), (WithLp.equiv 2 (m → 𝕜)).symm (B.transpose j)⟫_𝕜 = (A.conjTranspose * B) i j
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>h : StarConvex ℝ x s<VAR>hne : s.Nonempty<GOAL>ContractibleSpace ↑s
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>hne : s.Nonempty<GOAL>ContractibleSpace ↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Semifield R<VAR>Semifield S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>TopologicalSpace R<VAR>TopologicalSpace S<VAR>a : A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>h_cpct : CompactSpace ↑(spectrum S a)<GOAL>CompactSpace ↑(spectrum R a)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semifield R<VAR>StarRing R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Semifield S<VAR>StarRing S<VAR>TopologicalSpace S<VAR>TopologicalSemiring S<VAR>ContinuousStar S<VAR>Ring A<VAR>StarRing A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>a : A<VAR>φ : C(↑(spectrum S a), S) →⋆ₐ[S] A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<GOAL>∀ (a_1 : C(↑(spectrum R a), R)), (SpectrumRestricts.starAlgHom φ h) a_1 = φ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp (a_1.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Semifield S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalSemiring S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra S A<VAR>Algebra R S<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>a : A<VAR>φ : C(↑(spectrum S a), S) →⋆ₐ[S] A<VAR>hφ : ClosedEmbedding ⇑φ<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>CompactSpace ↑(spectrum S a)<GOAL>ClosedEmbedding ⇑(SpectrumRestricts.starAlgHom φ h)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Semifield S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalSemiring S<VAR>ContinuousStar S<VAR>Ring A<VAR>StarRing A<VAR>Algebra S A<VAR>Algebra R S<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>a : A<VAR>φ : C(↑(spectrum S a), S) →⋆ₐ[S] A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a<GOAL>(SpectrumRestricts.starAlgHom φ h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Semifield S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalSemiring S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra S A<VAR>ContinuousFunctionalCalculus S q<VAR>Algebra R S<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(spectrum S a)<GOAL>ContinuousFunctionalCalculus R p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Semifield S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalSemiring S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra S A<VAR>ContinuousFunctionalCalculus S q<VAR>Algebra R S<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : SpectrumRestricts a ⇑f<VAR>CompactSpace ↑(spectrum S a)<GOAL>cfcHom hpa = SpectrumRestricts.starAlgHom (cfcHom hqa) h
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Semifield S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalSemiring S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>Algebra S A<VAR>ContinuousFunctionalCalculus S q<VAR>Algebra R S<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>ContinuousFunctionalCalculus R p<VAR>UniqueContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : SpectrumRestricts a ⇑f<VAR>CompactSpace ↑(spectrum S a)<VAR>g : R → R<GOAL>cfc g a = cfc (fun x => (algebraMap R S) (g (f x))) a
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semifield R<VAR>StarRing R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Field S<VAR>StarRing S<VAR>TopologicalSpace S<VAR>TopologicalRing S<VAR>ContinuousStar S<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Algebra R S<VAR>Module R A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>a : A<VAR>φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<GOAL>∀ (a_1 : ContinuousMapZero (↑(quasispectrum R a)) R), (QuasispectrumRestricts.nonUnitalStarAlgHom φ h) a_1 = φ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp (a_1.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Field S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalRing S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Algebra R S<VAR>Module R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>a : A<VAR>φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A<VAR>hφ : ClosedEmbedding ⇑φ<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h_cpct : CompactSpace ↑(quasispectrum S a)<GOAL>ClosedEmbedding ⇑(QuasispectrumRestricts.nonUnitalStarAlgHom φ h)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Field S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalRing S<VAR>ContinuousStar S<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Algebra R S<VAR>Module R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>a : A<VAR>φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMapZero.id ⋯) = a<GOAL>(QuasispectrumRestricts.nonUnitalStarAlgHom φ h) (ContinuousMapZero.id ⋯) = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Field S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalRing S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>NonUnitalContinuousFunctionalCalculus S q<VAR>Algebra R S<VAR>Module R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(quasispectrum S a)<GOAL>NonUnitalContinuousFunctionalCalculus R p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Field S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalRing S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>NonUnitalContinuousFunctionalCalculus S q<VAR>Algebra R S<VAR>Module R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : QuasispectrumRestricts a ⇑f<VAR>CompactSpace ↑(quasispectrum S a)<GOAL>cfcₙHom hpa = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom hqa) h
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>Semifield R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>Field S<VAR>StarRing S<VAR>MetricSpace S<VAR>TopologicalRing S<VAR>ContinuousStar S<VAR>TopologicalSpace A<VAR>NonUnitalRing A<VAR>StarRing A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>NonUnitalContinuousFunctionalCalculus S q<VAR>Algebra R S<VAR>Module R A<VAR>IsScalarTower R S A<VAR>StarModule R S<VAR>ContinuousSMul R S<VAR>CompleteSpace R<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalContinuousFunctionalCalculus R p<VAR>UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : QuasispectrumRestricts a ⇑f<VAR>CompactSpace ↑(quasispectrum S a)<VAR>g : R → R<GOAL>cfcₙ g a = cfcₙ (fun x => (algebraMap R S) (g (f x))) a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>p q u v x y z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hu : u ∈ segment 𝕜 x p<VAR>hv : v ∈ segment 𝕜 y q<GOAL>¬Disjoint (segment 𝕜 u v) ((convexHull 𝕜) {p, q, z})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<GOAL>∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<GOAL>(Set.extremePoints ℝ s).Nonempty
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<GOAL>closure ((convexHull ℝ) (Set.extremePoints ℝ s)) = s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>T1Space F<VAR>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<GOAL>Set.SurjOn (⇑f) (Set.extremePoints ℝ s) (Set.extremePoints ℝ (⇑f '' s))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] = (fun p => p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x y : E<GOAL>openSegment 𝕜 x y = (fun p => p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] = [y-[𝕜]x]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x y : E<GOAL>openSegment 𝕜 x y = openSegment 𝕜 y x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>x y : E<GOAL>openSegment 𝕜 x y ⊆ [x-[𝕜]y]