ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>TopologicalSpace X<VAR>Z B : C<VAR>π : Z ⟶ B<VAR>CategoryTheory.Limits.HasPullback π π<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G<VAR>a : C(↑(G.obj Z), X)<VAR>ha : ⇑a ∘ ⇑(G.map (CategoryTheory.Limits.pullback.fst π π)) = ⇑a ∘ ⇑(G.map (CategoryTheory.Limits.pullback.snd π π))<GOAL>Function.FactorsThrough ⇑a ⇑(G.map π)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X : Type w'<VAR>TopologicalSpace X<VAR>(Z B : C) → (π : Z ⟶ B) → [inst : CategoryTheory.EffectiveEpi π] → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G<VAR>hq : ∀ (Z B : C) (π : Z ⟶ B) [inst : CategoryTheory.EffectiveEpi π], QuotientMap ⇑(G.map π)<GOAL>CategoryTheory.regularTopology.EqualizerCondition (ContinuousMap.yonedaPresheaf G X)
<VAR>X : TopCat<GOAL>∀ {X_1 Y : CompHausᵒᵖ} (f : X_1 ⟶ Y) (g : C(↑(compHausToTop.obj (Opposite.unop X_1)), ↑X)), X.toCondensedSet.val.map f g = g.comp f.unop
<VAR>X : TopCat<GOAL>∀ (X_1 : CompHausᵒᵖ), X.toCondensedSet.val.obj X_1 = C(↑(Opposite.unop X_1).toTop, ↑X)
<VAR>X : TopCat<GOAL>topCatToCondensedSet.obj X = X.toCondensedSet
<GOAL>∀ {X Y : TopCat} (f : X ⟶ Y) (x : CompHausᵒᵖ) (g : ((fun X => X.toCondensedSet) X).val.obj x), (topCatToCondensedSet.map f).val.app x g = ContinuousMap.comp f g
<VAR>S : SSet<VAR>self : S.Quasicategory<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>σ₀ : SSet.horn (n + 2) i ⟶ S<VAR>_h0 : 0 < i<VAR>_hn : i < Fin.last (n + 2)<GOAL>∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.hornInclusion (n + 2) i) σ
<VAR>S : SSet<VAR>S.Quasicategory<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h0 : 0 < i<VAR>hn : i < Fin.last n<VAR>σ₀ : SSet.horn n i ⟶ S<GOAL>∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.hornInclusion n i) σ
<VAR>S : SSet<VAR>filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : SSet.horn (n + 2) i ⟶ S), 0 < i → i < Fin.last (n + 2) → ∃ σ, ∀ (j : Fin (n + 3)) (h : j ≠ i), CategoryTheory.SimplicialObject.δ S j σ = σ₀.app (Opposite.op (SimplexCategory.mk (n + 1))) (SSet.horn.face i j h)<GOAL>S.Quasicategory
<VAR>x : SimplexCategory<VAR>f g : ↑x.toTopObj<GOAL>↑f = ↑g → f = g
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<VAR>g : ↑x.toTopObj<VAR>i : (CategoryTheory.forget SimplexCategory).obj y<GOAL>↑(SimplexCategory.toTopMap f g) i = ∑ j ∈ Finset.filter (fun x_1 => f x_1 = i) Finset.univ, ↑g j
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<GOAL>Continuous (SimplexCategory.toTopMap f)
<GOAL>∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.toTop.map f = { toFun := SimplexCategory.toTopMap f, continuous_toFun := ⋯ }
<VAR>x : SimplexCategory<GOAL>SimplexCategory.toTop.obj x = TopCat.of ↑x.toTopObj
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>SimplyConnectedSpace X ↔ Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : SimplyConnectedSpace X<GOAL>Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SimplyConnectedSpace X<VAR>x y : X<VAR>p₁ p₂ : Path x y<GOAL>p₁.Homotopic p₂
<VAR>Y : Type u_1<VAR>TopologicalSpace Y<GOAL>SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
<VAR>Y : Type u_1<VAR>TopologicalSpace Y<GOAL>SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
<VAR>z w : ℍ<GOAL>dist z w = 2 * Real.arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))
<VAR>z w : ℍ<GOAL>Real.sinh (dist z w / 2) = dist ↑z ↑w / (2 * √(z.im * w.im))
<VAR>z w : ℍ<GOAL>Real.cosh (dist z w / 2) = dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))
<VAR>z w : ℍ<GOAL>Real.tanh (dist z w / 2) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)
<VAR>z w : ℍ<GOAL>rexp (dist z w / 2) = (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))
<VAR>z w : ℍ<GOAL>Real.cosh (dist z w) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)
<VAR>a b c : ℍ<GOAL>Real.sinh ((dist a b + dist b c) / 2) = (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))
<VAR>z w : ℍ<GOAL>dist z w = dist w z
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist z w ≤ r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ Real.sinh (r / 2)
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist z w = r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = Real.sinh (r / 2)
<VAR>z w : ℍ<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>dist z w = r ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = Real.sinh (r / 2) ^ 2
<VAR>a b c : ℍ<GOAL>dist a c ≤ dist a b + dist b c
<VAR>z w : ℍ<GOAL>dist z w ≤ dist ↑z ↑w / √(z.im * w.im)
<VAR>z w : ℍ<GOAL>Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)
<VAR>z : ℍ<VAR>r : ℝ<GOAL>(z.center r).re = z.re
<VAR>z : ℍ<VAR>r : ℝ<GOAL>(z.center r).im = z.im * Real.cosh r
<VAR>z : ℍ<GOAL>z.center 0 = z
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist z w = r ↔ dist ↑z ↑(w.center r) = w.im * Real.sinh r
<VAR>z : ℍ<VAR>r : ℝ<GOAL>dist ↑z ↑(z.center r) = z.im * (Real.cosh r - 1)
<VAR>z w : ℍ<GOAL>dist ↑z ↑(w.center (dist z w)) = w.im * Real.sinh (dist z w)
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist z w < r ↔ dist ↑z ↑(w.center r) < w.im * Real.sinh r
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>r < dist z w ↔ w.im * Real.sinh r < dist ↑z ↑(w.center r)
<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist z w ≤ r ↔ dist ↑z ↑(w.center r) ≤ w.im * Real.sinh r
<VAR>z w : ℍ<VAR>h : z.re = w.re<GOAL>dist z w = dist (Real.log z.im) (Real.log w.im)
<VAR>z w : ℍ<GOAL>dist (Real.log z.im) (Real.log w.im) ≤ dist z w
<VAR>z w : ℍ<GOAL>z.im ≤ w.im * rexp (dist z w)
<VAR>z w : ℍ<GOAL>z.im / rexp (dist z w) ≤ w.im
<VAR>z w : ℍ<GOAL>dist ↑z ↑w ≤ w.im * (rexp (dist z w) - 1)
<VAR>z w : ℍ<GOAL>w.im * (1 - rexp (-dist z w)) ≤ dist ↑z ↑w
<VAR>z : ℍ<VAR>r : ℝ<VAR>w : ℂ<VAR>h : dist w ↑(z.center r) ≤ z.im * Real.sinh r<GOAL>0 < w.im
<VAR>z : ℍ<VAR>r : ℝ<GOAL>UpperHalfPlane.coe '' Metric.closedBall z r = Metric.closedBall (↑(z.center r)) (z.im * Real.sinh r)
<VAR>z : ℍ<VAR>r : ℝ<GOAL>UpperHalfPlane.coe '' Metric.ball z r = Metric.ball (↑(z.center r)) (z.im * Real.sinh r)
<VAR>z : ℍ<VAR>r : ℝ<GOAL>UpperHalfPlane.coe '' Metric.sphere z r = Metric.sphere (↑(z.center r)) (z.im * Real.sinh r)
<VAR>a : ℝ<GOAL>Isometry fun y => UpperHalfPlane.mk { re := a, im := rexp y } ⋯
<VAR>a : ℝ<GOAL>Isometry fun x => a +ᵥ x
<VAR>a : { x // 0 < x }<GOAL>Isometry fun x => a • x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>Du Eu Fu Gu : Type u<VAR>NormedAddCommGroup Du<VAR>NormedSpace 𝕜 Du<VAR>NormedAddCommGroup Eu<VAR>NormedSpace 𝕜 Eu<VAR>NormedAddCommGroup Fu<VAR>NormedSpace 𝕜 Fu<VAR>NormedAddCommGroup Gu<VAR>NormedSpace 𝕜 Gu<VAR>B : Eu →L[𝕜] Fu →L[𝕜] Gu<VAR>f : Du → Eu<VAR>g : Du → Fu<VAR>n : ℕ<VAR>s : Set Du<VAR>x : Du<VAR>hf : ContDiffOn 𝕜 (↑n) f s<VAR>hg : ContDiffOn 𝕜 (↑n) g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>NormedAddCommGroup D<VAR>NormedSpace 𝕜 D<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>NormedAddCommGroup D<VAR>NormedSpace 𝕜 D<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : D<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>NormedAddCommGroup D<VAR>NormedSpace 𝕜 D<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>hB : ‖B‖ ≤ 1<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>NormedAddCommGroup D<VAR>NormedSpace 𝕜 D<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : D<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>hB : ‖B‖ ≤ 1<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) 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>s : Set E<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → 𝕜'<VAR>g : E → F<VAR>N : ℕ∞<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : E<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => f y • g y) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g 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>𝕜' : Type u_2<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → 𝕜'<VAR>g : E → F<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : E<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => f y • g y) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>A : Type u_3<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>f g : E → A<VAR>N : ℕ∞<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : E<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => f y * g y) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>A : Type u_3<VAR>NormedRing A<VAR>NormedAlgebra 𝕜 A<VAR>f g : E → A<VAR>N : ℕ∞<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : E<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => f y * g y) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_2<VAR>A' : Type u_4<VAR>NormedCommRing A'<VAR>NormedAlgebra 𝕜 A'<VAR>DecidableEq ι<VAR>NormOneClass A'<VAR>u : Finset ι<VAR>f : ι → E → A'<VAR>N : ℕ∞<VAR>hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>x : E<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j ∈ u, f j x) s x‖ ≤ ∑ p ∈ u.sym n, ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_2<VAR>A' : Type u_4<VAR>NormedCommRing A'<VAR>NormedAlgebra 𝕜 A'<VAR>DecidableEq ι<VAR>NormOneClass A'<VAR>u : Finset ι<VAR>f : ι → E → A'<VAR>N : ℕ∞<VAR>hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)<VAR>x : E<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun x => ∏ j ∈ u, f j x) x‖ ≤ ∑ p ∈ u.sym n, ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Fu Gu : Type u<VAR>NormedAddCommGroup Fu<VAR>NormedSpace 𝕜 Fu<VAR>NormedAddCommGroup Gu<VAR>NormedSpace 𝕜 Gu<VAR>g : Fu → Gu<VAR>f : E → Fu<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set Fu<VAR>x : E<VAR>hg : ContDiffOn 𝕜 (↑n) g t<VAR>hf : ContDiffOn 𝕜 (↑n) f s<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : Set.MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : Set.MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>N : ℕ∞<VAR>hg : ContDiff 𝕜 N g<VAR>hf : ContDiff 𝕜 N f<VAR>hn : ↑n ≤ N<VAR>x : E<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i<GOAL>‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff 𝕜 N f<VAR>hg : ContDiff 𝕜 N g<VAR>x : E<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (f y) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff 𝕜 N f<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖
<VAR>Δ Δ' : SimplexCategory<VAR>f : Δ ⟶ Δ'<VAR>CategoryTheory.Epi f<GOAL>(SimplicialObject.Splitting.IndexSet.mk f).fst = Opposite.op Δ'
<VAR>Δ Δ' : SimplexCategory<VAR>f : Δ ⟶ Δ'<VAR>CategoryTheory.Epi f<GOAL>↑(SimplicialObject.Splitting.IndexSet.mk f).snd = f
<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>A = ⟨A.fst, ⟨A.e, ⋯⟩⟩
<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A₁ A₂ : SimplicialObject.Splitting.IndexSet Δ<VAR>h₁ : A₁.fst = A₂.fst<VAR>h₂ : A₁.e ≫ CategoryTheory.eqToHom ⋯ = A₂.e<GOAL>A₁ = A₂
<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>↑(SimplicialObject.Splitting.IndexSet.id Δ).snd = 𝟙 (Opposite.unop Δ)
<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(SimplicialObject.Splitting.IndexSet.id Δ).fst = Δ
<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>A.EqId ↔ A.fst = Δ
<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>A.EqId ↔ (Opposite.unop A.fst).len = (Opposite.unop Δ).len
<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>A.EqId ↔ (Opposite.unop Δ).len ≤ (Opposite.unop A.fst).len
<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>A.EqId ↔ CategoryTheory.Mono A.e
<VAR>Δ₁ Δ₂ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ₁<VAR>p : Δ₁ ⟶ Δ₂<VAR>CategoryTheory.Epi p.unop<GOAL>(A.epiComp p).fst = A.fst
<VAR>Δ₁ Δ₂ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ₁<VAR>p : Δ₁ ⟶ Δ₂<VAR>CategoryTheory.Epi p.unop<GOAL>↑(A.epiComp p).snd = p.unop ≫ A.e
<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<VAR>Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<GOAL>(A.pull θ).e ≫ CategoryTheory.Limits.image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>(s.cofan Δ).inj A = s.ι (Opposite.unop A.fst).len ≫ X.map A.e.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>n : ℕ<GOAL>(s.cofan (Opposite.op [n])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) = s.ι n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>f : X ⟶ Y<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>(s.cofan Δ).inj A ≫ f.app Δ = s.φ f (Opposite.unop A.fst).len ≫ Y.map A.e.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>Z : C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>f g : X.obj Δ ⟶ Z<VAR>h : ∀ (A : SimplicialObject.Splitting.IndexSet Δ), (s.cofan Δ).inj A ≫ f = (s.cofan Δ).inj A ≫ g<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>f g : X ⟶ Y<VAR>h : ∀ (n : ℕ), s.φ f n = s.φ g n<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>Z : C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>F : (A : SimplicialObject.Splitting.IndexSet Δ) → s.N (Opposite.unop A.fst).len ⟶ Z<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>(s.cofan Δ).inj A ≫ s.desc Δ F = F A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>e : X ≅ Y<GOAL>∀ (a : ℕ), (s.ofIso e).N a = s.N a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>e : X ≅ Y<VAR>n : ℕ<GOAL>(s.ofIso e).ι n = s.ι n ≫ e.hom.app (Opposite.op [n])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>e : X ≅ Y<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(s.ofIso e).isColimit' Δ = (s.isColimit Δ).ofIsoColimit (CategoryTheory.Limits.Cofan.ext (e.app Δ) ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>Δ₁ Δ₂ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ₁<VAR>p : Δ₁ ⟶ Δ₂<VAR>CategoryTheory.Epi p.unop<GOAL>(s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<GOAL>(SimplicialObject.Split.mk' s).s = s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<GOAL>(SimplicialObject.Split.mk' s).X = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ : SimplicialObject.Split C<VAR>self : S₁.Hom S₂<VAR>n : ℕ<GOAL>S₁.s.ι n ≫ self.F.app (Opposite.op [n]) = self.f n ≫ S₂.s.ι n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ : SimplicialObject.Split C<VAR>Φ₁ Φ₂ : S₁.Hom S₂<VAR>h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n<GOAL>Φ₁ = Φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ : SimplicialObject.Split C<VAR>Φ₁ Φ₂ : S₁ ⟶ S₂<VAR>h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n<GOAL>Φ₁ = Φ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ : SimplicialObject.Split C<VAR>Φ₁ Φ₂ : S₁ ⟶ S₂<VAR>h : Φ₁ = Φ₂<GOAL>Φ₁.f = Φ₂.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ : SimplicialObject.Split C<VAR>Φ₁ Φ₂ : S₁ ⟶ S₂<VAR>h : Φ₁ = Φ₂<VAR>n : ℕ<GOAL>Φ₁.f n = Φ₂.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S : SimplicialObject.Split C<GOAL>(𝟙 S).F = 𝟙 S.X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S : SimplicialObject.Split C<VAR>n : ℕ<GOAL>(𝟙 S).f n = 𝟙 (S.s.N n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ S₃ : SimplicialObject.Split C<VAR>Φ₁₂ : S₁ ⟶ S₂<VAR>Φ₂₃ : S₂ ⟶ S₃<GOAL>(Φ₁₂ ≫ Φ₂₃).F = Φ₁₂.F ≫ Φ₂₃.F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ S₃ : SimplicialObject.Split C<VAR>Φ₁₂ : S₁ ⟶ S₂<VAR>Φ₂₃ : S₂ ⟶ S₃<VAR>n : ℕ<GOAL>(Φ₁₂ ≫ Φ₂₃).f n = Φ₁₂.f n ≫ Φ₂₃.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S₁ S₂ : SimplicialObject.Split C<VAR>Φ : S₁ ⟶ S₂<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>(S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f (Opposite.unop A.fst).len ≫ (S₂.s.cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>S : SimplicialObject.Split C<GOAL>(SimplicialObject.Split.forget C).obj S = S.X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>∀ {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y), (SimplicialObject.Split.forget C).map Φ = Φ.F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<GOAL>∀ {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y), (SimplicialObject.Split.evalN C n).map Φ = Φ.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>S : SimplicialObject.Split C<GOAL>(SimplicialObject.Split.evalN C n).obj S = S.s.N n