ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>Function.Bijective ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>Function.Injective ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>Function.Surjective ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<GOAL>e x = e y ↔ x = y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x y : E<VAR>h : x ≠ y<GOAL>e x ≠ e y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>LipschitzWith 1 ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<GOAL>AntilipschitzWith 1 ⇑e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<GOAL>EMetric.diam (⇑e '' s) = EMetric.diam s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>s : Set E<GOAL>Metric.diam (⇑e '' s) = Metric.diam s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E₂<VAR>r : ℝ<GOAL>⇑e ⁻¹' Metric.ball x r = Metric.ball (e.symm x) r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E₂<VAR>r : ℝ<GOAL>⇑e ⁻¹' Metric.sphere x r = Metric.sphere (e.symm x) r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E₂<VAR>r : ℝ<GOAL>⇑e ⁻¹' Metric.closedBall x r = Metric.closedBall (e.symm x) r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>⇑e '' Metric.ball x r = Metric.ball (e x) r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>⇑e '' Metric.sphere x r = Metric.sphere (e x) r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<GOAL>⇑e '' Metric.closedBall x r = Metric.closedBall (e x) r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>α : Type u_11<VAR>TopologicalSpace α<VAR>f : α → E<VAR>s : Set α<GOAL>ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>e : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>α : Type u_11<VAR>TopologicalSpace α<VAR>f : α → E<GOAL>Continuous (⇑e ∘ f) ↔ Continuous f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E₂ : Type u_6<VAR>F : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E₂<VAR>Module R₂ E₂<VAR>NormedAddCommGroup F<VAR>Module R F<VAR>f : F →ₛₗᵢ[σ₁₂] E₂<VAR>hfr : Function.Surjective ⇑f<GOAL>⇑(LinearIsometryEquiv.ofSurjective f hfr) = ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>g : E₂ →ₛₗ[σ₂₁] E<VAR>h₁ : f.comp g = LinearMap.id<VAR>h₂ : g.comp f.toLinearMap = LinearMap.id<GOAL>⇑(LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂) = ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>f : E →ₛₗᵢ[σ₁₂] E₂<VAR>g : E₂ →ₛₗ[σ₂₁] E<VAR>h₁ : f.comp g = LinearMap.id<VAR>h₂ : g.comp f.toLinearMap = LinearMap.id<GOAL>⇑(LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂).symm = ⇑g
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>⇑(LinearIsometryEquiv.neg R) = fun x => -x
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>Module R E<GOAL>(LinearIsometryEquiv.neg R).symm = LinearIsometryEquiv.neg R
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R E₂<VAR>Module R E₃<GOAL>⇑(LinearIsometryEquiv.prodAssoc R E E₂ E₃) = ⇑(Equiv.prodAssoc E E₂ E₃)
<VAR>R : Type u_1<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>E₃ : Type u_7<VAR>Semiring R<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>SeminormedAddCommGroup E₃<VAR>Module R E<VAR>Module R E₂<VAR>Module R E₃<GOAL>⇑(LinearIsometryEquiv.prodAssoc R E E₂ E₃).symm = ⇑(Equiv.prodAssoc E E₂ E₃).symm
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R : Type u_12<VAR>Ring R<VAR>Module R E<VAR>p : Submodule R E<VAR>hp : p = ⊤<GOAL>(LinearIsometryEquiv.ofTop E p hp).toLinearEquiv = LinearEquiv.ofTop p hp
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R : Type u_12<VAR>Ring R<VAR>Module R E<VAR>p : Submodule R E<VAR>hp : p = ⊤<VAR>x : E<GOAL>↑((LinearIsometryEquiv.ofTop E p hp).symm x) = x
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R : Type u_12<VAR>Ring R<VAR>Module R E<VAR>p : Submodule R E<VAR>hp : p = ⊤<VAR>self : ↥p<GOAL>(LinearIsometryEquiv.ofTop E p hp) self = ↑self
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R' : Type u_12<VAR>Ring R'<VAR>Module R' E<VAR>p q : Submodule R' E<VAR>h : p = q<VAR>x : ↥p<GOAL>↑((LinearIsometryEquiv.ofEq p q h) x) = ↑x
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R' : Type u_12<VAR>Ring R'<VAR>Module R' E<VAR>p q : Submodule R' E<VAR>h : p = q<GOAL>(LinearIsometryEquiv.ofEq p q h).symm = LinearIsometryEquiv.ofEq q p ⋯
<VAR>E : Type u_5<VAR>SeminormedAddCommGroup E<VAR>R' : Type u_12<VAR>Ring R'<VAR>Module R' E<VAR>p : Submodule R' E<GOAL>LinearIsometryEquiv.ofEq p p ⋯ = LinearIsometryEquiv.refl R' ↥p
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>ι : Type u_11<VAR>b : Basis ι R E<VAR>f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂<VAR>h : ∀ (i : ι), f₁ (b i) = f₂ (b i)<GOAL>f₁ = f₂
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>E : Type u_5<VAR>E₂ : Type u_6<VAR>Semiring R<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup E₂<VAR>Module R E<VAR>Module R₂ E₂<VAR>ι : Type u_11<VAR>b : Basis ι R E<VAR>f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂<VAR>h : ∀ (i : ι), f₁ (b i) = f₂ (b i)<GOAL>f₁ = f₂
<VAR>E : Type u_5<VAR>F : Type u_9<VAR>SeminormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>R : Type u_11<VAR>S : Type u_12<VAR>Semiring R<VAR>Ring S<VAR>Module S E<VAR>Module R F<VAR>σ₁₂ : R →+* S<VAR>σ₂₁ : S →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>f : F →ₛₗᵢ[σ₁₂] E<VAR>a : F<GOAL>↑(f.equivRange a) = f a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>Subsingleton A<VAR>a : A<GOAL>spectralRadius 𝕜 a = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<GOAL>spectralRadius 𝕜 0 = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>a : A<VAR>k : 𝕜<VAR>h : spectralRadius 𝕜 a < ↑‖k‖₊<GOAL>k ∈ resolventSet 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>IsOpen (resolventSet 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>IsClosed (spectrum 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ * ‖1‖ < ‖k‖<GOAL>k ∈ resolventSet 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>NormOneClass A<VAR>a : A<VAR>k : 𝕜<VAR>h : ‖a‖ < ‖k‖<GOAL>k ∈ resolventSet 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ spectrum 𝕜 a<GOAL>‖k‖ ≤ ‖a‖ * ‖1‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>NormOneClass A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ spectrum 𝕜 a<GOAL>‖k‖ ≤ ‖a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>spectrum 𝕜 a ⊆ Metric.closedBall 0 (‖a‖ * ‖1‖)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>NormOneClass A<VAR>a : A<GOAL>spectrum 𝕜 a ⊆ Metric.closedBall 0 ‖a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>Bornology.IsBounded (spectrum 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>ProperSpace 𝕜<VAR>a : A<GOAL>IsCompact (spectrum 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>B : Type u_3<VAR>NonUnitalNormedRing B<VAR>NormedSpace 𝕜 B<VAR>CompleteSpace B<VAR>IsScalarTower 𝕜 B B<VAR>SMulCommClass 𝕜 B B<VAR>ProperSpace 𝕜<VAR>a : B<GOAL>IsCompact (quasispectrum 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>NormOneClass A<VAR>a : A<GOAL>spectralRadius 𝕜 a ≤ ↑‖a‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>ProperSpace 𝕜<VAR>a : A<VAR>ha : (spectrum 𝕜 a).Nonempty<GOAL>∃ k ∈ spectrum 𝕜 a, ↑‖k‖₊ = spectralRadius 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>ProperSpace 𝕜<VAR>a : A<VAR>ha : (spectrum 𝕜 a).Nonempty<VAR>r : ℝ≥0<VAR>hr : ∀ k ∈ spectrum 𝕜 a, ‖k‖₊ < r<GOAL>spectralRadius 𝕜 a < ↑r
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<VAR>n : ℕ<GOAL>spectralRadius 𝕜 a ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>spectralRadius 𝕜 a ≤ Filter.liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ resolventSet 𝕜 a<GOAL>HasDerivAt (resolvent a) (-resolvent a k ^ 2) k
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>∀ᶠ (z : 𝕜) in Bornology.cobounded 𝕜, IsUnit (resolvent a z)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>resolvent a =O[Bornology.cobounded 𝕜] Inv.inv
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>Filter.Tendsto (resolvent a) (Bornology.cobounded 𝕜) (nhds 0)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<GOAL>HasFPowerSeriesOnBall (fun z => Ring.inverse (1 - z • a)) (fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 (↑‖a‖₊)⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>a : A<VAR>z : 𝕜<VAR>h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹<GOAL>IsUnit (1 - z • a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ↑r < (spectralRadius 𝕜 a)⁻¹<GOAL>DifferentiableOn 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r)
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>a : A<GOAL>Filter.limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop ≤ spectralRadius ℂ a
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>a : A<GOAL>Filter.Tendsto (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ a))
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>a : A<GOAL>Filter.Tendsto (fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) Filter.atTop (nhds (spectralRadius ℂ a))
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>Nontrivial A<VAR>a : A<GOAL>(spectrum ℂ a).Nonempty
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>Nontrivial A<VAR>a : A<GOAL>∃ z ∈ spectrum ℂ a, ↑‖z‖₊ = spectralRadius ℂ a
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>Nontrivial A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ∀ z ∈ spectrum ℂ a, ‖z‖₊ < r<GOAL>spectralRadius ℂ a < ↑r
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>Nontrivial A<VAR>a : A<VAR>p : Polynomial ℂ<GOAL>spectrum ℂ ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum ℂ a
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>Nontrivial A<VAR>a : A<VAR>n : ℕ<GOAL>spectrum ℂ (a ^ n) = (fun x => x ^ n) '' spectrum ℂ a
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0<VAR>a : A<VAR>z : ℂ<VAR>h : z ∈ spectrum ℂ a<GOAL>(algebraMap ℂ A) z = a
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0<VAR>CompleteSpace A<VAR>a : ℂ<GOAL>(NormedRing.algEquivComplexOfComplete hA) a = (algebraMap ℂ A) a
<VAR>A : Type u_2<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0<VAR>CompleteSpace A<VAR>a : A<GOAL>(NormedRing.algEquivComplexOfComplete hA).symm a = ⋯.some
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<GOAL>NormedSpace.exp 𝕜 z ∈ spectrum 𝕜 (NormedSpace.exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>φ : A →ₐ[𝕜] 𝕜<GOAL>⇑φ.toContinuousLinearMap = ⇑φ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>F : Type u_3<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>FunLike F A 𝕜<VAR>AlgHomClass F 𝕜 A 𝕜<VAR>f : F<VAR>a : A<GOAL>‖f a‖ ≤ ‖a‖ * ‖1‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>F : Type u_3<VAR>NormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>NormOneClass A<VAR>FunLike F A 𝕜<VAR>AlgHomClass F 𝕜 A 𝕜<VAR>f : F<VAR>a : A<GOAL>‖f a‖ ≤ ‖a‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>NormOneClass A<VAR>φ : A →ₐ[𝕜] 𝕜<GOAL>‖φ.toContinuousLinearMap‖ = 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>CompleteSpace A<VAR>NormedAlgebra 𝕜 A<VAR>f : ↑(WeakDual.characterSpace 𝕜 A)<GOAL>⇑(WeakDual.CharacterSpace.equivAlgHom f) = ⇑f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedRing A<VAR>CompleteSpace A<VAR>NormedAlgebra 𝕜 A<VAR>f : A →ₐ[𝕜] 𝕜<GOAL>⇑(WeakDual.CharacterSpace.equivAlgHom.symm f) = ⇑f
<VAR>𝕜₁ : Type u_3<VAR>𝕜₂ : Type u_4<VAR>A : Type u_5<VAR>NormedField 𝕜₁<VAR>NormedField 𝕜₂<VAR>NormedRing A<VAR>NormedAlgebra 𝕜₁ A<VAR>NormedAlgebra 𝕜₂ A<VAR>NormedAlgebra 𝕜₁ 𝕜₂<VAR>IsScalarTower 𝕜₁ 𝕜₂ A<VAR>f : 𝕜₂ → 𝕜₁<VAR>a : A<VAR>h : SpectrumRestricts a f<GOAL>spectralRadius 𝕜₁ a = spectralRadius 𝕜₂ a
<VAR>A : Type u_3<VAR>Ring A<VAR>Algebra ℝ A<VAR>a : A<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x
<VAR>A : Type u_4<VAR>Ring A<VAR>PartialOrder A<VAR>Algebra ℝ A<VAR>NonnegSpectrumClass ℝ A<VAR>a : A<VAR>ha : 0 ≤ a<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_3<VAR>Ring A<VAR>Algebra ℂ A<VAR>a : A<GOAL>SpectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = ↑x.re
<VAR>A : Type u_3<VAR>Ring A<VAR>Algebra ℝ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ht : spectralRadius ℝ a ≤ ↑t<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
<VAR>A : Type u_4<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>(spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a
<VAR>A : Type u_4<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<VAR>ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
<VAR>A : Type u_4<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>a : A<VAR>ha : (spectrum ℝ a).Nonempty<GOAL>(spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing 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>TopologicalSpace R<VAR>TopologicalSpace S<VAR>a : A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>h_cpct : CompactSpace ↑(quasispectrum S a)<GOAL>CompactSpace ↑(quasispectrum R a)
<VAR>A : Type u_3<VAR>NonUnitalRing A<VAR>Module ℝ A<VAR>IsScalarTower ℝ A A<VAR>SMulCommClass ℝ A A<VAR>a : A<GOAL>QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ quasispectrum ℝ a, 0 ≤ x
<VAR>A : Type u_3<VAR>NonUnitalRing A<VAR>Module ℝ A<VAR>IsScalarTower ℝ A A<VAR>SMulCommClass ℝ A A<VAR>PartialOrder A<VAR>NonnegSpectrumClass ℝ A<VAR>a : A<VAR>ha : 0 ≤ a<GOAL>QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_3<VAR>NonUnitalRing A<VAR>Module ℂ A<VAR>IsScalarTower ℂ A A<VAR>SMulCommClass ℂ A A<VAR>a : A<GOAL>QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ quasispectrum ℂ a, x = ↑x.re
<VAR>A : Type u_3<VAR>Ring A<VAR>PartialOrder A<VAR>Algebra ℝ A<VAR>NonnegSpectrumClass ℝ A<VAR>a : A<VAR>x : ℝ≥0<VAR>ha : 0 ≤ a := by cfc_tac<GOAL>↑x ∈ spectrum ℝ a ↔ x ∈ spectrum ℝ≥0 a
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<VAR>x : X<GOAL>ConformalAt id x
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<VAR>c : ℝ<VAR>h : c ≠ 0<VAR>x : X<GOAL>ConformalAt (fun x' => c • x') x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>Subsingleton X<VAR>f : X → Y<VAR>x : X<GOAL>ConformalAt f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>f : X → Y<VAR>x : X<GOAL>ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>f : X → Y<VAR>x : X<VAR>h : ConformalAt f x<GOAL>DifferentiableAt ℝ f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>f g : X → Y<VAR>x : X<VAR>u : Set X<VAR>hx : x ∈ u<VAR>hu : IsOpen u<VAR>hf : ConformalAt f x<VAR>h : ∀ x ∈ u, g x = f x<GOAL>ConformalAt g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedAddCommGroup Z<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>NormedSpace ℝ Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>x : X<VAR>hg : ConformalAt g (f x)<VAR>hf : ConformalAt f x<GOAL>ConformalAt (g ∘ f) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>f : X → Y<VAR>x : X<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>hf : ConformalAt f x<GOAL>ConformalAt (c • f) x
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<GOAL>Conformal id
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<VAR>c : ℝ<VAR>h : c ≠ 0<GOAL>Conformal fun x => c • x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>f : X → Y<VAR>h : Conformal f<VAR>x : X<GOAL>ConformalAt f x