ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : MeasureTheory.IntegrableOn (fun z => Complex.I • (f' z) 1 - (f' z) Complex.I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) MeasureTheory.volume<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, Complex.I • (f' (↑x + ↑y * Complex.I)) 1 - (f' (↑x + ↑y * Complex.I)) Complex.I
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im), HasFDerivAt f (f' x) x<VAR>Hi : MeasureTheory.IntegrableOn (fun z => Complex.I • (f' z) 1 - (f' z) Complex.I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) MeasureTheory.volume<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, Complex.I • (f' (↑x + ↑y * Complex.I)) 1 - (f' (↑x + ↑y * Complex.I)) Complex.I
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hi : MeasureTheory.IntegrableOn (fun z => Complex.I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) Complex.I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) MeasureTheory.volume<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, Complex.I • (fderiv ℝ f (↑x + ↑y * Complex.I)) 1 - (fderiv ℝ f (↑x + ↑y * Complex.I)) Complex.I
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s, DifferentiableAt ℂ f x<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : DifferentiableOn ℂ f (Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im))<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>H : DifferentiableOn ℂ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>c : ℂ<VAR>r R : ℝ<VAR>h0 : 0 < r<VAR>hle : r ≤ R<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (Metric.closedBall c R \ Metric.ball c r)<VAR>hd : ∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>c : ℂ<VAR>r R : ℝ<VAR>h0 : 0 < r<VAR>hle : r ≤ R<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (Metric.closedBall c R \ Metric.ball c r)<VAR>hd : ∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z<GOAL>(∮ (z : ℂ) in C(c, R), f z) = ∮ (z : ℂ) in C(c, r), f z
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>y : E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (Metric.closedBall c R \ {c})<VAR>hd : ∀ z ∈ (Metric.ball c R \ {c}) \ s, DifferentiableAt ℂ f z<VAR>hy : Filter.Tendsto f (𝓝[≠] c) (𝓝 y)<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * Complex.I) • y
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>h0 : 0 < R<VAR>f : ℂ → E<VAR>c : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (Metric.closedBall c R)<VAR>hd : ∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * Complex.I) • f c
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>h0 : 0 ≤ R<VAR>f : ℂ → E<VAR>c : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (Metric.closedBall c R)<VAR>hd : ∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z<GOAL>(∮ (z : ℂ) in C(c, R), f z) = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ Metric.ball c R \ s<VAR>hc : ContinuousOn f (Metric.closedBall c R)<VAR>hd : ∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * Complex.I) • f w
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ Metric.ball c R<VAR>hc : ContinuousOn f (Metric.closedBall c R)<VAR>hd : ∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x<GOAL>((2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ Metric.ball c R<VAR>hc : ContinuousOn f (Metric.closedBall c R)<VAR>hd : ∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * Complex.I) • f w
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>h : DiffContOnCl ℂ f (Metric.ball c R)<VAR>hw : w ∈ Metric.ball c R<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * Complex.I) • f w
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>hf : DiffContOnCl ℂ f (Metric.ball c R)<VAR>hw : w ∈ Metric.ball c R<GOAL>((2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>hd : DifferentiableOn ℂ f (Metric.closedBall c R)<VAR>hw : w ∈ Metric.ball c R<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * Complex.I) • f w
<VAR>R : ℝ<VAR>c w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ Metric.ball c R<VAR>f : ℂ → ℂ<VAR>hc : ContinuousOn f (Metric.closedBall c R)<VAR>hd : ∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z<GOAL>(∮ (z : ℂ) in C(c, R), f z / (z - w)) = 2 * ↑π * Complex.I * f w
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ≥0<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (Metric.closedBall c ↑R)<VAR>hd : ∀ z ∈ Metric.ball c ↑R \ s, DifferentiableAt ℂ f z<VAR>hR : 0 < R<GOAL>HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ≥0<VAR>c : ℂ<VAR>f : ℂ → E<VAR>hf : DiffContOnCl ℂ f (Metric.ball c ↑R)<VAR>hR : 0 < R<GOAL>HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>R : ℝ≥0<VAR>c : ℂ<VAR>f : ℂ → E<VAR>hd : DifferentiableOn ℂ f (Metric.closedBall c ↑R)<VAR>hR : 0 < R<GOAL>HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>s : Set ℂ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DifferentiableOn ℂ f s<VAR>hz : s ∈ 𝓝 z<GOAL>AnalyticAt ℂ f z
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>s : Set ℂ<VAR>f : ℂ → E<VAR>hd : DifferentiableOn ℂ f s<VAR>hs : IsOpen s<GOAL>AnalyticOn ℂ f s
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>s : Set ℂ<VAR>f : ℂ → E<VAR>n : ℕ<VAR>hd : DifferentiableOn ℂ f s<VAR>hs : IsOpen s<GOAL>ContDiffOn ℂ (↑n) f s
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>hf : Differentiable ℂ f<VAR>z : ℂ<GOAL>AnalyticAt ℂ f z
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>hf : Differentiable ℂ f<VAR>n : ℕ∞<GOAL>ContDiff ℂ n f
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>h : Differentiable ℂ f<VAR>z : ℂ<VAR>R : ℝ≥0<VAR>hR : 0 < R<GOAL>HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑R) z ⊤
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>o : IsOpen s<GOAL>AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<GOAL>AnalyticOn ℂ f Set.univ ↔ Differentiable ℂ f
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<GOAL>AnalyticAt ℂ f c ↔ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
<VAR>S : SSet<VAR>self : S.KanComplex<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>σ₀ : SSet.horn n i ⟶ S<GOAL>∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.hornInclusion n i) σ
<VAR>X Y : SSet<VAR>f g : X ⟶ Y<VAR>w : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n<GOAL>f = g
<VAR>n : SimplexCategory<GOAL>SSet.standardSimplex.map (SimplexCategory.Hom.mk OrderHom.id) = 𝟙 (SSet.standardSimplex.obj n)
<VAR>m₁ m₂ : SimplexCategoryᵒᵖ<VAR>f : m₁ ⟶ m₂<VAR>n : SimplexCategory<VAR>x : (SSet.standardSimplex.obj n).obj m₁<GOAL>(SSet.standardSimplex.obj n).map f x = (SSet.standardSimplex.objEquiv n m₂).symm (f.unop ≫ (SSet.standardSimplex.objEquiv n m₁) x)
<VAR>n : ℕ<VAR>k : Fin (n + 1)<VAR>m : SimplexCategoryᵒᵖ<GOAL>SimplexCategory.Hom.toOrderHom (SSet.standardSimplex.const n k m).down = (OrderHom.const (Fin ((Opposite.unop m).len + 1))) k
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>hab : a ≤ b<GOAL>⇑(SimplexCategory.Hom.toOrderHom (SSet.standardSimplex.edge n a b hab).down) = ![a, b]
<VAR>n : ℕ<VAR>a b c : Fin (n + 1)<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>⇑(SimplexCategory.Hom.toOrderHom (SSet.standardSimplex.triangle a b c hab hbc).down) = ![a, b, c]
<VAR>n : ℕ<VAR>i k : Fin (n + 3)<VAR>m : SimplexCategoryᵒᵖ<GOAL>↑(SSet.horn.const n i k m) = SSet.standardSimplex.const (n + 2) k m
<VAR>n : ℕ<VAR>i a b : Fin (n + 1)<VAR>hab : a ≤ b<VAR>H : {i, a, b}.card ≤ n<GOAL>↑(SSet.horn.edge n i a b hab H) = SSet.standardSimplex.edge n a b hab
<VAR>n : ℕ<VAR>i a b : Fin (n + 1)<VAR>hab : a ≤ b<VAR>H : 3 ≤ n<GOAL>(↑(SSet.horn.edge₃ n i a b hab H)).down = SimplexCategory.Hom.mk { toFun := ![a, b], monotone' := ⋯ }
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last n<VAR>j : Fin n<GOAL>(↑(SSet.horn.primitiveEdge h₀ hₙ j)).down = SimplexCategory.Hom.mk { toFun := ![j.castSucc, j.succ], monotone' := ⋯ }
<VAR>n : ℕ<VAR>i : Fin (n + 4)<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last (n + 3)<VAR>k : ℕ<VAR>h : k < n + 2<GOAL>↑(SSet.horn.primitiveTriangle i h₀ hₙ k h) = SSet.standardSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯
<VAR>n : ℕ<VAR>i j : Fin (n + 2)<VAR>h : j ≠ i<GOAL>↑(SSet.horn.face i j h) = (SSet.standardSimplex.objEquiv [n + 1] (Opposite.op [n])).symm (SimplexCategory.δ j)
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>S : SSet<VAR>σ₁ σ₂ : Λ[n + 1, i] ⟶ S<VAR>h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (Opposite.op [n]) (SSet.horn.face i j h) = σ₂.app (Opposite.op [n]) (SSet.horn.face i j h)<GOAL>σ₁ = σ₂
<VAR>n : ℕ<VAR>X Y : SSet.Truncated n<VAR>f g : X ⟶ Y<VAR>w : ∀ (n_1 : (SimplexCategory.Truncated n)ᵒᵖ), f.app n_1 = g.app n_1<GOAL>f = g
<VAR>Δ : SimplexCategory<VAR>Δ' : SimplexCategoryᵒᵖ<GOAL>∀ (a : ((𝟭 (CategoryTheory.SimplicialObject (Type u))).obj (SSet.standardSimplex.obj Δ)).obj Δ'), (SSet.Augmented.standardSimplex.obj Δ).hom.app Δ' a = CategoryTheory.Limits.terminal.from (((𝟭 (CategoryTheory.SimplicialObject (Type u))).obj (SSet.standardSimplex.obj Δ)).obj Δ') a
<VAR>Δ : SimplexCategory<GOAL>(SSet.Augmented.standardSimplex.obj Δ).left = SSet.standardSimplex.obj Δ
<GOAL>∀ {X Y : SimplexCategory} (θ : X ⟶ Y) (a : ((fun Δ => { left := SSet.standardSimplex.obj Δ, right := ⊤_ Type u, hom := { app := fun Δ' => CategoryTheory.Limits.terminal.from (((𝟭 (CategoryTheory.SimplicialObject (Type u))).obj (SSet.standardSimplex.obj Δ)).obj Δ'), naturality := ⋯ } }) X).right), (SSet.Augmented.standardSimplex.map θ).right a = CategoryTheory.Limits.terminal.from ((fun Δ => { left := SSet.standardSimplex.obj Δ, right := ⊤_ Type u, hom := { app := fun Δ' => CategoryTheory.Limits.terminal.from (((𝟭 (CategoryTheory.SimplicialObject (Type u))).obj (SSet.standardSimplex.obj Δ)).obj Δ'), naturality := ⋯ } }) X).right a
<VAR>Δ : SimplexCategory<GOAL>(SSet.Augmented.standardSimplex.obj Δ).right = ⊤_ Type u
<GOAL>∀ {X Y : SimplexCategory} (θ : X ⟶ Y), (SSet.Augmented.standardSimplex.map θ).left = SSet.standardSimplex.map θ
<VAR>x y : ZFSet<VAR>h : x.IsTransitive<GOAL>y ∈ x → y ⊆ x
<VAR>z : ZFSet<GOAL>z.IsTransitive ↔ ∀ {x y : ZFSet}, x ∈ y → y ∈ z → x ∈ z
<VAR>x y : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<GOAL>(x ∩ y).IsTransitive
<VAR>x : ZFSet<VAR>h : x.IsTransitive<GOAL>(⋃₀ x).IsTransitive
<VAR>x : ZFSet<VAR>H : ∀ y ∈ x, y.IsTransitive<GOAL>(⋃₀ x).IsTransitive
<VAR>x y : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<GOAL>(x ∪ y).IsTransitive
<VAR>x : ZFSet<VAR>h : x.IsTransitive<GOAL>x.powerset.IsTransitive
<VAR>x : ZFSet<GOAL>x.IsTransitive ↔ ⋃₀ x ⊆ x
<VAR>x : ZFSet<GOAL>x.IsTransitive ↔ x ⊆ x.powerset
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.P 0 = 𝟙 K[X]
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>AlgebraicTopology.DoldKan.P (q + 1) = AlgebraicTopology.DoldKan.P q ≫ (𝟙 K[X] + AlgebraicTopology.DoldKan.Hσ q)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>(AlgebraicTopology.DoldKan.P q).f 0 = 𝟙 (K[X].X 0)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>AlgebraicTopology.DoldKan.P q + AlgebraicTopology.DoldKan.Q q = 𝟙 K[X]
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<GOAL>(AlgebraicTopology.DoldKan.P q).f n + (AlgebraicTopology.DoldKan.Q q).f n = 𝟙 (X _[n])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.Q 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>AlgebraicTopology.DoldKan.Q (q + 1) = AlgebraicTopology.DoldKan.Q q - AlgebraicTopology.DoldKan.P q ≫ AlgebraicTopology.DoldKan.Hσ q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>(AlgebraicTopology.DoldKan.Q q).f 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<GOAL>AlgebraicTopology.DoldKan.HigherFacesVanish q ((AlgebraicTopology.DoldKan.P q).f (n + 1))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ<GOAL>φ ≫ (AlgebraicTopology.DoldKan.P q).f (n + 1) = φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<GOAL>φ ≫ (AlgebraicTopology.DoldKan.P q).f (n + 1) = φ ↔ AlgebraicTopology.DoldKan.HigherFacesVanish q φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<GOAL>(AlgebraicTopology.DoldKan.P q).f n ≫ (AlgebraicTopology.DoldKan.P q).f n = (AlgebraicTopology.DoldKan.P q).f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<GOAL>(AlgebraicTopology.DoldKan.Q q).f n ≫ (AlgebraicTopology.DoldKan.Q q).f n = (AlgebraicTopology.DoldKan.Q q).f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>AlgebraicTopology.DoldKan.P q ≫ AlgebraicTopology.DoldKan.P q = AlgebraicTopology.DoldKan.P q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>AlgebraicTopology.DoldKan.Q q ≫ AlgebraicTopology.DoldKan.Q q = AlgebraicTopology.DoldKan.Q q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>q : ℕ<VAR>X : CategoryTheory.SimplicialObject C<GOAL>(AlgebraicTopology.DoldKan.natTransP q).app X = AlgebraicTopology.DoldKan.P q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>q n : ℕ<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (Opposite.op [n]) ≫ (AlgebraicTopology.DoldKan.P q).f n = (AlgebraicTopology.DoldKan.P q).f n ≫ f.app (Opposite.op [n])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>q n : ℕ<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (Opposite.op [n]) ≫ (AlgebraicTopology.DoldKan.Q q).f n = (AlgebraicTopology.DoldKan.Q q).f n ≫ f.app (Opposite.op [n])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>q : ℕ<VAR>X : CategoryTheory.SimplicialObject C<GOAL>(AlgebraicTopology.DoldKan.natTransQ q).app X = AlgebraicTopology.DoldKan.Q q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>G : C ⥤ D<VAR>G.Additive<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<GOAL>G.map ((AlgebraicTopology.DoldKan.P q).f n) = (AlgebraicTopology.DoldKan.P q).f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>G : C ⥤ D<VAR>G.Additive<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<GOAL>G.map ((AlgebraicTopology.DoldKan.Q q).f n) = (AlgebraicTopology.DoldKan.Q q).f n
<VAR>i j : ℕ<VAR>h : j + 1 = i<GOAL>AlgebraicTopology.DoldKan.c.Rel i j
<VAR>j : ℕ<GOAL>¬AlgebraicTopology.DoldKan.c.Rel 0 j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n m : ℕ<VAR>hnq : n < q<VAR>hnm : AlgebraicTopology.DoldKan.c.Rel m n<GOAL>AlgebraicTopology.DoldKan.hσ' q n m hnm = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n a m : ℕ<VAR>ha : n = a + q<VAR>hnm : AlgebraicTopology.DoldKan.c.Rel m n<GOAL>AlgebraicTopology.DoldKan.hσ' q n m hnm = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n a : ℕ<VAR>ha : n = a + q<GOAL>AlgebraicTopology.DoldKan.hσ' q n (n + 1) ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q : ℕ<GOAL>(AlgebraicTopology.DoldKan.Hσ q).f 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>q n m : ℕ<VAR>hnm : AlgebraicTopology.DoldKan.c.Rel m n<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (Opposite.op [n]) ≫ AlgebraicTopology.DoldKan.hσ' q n m hnm = AlgebraicTopology.DoldKan.hσ' q n m hnm ≫ f.app (Opposite.op [m])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>G : C ⥤ D<VAR>G.Additive<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n m : ℕ<VAR>hnm : AlgebraicTopology.DoldKan.c.Rel m n<GOAL>AlgebraicTopology.DoldKan.hσ' q n m hnm = G.map (AlgebraicTopology.DoldKan.hσ' q n m hnm)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>G : C ⥤ D<VAR>G.Additive<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<GOAL>(AlgebraicTopology.DoldKan.Hσ q).f n = G.map ((AlgebraicTopology.DoldKan.Hσ q).f n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>∀ {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y), CategoryTheory.Idempotents.DoldKan.N.map f = (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁.map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>CategoryTheory.Idempotents.DoldKan.N.obj X = (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse.obj (AlgebraicTopology.DoldKan.N₁.obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<GOAL>∀ {X_1 Y : SimplexCategoryᵒᵖ} (θ : X_1 ⟶ Y), (CategoryTheory.Idempotents.DoldKan.Γ.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>∀ {X Y : ChainComplex C ℕ} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ), (CategoryTheory.Idempotents.DoldKan.Γ.map f).app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting X).desc Δ fun A => f.f (Opposite.unop A.fst).len ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting Y).cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.IsIdempotentComplete C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(CategoryTheory.Idempotents.DoldKan.Γ.obj X).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ