ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F' : Type u_6<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>s : Set E<VAR>t : Set E'<VAR>f : E → F<VAR>g : E' → F'<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g t<GOAL>ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>x : E<VAR>y : E'<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g y<GOAL>ContDiffAt 𝕜 n (Prod.map f g) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>p : E × E'<VAR>hf : ContDiffAt 𝕜 n f p.1<VAR>hg : ContDiffAt 𝕜 n g p.2<GOAL>ContDiffAt 𝕜 n (Prod.map f g) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n (Prod.map f g)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f₀ : F<GOAL>ContDiff 𝕜 n fun e => (e, f₀)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>e₀ : E<GOAL>ContDiff 𝕜 n fun f => (e₀, f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ∞<VAR>R : Type u_3<VAR>NormedRing R<VAR>NormedAlgebra 𝕜 R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>ContDiffAt 𝕜 n Ring.inverse ↑x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_4<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>CompleteSpace 𝕜'<VAR>x : 𝕜'<VAR>hx : x ≠ 0<VAR>n : ℕ∞<GOAL>ContDiffAt 𝕜 n Inv.inv x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_4<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>CompleteSpace 𝕜'<VAR>n : ℕ∞<GOAL>ContDiffOn 𝕜 n Inv.inv {0}ᶜ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>𝕜' : Type u_4<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>CompleteSpace 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hx : f x ≠ 0<GOAL>ContDiffWithinAt 𝕜 n (fun x => (f x)⁻¹) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>𝕜' : Type u_4<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>CompleteSpace 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiffOn 𝕜 n f s<VAR>h : ∀ x ∈ s, f x ≠ 0<GOAL>ContDiffOn 𝕜 n (fun x => (f x)⁻¹) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝕜' : Type u_4<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>CompleteSpace 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hx : f x ≠ 0<GOAL>ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_4<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>CompleteSpace 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>ContDiff 𝕜 n fun x => (f x)⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>CompleteSpace 𝕜<VAR>f g : E → 𝕜<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<VAR>hx : g x ≠ 0<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>CompleteSpace 𝕜<VAR>f g : E → 𝕜<VAR>n : ℕ∞<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g s<VAR>h₀ : ∀ x ∈ s, g x ≠ 0<GOAL>ContDiffOn 𝕜 n (f / g) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>CompleteSpace 𝕜<VAR>f g : E → 𝕜<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<VAR>hx : g x ≠ 0<GOAL>ContDiffAt 𝕜 n (fun x => f x / g x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>f g : E → 𝕜<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<VAR>h0 : ∀ (x : E), g x ≠ 0<GOAL>ContDiff 𝕜 n fun x => f x / g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>CompleteSpace E<VAR>e : E ≃L[𝕜] F<GOAL>ContDiffAt 𝕜 n ContinuousLinearMap.inverse ↑e
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>CompleteSpace E<VAR>f : PartialHomeomorph E F<VAR>f₀' : E ≃L[𝕜] F<VAR>a : F<VAR>ha : a ∈ f.target<VAR>hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)<VAR>hf : ContDiffAt 𝕜 n (↑f) (↑f.symm a)<GOAL>ContDiffAt 𝕜 n (↑f.symm) a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>CompleteSpace E<VAR>f : E ≃ₜ F<VAR>f₀' : E → E ≃L[𝕜] F<VAR>hf₀' : ∀ (a : E), HasFDerivAt (⇑f) (↑(f₀' a)) a<VAR>hf : ContDiff 𝕜 n ⇑f<GOAL>ContDiff 𝕜 n ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ∞<VAR>CompleteSpace 𝕜<VAR>f : PartialHomeomorph 𝕜 𝕜<VAR>f₀' a : 𝕜<VAR>h₀ : f₀' ≠ 0<VAR>ha : a ∈ f.target<VAR>hf₀' : HasDerivAt (↑f) f₀' (↑f.symm a)<VAR>hf : ContDiffAt 𝕜 n (↑f) (↑f.symm a)<GOAL>ContDiffAt 𝕜 n (↑f.symm) a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ∞<VAR>CompleteSpace 𝕜<VAR>f : 𝕜 ≃ₜ 𝕜<VAR>f' : 𝕜 → 𝕜<VAR>h₀ : ∀ (x : 𝕜), f' x ≠ 0<VAR>hf' : ∀ (x : 𝕜), HasDerivAt (⇑f) (f' x) x<VAR>hf : ContDiff 𝕜 n ⇑f<GOAL>ContDiff 𝕜 n ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>n : ℕ<GOAL>(PartialHomeomorph.restrContDiff 𝕜 f n).source = f.source ∩ {x | ContDiffAt 𝕜 (↑n) (↑f) x ∧ ContDiffAt 𝕜 (↑n) (↑f.symm) (↑f x)}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>n : ℕ<GOAL>∀ (a : E), ↑(PartialHomeomorph.restrContDiff 𝕜 f n) a = ↑f a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>n : ℕ<GOAL>(PartialHomeomorph.restrContDiff 𝕜 f n).target = f.target ∩ {y | ContDiffAt 𝕜 (↑n) (↑f.symm) y ∧ ContDiffAt 𝕜 (↑n) (↑f) (↑f.symm y)}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>n : ℕ<GOAL>∀ (a : F), ↑(PartialHomeomorph.restrContDiff 𝕜 f n).symm a = ↑f.symm a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>n : ℕ<GOAL>ContDiffOn 𝕜 (↑n) (↑f) (PartialHomeomorph.restrContDiff 𝕜 f n).source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : PartialHomeomorph E F<VAR>n : ℕ<GOAL>ContDiffOn 𝕜 (↑n) (↑f.symm) (PartialHomeomorph.restrContDiff 𝕜 f n).target
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s₂<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (↑n) (derivWithin f₂ s₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>n : ℕ<VAR>hs : IsOpen s₂<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (↑n) (deriv f₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>hs : UniqueDiffOn 𝕜 s₂<GOAL>ContDiffOn 𝕜 ⊤ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (derivWithin f₂ s₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>hs : IsOpen s₂<GOAL>ContDiffOn 𝕜 ⊤ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (deriv f₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m n : ℕ∞<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>hf : ContDiffOn 𝕜 n f₂ s₂<VAR>hs : UniqueDiffOn 𝕜 s₂<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffOn 𝕜 m (derivWithin f₂ s₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>m n : ℕ∞<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>hf : ContDiffOn 𝕜 n f₂ s₂<VAR>hs : IsOpen s₂<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffOn 𝕜 m (deriv f₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>h : ContDiffOn 𝕜 n f₂ s₂<VAR>hs : UniqueDiffOn 𝕜 s₂<VAR>hn : 1 ≤ n<GOAL>ContinuousOn (derivWithin f₂ s₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>h : ContDiffOn 𝕜 n f₂ s₂<VAR>hs : IsOpen s₂<VAR>hn : 1 ≤ n<GOAL>ContinuousOn (deriv f₂) s₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₂ : 𝕜 → F<VAR>n : ℕ<GOAL>ContDiff 𝕜 (↑(n + 1)) f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 (↑n) (deriv f₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₂ : 𝕜 → F<GOAL>ContDiff 𝕜 1 f₂ ↔ Differentiable 𝕜 f₂ ∧ Continuous (deriv f₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₂ : 𝕜 → F<GOAL>ContDiff 𝕜 ⊤ f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 ⊤ (deriv f₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f₂ : 𝕜 → F<VAR>h : ContDiff 𝕜 n f₂<VAR>hn : 1 ≤ n<GOAL>Continuous (deriv f₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f₂ : 𝕜 → F<GOAL>ContDiff 𝕜 ⊤ f₂ → ContDiff 𝕜 ⊤ (deriv^[n] f₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n k : ℕ<VAR>f₂ : 𝕜 → F<GOAL>ContDiff 𝕜 (↑(n + k)) f₂ → ContDiff 𝕜 (↑n) (deriv^[k] f₂)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>𝕜' : Type u_3<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>p' : E → FormalMultilinearSeries 𝕜' E F<VAR>h : HasFTaylorSeriesUpToOn n f p' s<GOAL>HasFTaylorSeriesUpToOn n f (fun x => FormalMultilinearSeries.restrictScalars 𝕜 (p' x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>𝕜' : Type u_3<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : ContDiffWithinAt 𝕜' n f s x<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>𝕜' : Type u_3<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : ContDiffOn 𝕜' n f s<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>𝕜' : Type u_3<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : ContDiffAt 𝕜' n f x<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>n : ℕ∞<VAR>𝕜' : Type u_3<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : ContDiff 𝕜' n f<GOAL>ContDiff 𝕜 n f
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>self : H.Preconnected<GOAL>H.coe.Preconnected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<GOAL>H.Preconnected ↔ H.coe.Preconnected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>self : H.Connected<GOAL>H.coe.Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<GOAL>H.Connected ↔ H.coe.Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<GOAL>H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>h : H.Connected<GOAL>H.Preconnected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>h : H.Connected<GOAL>H.verts.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>(G.singletonSubgraph v).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>huv : G.Adj u v<GOAL>(⊤.induce {u, v}).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H H' : G.Subgraph<VAR>hle : H ≤ H'<VAR>hv : H.verts = H'.verts<VAR>h : H.Connected<GOAL>H'.Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H H' : G.Subgraph<VAR>hle : ∀ (v w : V), H.Adj v w → H'.Adj v w<VAR>hv : H.verts = H'.verts<VAR>h : H.Connected<GOAL>H'.Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H K : G.Subgraph<VAR>hH : H.Connected<VAR>hK : K.Connected<VAR>hn : (H ⊓ K).verts.Nonempty<GOAL>(H ⊔ K).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>(SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).toSubgraph = G.subgraphOfAdj h
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>w ∈ p.toSubgraph.verts ↔ w ∈ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>u ∈ p.toSubgraph.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>v ∈ p.toSubgraph.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.toSubgraph.verts = {w | w ∈ p.support}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<VAR>e : Sym2 V<GOAL>e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.toSubgraph.edgeSet = {e | e ∈ p.edges}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>(p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.toSubgraph = p.toSubgraph
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>DecidableEq V<VAR>c : G.Walk v v<VAR>h : u ∈ c.support<GOAL>(c.rotate h).toSubgraph = c.toSubgraph
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>f : G →g G'<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.map f p).toSubgraph = SimpleGraph.Subgraph.map f p.toSubgraph
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>(p.toSubgraph.neighborSet w).Finite
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.toSubgraph ≤ ⊤.induce {v_1 | v_1 ∈ p.support}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>w : G.Walk u v<VAR>i : ℕ<VAR>hi : i < w.length<GOAL>w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v u' v' : V<VAR>w : G.Walk u v<GOAL>w.toSubgraph.Adj u' v' ↔ ∃ i, s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.toSubgraph.Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>s t : Set V<VAR>sconn : (H.induce s).Connected<VAR>tconn : (H.induce t).Connected<VAR>sintert : (s ⊓ t).Nonempty<GOAL>(H.induce (s ∪ t)).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H K : G.Subgraph<VAR>Hconn : H.Connected<VAR>Kconn : K.Connected<VAR>u v : V<VAR>uH : u ∈ H.verts<VAR>vK : v ∈ K.verts<VAR>huv : G.Adj u v<GOAL>(⊤.induce {u, v} ⊔ H ⊔ K).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<GOAL>H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<GOAL>H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set V<GOAL>(SimpleGraph.induce s G).Connected ↔ (⊤.induce s).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s t : Set V<VAR>sconn : (SimpleGraph.induce s G).Connected<VAR>tconn : (SimpleGraph.induce t G).Connected<VAR>sintert : (s ∩ t).Nonempty<GOAL>(SimpleGraph.induce (s ∪ t) G).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>huv : G.Adj u v<GOAL>(SimpleGraph.induce {u, v} G).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>h : H.Connected<GOAL>(SimpleGraph.induce H.verts G).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.induce {v_1 | v_1 ∈ p.support} G).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>s t : Set V<VAR>sconn : (SimpleGraph.induce s G).Connected<VAR>tconn : (SimpleGraph.induce t G).Connected<VAR>hv : v ∈ s<VAR>hw : w ∈ t<VAR>ha : G.Adj v w<GOAL>(SimpleGraph.induce (s ∪ t) G).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set V<VAR>u : V<VAR>hu : u ∈ s<VAR>patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (SimpleGraph.induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩<GOAL>(SimpleGraph.induce s G).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>S : Set (Set V)<VAR>Sn : S.Nonempty<VAR>Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty<VAR>Sc : ∀ {s : Set V}, s ∈ S → (SimpleGraph.induce s G).Connected<GOAL>(SimpleGraph.induce (⋃₀ S) G).Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Gpc : G.Preconnected<VAR>t : Finset V<VAR>tn : t.Nonempty<GOAL>∃ t', t ⊆ t' ∧ (SimpleGraph.induce (↑t') G).Connected
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<GOAL>(SzemerediRegularity.increment hP G ε).parts.card = SzemerediRegularity.stepBound P.parts.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<GOAL>(SzemerediRegularity.increment hP G ε).IsEquipartition
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<GOAL>P.parts.offDiag.attach.biUnion (SzemerediRegularity.distinctPairs hP G ε) ⊆ (SzemerediRegularity.increment hP G ε).parts.offDiag
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<GOAL>(↑P.parts.offDiag.attach).PairwiseDisjoint (SzemerediRegularity.distinctPairs hP G ε)
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>Nonempty α<VAR>x : { i // i ∈ P.parts.offDiag }<VAR>hε₁ : ε ≤ 1<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<GOAL>↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 + ((if G.IsUniform ε (↑x).1 (↑x).2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤ (∑ i ∈ SzemerediRegularity.distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>P : Finpartition Finset.univ<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : ℝ<VAR>Nonempty α<VAR>hP : P.IsEquipartition<VAR>hP₇ : 7 ≤ P.parts.card<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hε₀ : 0 ≤ ε<VAR>hε₁ : ε ≤ 1<GOAL>↑(P.energy G) + ε ^ 5 / 4 ≤ ↑((SzemerediRegularity.increment hP G ε).energy G)
<GOAL>NatOrdinal.toOrdinal.symm = Ordinal.toNatOrdinal
<VAR>a : NatOrdinal<GOAL>Ordinal.toNatOrdinal (NatOrdinal.toOrdinal a) = a
<VAR>a : NatOrdinal<GOAL>NatOrdinal.toOrdinal a = 0 ↔ a = 0
<VAR>a : NatOrdinal<GOAL>NatOrdinal.toOrdinal a = 1 ↔ a = 1
<VAR>a b : NatOrdinal<GOAL>NatOrdinal.toOrdinal (max a b) = max (NatOrdinal.toOrdinal a) (NatOrdinal.toOrdinal b)
<VAR>a b : NatOrdinal<GOAL>NatOrdinal.toOrdinal (min a b) = min (NatOrdinal.toOrdinal a) (NatOrdinal.toOrdinal b)
<VAR>a : NatOrdinal<GOAL>Order.succ a = Ordinal.toNatOrdinal (NatOrdinal.toOrdinal a + 1)
<VAR>p : NatOrdinal → Prop<VAR>i : NatOrdinal<GOAL>(∀ (j : NatOrdinal), (∀ k < j, p k) → p j) → p i
<GOAL>Ordinal.toNatOrdinal.symm = NatOrdinal.toOrdinal
<VAR>a : Ordinal.{u_1}<GOAL>NatOrdinal.toOrdinal (Ordinal.toNatOrdinal a) = a
<VAR>a : Ordinal.{u_1}<GOAL>Ordinal.toNatOrdinal a = 0 ↔ a = 0
<VAR>a : Ordinal.{u_1}<GOAL>Ordinal.toNatOrdinal a = 1 ↔ a = 1
<VAR>a b : Ordinal.{u_1}<GOAL>Ordinal.toNatOrdinal (max a b) = max (Ordinal.toNatOrdinal a) (Ordinal.toNatOrdinal b)
<VAR>a b : Ordinal.{u_1}<GOAL>Ordinal.toNatOrdinal (min a b) = min (Ordinal.toNatOrdinal a) (Ordinal.toNatOrdinal b)
<VAR>a b : Ordinal.{u}<GOAL>a ♯ b = max (a.blsub fun a' x => a' ♯ b) (b.blsub fun b' x => a ♯ b')
<VAR>b c : Ordinal.{u}<VAR>h : b < c<VAR>a : Ordinal.{u}<GOAL>a ♯ b < a ♯ c
<VAR>b c : Ordinal.{u}<VAR>h : b < c<VAR>a : Ordinal.{u}<GOAL>b ♯ a < c ♯ a
<VAR>b c : Ordinal.{u}<VAR>h : b ≤ c<VAR>a : Ordinal.{u}<GOAL>a ♯ b ≤ a ♯ c
<VAR>b c : Ordinal.{u}<VAR>h : b ≤ c<VAR>a : Ordinal.{u}<GOAL>b ♯ a ≤ c ♯ a
<VAR>a b : Ordinal.{u_1}<GOAL>a ♯ b = b ♯ a
<VAR>a b : Ordinal.{u}<VAR>f : (c : Ordinal.{u}) → c < a ♯ b → Ordinal.{max u v}<VAR>hf : ∀ {i j : Ordinal.{u}} (hi : i < a ♯ b) (hj : j < a ♯ b), i ≤ j → f i hi ≤ f j hj<GOAL>(a ♯ b).blsub f = max (a.blsub fun a' ha' => f (a' ♯ b) ⋯) (b.blsub fun b' hb' => f (a ♯ b') ⋯)
<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b ♯ c = a ♯ (b ♯ c)
<VAR>a : Ordinal.{u}<GOAL>a ♯ 0 = a
<VAR>a : Ordinal.{u}<GOAL>0 ♯ a = a
<VAR>a : Ordinal.{u}<GOAL>a ♯ 1 = Order.succ a
<VAR>a : Ordinal.{u}<GOAL>1 ♯ a = Order.succ a
<VAR>a b : Ordinal.{u}<GOAL>a ♯ Order.succ b = Order.succ (a ♯ b)
<VAR>a b : Ordinal.{u}<GOAL>Order.succ a ♯ b = Order.succ (a ♯ b)
<VAR>a : Ordinal.{u}<VAR>n : ℕ<GOAL>a ♯ ↑n = a + ↑n