ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<GOAL>DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffOn 𝕜 n f s<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>n : ℕ∞<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 n f s ↔ (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>hxs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>x : 𝕜<GOAL>iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x) fun x => 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<GOAL>iteratedDeriv n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<GOAL>iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>m : Fin n → 𝕜<GOAL>(iteratedFDeriv 𝕜 n f x) m = (∏ i : Fin n, m i) • iteratedDeriv n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>x : 𝕜<GOAL>‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<GOAL>iteratedDeriv 0 f = f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<GOAL>iteratedDeriv 1 f = deriv f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ (∀ (m : ℕ), ↑m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 (iteratedDeriv m f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>n : ℕ∞<VAR>h : ∀ (m : ℕ), ↑m ≤ n → Differentiable 𝕜 (iteratedDeriv m f)<GOAL>ContDiff 𝕜 n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiff 𝕜 n f<VAR>hmn : ↑m ≤ n<GOAL>Continuous (iteratedDeriv m f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiff 𝕜 n f<VAR>hmn : ↑m < n<GOAL>Differentiable 𝕜 (iteratedDeriv m f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<GOAL>iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<GOAL>iteratedDeriv n f = deriv^[n] f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<GOAL>iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
<VAR>p : Polynomial ℤ<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((Polynomial.aeval z) p = 0 ∧ (Polynomial.aeval z) p.mirror = 0)<GOAL>Irreducible p
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<GOAL>∀ᵐ (p : E) ∂μ, LineDifferentiableAt ℝ f p v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>hf : LipschitzWith C f<VAR>v : E<GOAL>MeasureTheory.Memℒp (fun x => lineDeriv ℝ f x v) ⊤ μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<GOAL>MeasureTheory.LocallyIntegrable (fun x => lineDeriv ℝ f x v) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f g : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : MeasureTheory.Integrable g μ<VAR>v : E<GOAL>Filter.Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f g : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>v : E<GOAL>Filter.Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<GOAL>∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<GOAL>∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : s.Countable<GOAL>∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>C : ℝ≥0<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : Metric.sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<GOAL>HasFDerivAt f L x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f : E → ℝ<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<GOAL>∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>f : E → ℝ<VAR>s : Set E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>hf : LipschitzOnWith C f s<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>C : ℝ≥0<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : E → ι → ℝ<VAR>s : Set E<VAR>hf : LipschitzOnWith C f s<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>C : ℝ≥0<VAR>s : Set E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>C : ℝ≥0<VAR>s : Set E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>C : ℝ≥0<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>f : E → F<VAR>h : LipschitzWith C f<GOAL>∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
<GOAL>LinearMap.det ↑Complex.conjLIE.toLinearEquiv = -1
<GOAL>LinearEquiv.det Complex.conjLIE.toLinearEquiv = -1
<GOAL>‖↑Complex.conjCLE‖₊ = 1
<GOAL>‖Complex.ofRealCLM‖₊ = 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>s : Set E<VAR>x : E<GOAL>UniqueDiffWithinAt 𝕜 s x ↔ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>s : Set E<VAR>x : E<VAR>self : UniqueDiffWithinAt 𝕜 s x<GOAL>x ∈ closure s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>s : Set E<VAR>x : E<VAR>self : UniqueDiffWithinAt 𝕜 s x<GOAL>Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x y : E<VAR>s : Set E<VAR>r : 𝕜<VAR>hr₀ : r ≠ 0<VAR>hr : ‖r‖ < 1<VAR>hs : ∀ᶠ (n : ℕ) in Filter.atTop, x + r ^ n • y ∈ s<GOAL>y ∈ tangentConeAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>tangentConeAt 𝕜 Set.univ x = Set.univ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>h : s ⊆ t<GOAL>tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>y : E<VAR>α : Type u_5<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>hc : Filter.Tendsto (fun n => ‖c n‖) l Filter.atTop<VAR>hd : Filter.Tendsto (fun n => c n • d n) l (𝓝 y)<GOAL>Filter.Tendsto d l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>h : 𝓝[s] x ≤ 𝓝[t] x<GOAL>tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>h : 𝓝[s] x = 𝓝[t] x<GOAL>tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>ht : t ∈ 𝓝 x<GOAL>tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>t : Set F<VAR>y : F<VAR>ht : y ∈ closure t<GOAL>⇑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : x ∈ closure s<GOAL>⇑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_5<VAR>DecidableEq ι<VAR>E : ι → Type u_6<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)<GOAL>Set.MapsTo (⇑(LinearMap.single i)) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.univ.pi s) x)
<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>s : Set G<VAR>x y : G<VAR>h : openSegment ℝ x y ⊆ s<GOAL>y - x ∈ tangentConeAt ℝ s x
<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>s : Set G<VAR>x y : G<VAR>h : segment ℝ x y ⊆ s<GOAL>y - x ∈ tangentConeAt ℝ s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>h : x ∈ s<GOAL>UniqueDiffWithinAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>UniqueDiffWithinAt 𝕜 Set.univ x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>UniqueDiffOn 𝕜 Set.univ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>UniqueDiffOn 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x y : E<VAR>s : Set E<VAR>h : UniqueDiffWithinAt 𝕜 s x<VAR>hy : x = y<GOAL>UniqueDiffWithinAt 𝕜 s y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>h : UniqueDiffWithinAt 𝕜 s x<VAR>st : 𝓝[s] x ≤ 𝓝[t] x<GOAL>UniqueDiffWithinAt 𝕜 t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>h : UniqueDiffWithinAt 𝕜 s x<VAR>st : s ⊆ t<GOAL>UniqueDiffWithinAt 𝕜 t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>st : 𝓝[s] x = 𝓝[t] x<GOAL>UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>ht : t ∈ 𝓝 x<GOAL>UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>ht : t ∈ 𝓝 x<GOAL>UniqueDiffWithinAt 𝕜 (s ∩ t) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>ht : t ∈ 𝓝[s] x<GOAL>UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s t : Set E<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>ht : t ∈ 𝓝[s] x<GOAL>UniqueDiffWithinAt 𝕜 (s ∩ t) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<GOAL>UniqueDiffWithinAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>xs : x ∈ s<GOAL>UniqueDiffWithinAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s t : Set E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>ht : IsOpen t<GOAL>UniqueDiffOn 𝕜 (s ∩ t)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>UniqueDiffOn 𝕜 s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>ht : UniqueDiffWithinAt 𝕜 t y<GOAL>UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_5<VAR>Finite ι<VAR>E : ι → Type u_6<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)<GOAL>UniqueDiffWithinAt 𝕜 (Set.univ.pi s) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_5<VAR>Finite ι<VAR>E : ι → Type u_6<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>I : Set ι<VAR>h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)<GOAL>UniqueDiffWithinAt 𝕜 (I.pi s) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>t : Set F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>ht : UniqueDiffOn 𝕜 t<GOAL>UniqueDiffOn 𝕜 (s ×ˢ t)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_5<VAR>Finite ι<VAR>E : ι → Type u_6<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>I : Set ι<VAR>h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i)<GOAL>UniqueDiffOn 𝕜 (I.pi s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_5<VAR>Finite ι<VAR>E : ι → Type u_6<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>h : ∀ (i : ι), UniqueDiffOn 𝕜 (s i)<GOAL>UniqueDiffOn 𝕜 (Set.univ.pi s)
<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>hs : (interior s).Nonempty<VAR>x : G<VAR>hx : x ∈ closure s<GOAL>UniqueDiffWithinAt ℝ s x
<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>s : Set G<VAR>conv : Convex ℝ s<VAR>hs : (interior s).Nonempty<GOAL>UniqueDiffOn ℝ s
<VAR>a : ℝ<GOAL>UniqueDiffOn ℝ (Set.Ici a)
<VAR>a : ℝ<GOAL>UniqueDiffOn ℝ (Set.Iic a)
<VAR>a : ℝ<GOAL>UniqueDiffOn ℝ (Set.Ioi a)
<VAR>a : ℝ<GOAL>UniqueDiffOn ℝ (Set.Iio a)
<VAR>a b : ℝ<VAR>hab : a < b<GOAL>UniqueDiffOn ℝ (Set.Icc a b)
<VAR>a b : ℝ<GOAL>UniqueDiffOn ℝ (Set.Ico a b)
<VAR>a b : ℝ<GOAL>UniqueDiffOn ℝ (Set.Ioc a b)
<VAR>a b : ℝ<GOAL>UniqueDiffOn ℝ (Set.Ioo a b)
<GOAL>UniqueDiffOn ℝ (Set.Icc 0 1)
<VAR>a b t : ℝ<VAR>ht : t ∈ Set.Ioo a b<GOAL>UniqueDiffWithinAt ℝ (Set.Ioo a b) t
<VAR>a : ℝ<GOAL>UniqueDiffWithinAt ℝ (Set.Ioi a) a
<VAR>a : ℝ<GOAL>UniqueDiffWithinAt ℝ (Set.Iio a) a
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<GOAL>HasGradientWithinAt f f' s x ↔ HasFDerivWithinAt f ((InnerProductSpace.toDual 𝕜 F) f') s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>frechet : F →L[𝕜] 𝕜<VAR>s : Set F<GOAL>HasFDerivWithinAt f frechet s x ↔ HasGradientWithinAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<GOAL>HasGradientAt f f' x ↔ HasFDerivAt f ((InnerProductSpace.toDual 𝕜 F) f') x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>frechet : F →L[𝕜] 𝕜<GOAL>HasFDerivAt f frechet x ↔ HasGradientAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>h : ¬DifferentiableAt 𝕜 f x<GOAL>∇ f x = 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x gradf gradg : F<VAR>hf : HasGradientAt f gradf x<VAR>hg : HasGradientAt f gradg x<GOAL>gradf = gradg
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>h : DifferentiableAt 𝕜 f x<GOAL>HasGradientAt f (∇ f x) x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>h : HasGradientAt f f' x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>s : Set F<VAR>h : DifferentiableWithinAt 𝕜 f s x<GOAL>HasGradientWithinAt f (gradientWithin f s x) s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>h : HasGradientWithinAt f f' s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<GOAL>HasGradientWithinAt f f' Set.univ x ↔ HasGradientAt f f' x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>s : Set F<VAR>h : DifferentiableOn 𝕜 f s<VAR>hs : s ∈ 𝓝 x<GOAL>HasGradientAt f (∇ f x) x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>h : HasGradientAt f f' x<GOAL>∇ f x = f'
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' : F → F<VAR>h : ∀ (x : F), HasGradientAt f (f' x) x<GOAL>∇ f = f'
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>L' : Filter 𝕜<VAR>h : HasGradientAtFilter g g' u L'<GOAL>HasDerivAtFilter g ((starRingEnd 𝕜) g') u L'
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>L' : Filter 𝕜<VAR>h : HasDerivAtFilter g g' u L'<GOAL>HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>h : HasGradientAt g g' u<GOAL>HasDerivAt g ((starRingEnd 𝕜) g') u
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>h : HasDerivAt g g' u<GOAL>HasGradientAt g ((starRingEnd 𝕜) g') u
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>g : 𝕜 → 𝕜<VAR>u : 𝕜<GOAL>∇ g u = (starRingEnd 𝕜) (deriv g u)
<VAR>g : ℝ → ℝ<VAR>g' u : ℝ<VAR>L' : Filter ℝ<VAR>h : HasGradientAtFilter g g' u L'<GOAL>HasDerivAtFilter g g' u L'
<VAR>g : ℝ → ℝ<VAR>g' u : ℝ<VAR>L' : Filter ℝ<VAR>h : HasDerivAtFilter g g' u L'<GOAL>HasGradientAtFilter g g' u L'
<VAR>g : ℝ → ℝ<VAR>g' u : ℝ<VAR>h : HasGradientAt g g' u<GOAL>HasDerivAt g g' u
<VAR>g : ℝ → ℝ<VAR>g' u : ℝ<VAR>h : HasDerivAt g g' u<GOAL>HasGradientAt g g' u
<VAR>g : ℝ → ℝ<VAR>u : ℝ<GOAL>∇ g u = deriv g u
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>L : Filter F<GOAL>HasGradientAtFilter f f' x L ↔ (fun x' => f x' - f x - ⟪f', x' - x⟫_𝕜) =o[L] fun x' => x' - x