ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<VAR>F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v<VAR>F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v<VAR>B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖<VAR>h0 : ∀ (w' : W), Integrable (F w') μ<VAR>h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ<GOAL>HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<VAR>F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v<VAR>F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v<VAR>B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖<VAR>h0 : ∀ (w' : W), Integrable (F w') μ<VAR>h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ<VAR>h3 : AEStronglyMeasurable (F' w) μ<GOAL>HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<VAR>F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v<VAR>F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v<VAR>B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖<VAR>h0 : ∀ (w' : W), Integrable (F w') μ<VAR>h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ<VAR>h3 : AEStronglyMeasurable (F' w) μ<VAR>h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v<GOAL>HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<VAR>F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v<VAR>F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v<VAR>B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖<VAR>h0 : ∀ (w' : W), Integrable (F w') μ<VAR>h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ<VAR>h3 : AEStronglyMeasurable (F' w) μ<VAR>h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v<VAR>h5 : Integrable B μ<GOAL>HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<VAR>F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v<VAR>F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v<VAR>B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖<VAR>h0 : ∀ (w' : W), Integrable (F w') μ<VAR>h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ<VAR>h3 : AEStronglyMeasurable (F' w) μ<VAR>h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v<VAR>h5 : Integrable B μ<VAR>h6 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, HasFDerivAt (fun x => F x v) (F' w' v) w'<GOAL>HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<GOAL>(emptyOn α).map f ⋯ = emptyOn β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrichotomous α r<VAR>inst✝ : IsIrrefl β s<VAR>f : α → β<VAR>hf : ∀ {x y : α}, r x y → s (f x) (f y)<VAR>x y : α<VAR>hxy : f x = f y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrichotomous α r<VAR>inst✝ : IsIrrefl β s<VAR>f : α → β<VAR>hf : ∀ {x y : α}, r x y → s (f x) (f y)<VAR>x y : α<VAR>hxy : f x = f y<VAR>h : r x y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrichotomous α r<VAR>inst✝ : IsIrrefl β s<VAR>f : α → β<VAR>hf : ∀ {x y : α}, r x y → s (f x) (f y)<VAR>x y : α<VAR>hxy : f x = f y<VAR>h : x = y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrichotomous α r<VAR>inst✝ : IsIrrefl β s<VAR>f : α → β<VAR>hf : ∀ {x y : α}, r x y → s (f x) (f y)<VAR>x y : α<VAR>hxy : f x = f y<VAR>h : r y x<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ↑r < (spectralRadius 𝕜 a)⁻¹<VAR>z : 𝕜<VAR>z_mem : z ∈ Metric.closedBall 0 ↑r<GOAL>DifferentiableWithinAt 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r) z
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ↑r < (spectralRadius 𝕜 a)⁻¹<VAR>z : 𝕜<VAR>z_mem : z ∈ Metric.closedBall 0 ↑r<GOAL>DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ↑r < (spectralRadius 𝕜 a)⁻¹<VAR>z : 𝕜<VAR>z_mem : z ∈ Metric.closedBall 0 ↑r<VAR>hu : IsUnit (1 - z • a)<GOAL>DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ↑r < (spectralRadius 𝕜 a)⁻¹<VAR>z : 𝕜<VAR>z_mem : z ∈ Metric.closedBall 0 ↑r<VAR>hu : IsUnit (1 - z • a)<VAR>H₁ : Differentiable 𝕜 fun w => 1 - w • a<GOAL>DifferentiableAt 𝕜 (fun z => Ring.inverse (1 - z • a)) z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>f : R → R<VAR>n : ℕ<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f x ^ n) a = cfc f a ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>f : R → R<VAR>n : ℕ<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>(cfcHom ha) { toFun := (spectrum R a).restrict fun x => f x ^ n, continuous_toFun := ⋯ } = (cfcHom ha) ({ toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ^ n)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅↑x_1, x⁆ ∈ H
<VAR>α : Type u_1<VAR>inst✝³ : AddGroup α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>sign (-a) = -sign a
<VAR>α : Type u_1<VAR>inst✝³ : AddGroup α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>(if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.contsAux (n + 2) = g.contsAux (n + 1)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>terminatedAt_n : g.s.get? n = none<GOAL>g.contsAux (n + 2) = g.contsAux (n + 1)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>S : StarSubalgebra R A<VAR>h : S = ⊤<VAR>x : A<GOAL>x ∈ ⊤
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>S : StarSubalgebra R A<VAR>h : ∀ (x : A), x ∈ S<VAR>x : A<GOAL>x ∈ S ↔ x ∈ ⊤
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>s : σ<VAR>a : R<GOAL>C a * X s = (monomial (Finsupp.single s 1)) a
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>hf : LinearIndependent 𝕜 f<GOAL>∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>hf : LinearIndependent 𝕜 f<VAR>val✝ : Fintype ι<GOAL>∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<GOAL>∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<GOAL>∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 (∑ i : ι, ‖f i - f i‖))<GOAL>∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<GOAL>∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹<GOAL>LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹<GOAL>LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹<GOAL>Function.Injective ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i))
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹<VAR>v u : ι → 𝕜<GOAL>dist ((⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) - ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))) v) ((⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) - ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))) u) ≤ ↑(∑ i : ι, ‖g i - f i‖₊) * dist v u
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹<VAR>v u : ι → 𝕜<GOAL>‖∑ x : ι, (v x - u x) • (g x - f x)‖ ≤ ∑ i : ι, ‖g i - f i‖ * ‖v - u‖
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹<VAR>v u : ι → 𝕜<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹<VAR>v u : ι → 𝕜<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖