ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<VAR>S : SimplicialObject.Split C<GOAL>(SimplicialObject.Split.natTransCofanInj C A).app S = (S.s.cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.AlternatingFaceMapComplex.objD X (n + 1) ≫ AlgebraicTopology.AlternatingFaceMapComplex.objD X n = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>(AlgebraicTopology.AlternatingFaceMapComplex.obj X).X 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<VAR>n : ℕ<GOAL>(AlgebraicTopology.AlternatingFaceMapComplex.obj X).d (n + 1) n = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<VAR>n : ℕ<GOAL>(AlgebraicTopology.AlternatingFaceMapComplex.map f).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>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>((AlgebraicTopology.alternatingFaceMapComplex C).obj X).X 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<VAR>n : ℕ<GOAL>((AlgebraicTopology.alternatingFaceMapComplex C).obj X).d (n + 1) n = AlgebraicTopology.AlternatingFaceMapComplex.objD X n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<VAR>n : ℕ<GOAL>((AlgebraicTopology.alternatingFaceMapComplex C).map f).f n = f.app (Opposite.op [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>F : C ⥤ D<VAR>F.Additive<GOAL>AlgebraicTopology.alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ) = (CategoryTheory.SimplicialObject.whiskering C D).obj F ⋙ AlgebraicTopology.alternatingFaceMapComplex D
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)<VAR>n : ℕ<GOAL>((AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f = P.p.app (Opposite.op [n + 1]) ≫ (AlgebraicTopology.AlternatingFaceMapComplex.obj P.X).d (n + 1) n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>(AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f 0 = X.hom.app (Opposite.op [0])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>n : ℕ<GOAL>(AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f (n + 1) = 0
<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<VAR>n : ℕ<GOAL>(AlgebraicTopology.inclusionOfMooreComplexMap X).f n = (AlgebraicTopology.NormalizedMooreComplex.objX X n).arrow
<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<GOAL>(AlgebraicTopology.inclusionOfMooreComplex A).app X = AlgebraicTopology.inclusionOfMooreComplexMap X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.AlternatingCofaceMapComplex.objD X n = (AlgebraicTopology.AlternatingFaceMapComplex.objD ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.obj (Opposite.op X)) n).unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.AlternatingCofaceMapComplex.objD X n ≫ AlgebraicTopology.AlternatingCofaceMapComplex.objD X (n + 1) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.CosimplicialObject C<GOAL>(AlgebraicTopology.alternatingCofaceMapComplex C).obj X = AlgebraicTopology.AlternatingCofaceMapComplex.obj X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<GOAL>∀ {X Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y), (AlgebraicTopology.alternatingCofaceMapComplex C).map f = AlgebraicTopology.AlternatingCofaceMapComplex.map f
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<VAR>i : ℕ<GOAL>(CategoryTheory.Abelian.DoldKan.comparisonN.hom.app X).f i = ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).unitIso.hom.app (CategoryTheory.Abelian.DoldKan.N.obj X)).f i ≫ ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).inverse.map ((AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi A).inv.app X)).f i
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<VAR>i : ℕ<GOAL>(CategoryTheory.Abelian.DoldKan.comparisonN.inv.app X).f i = ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).inverse.map ((AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi A).hom.app X)).f i ≫ ((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).unitIso.inv.app (CategoryTheory.Abelian.DoldKan.N.obj X)).f i
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<GOAL>CategoryTheory.Abelian.DoldKan.equivalence.functor = CategoryTheory.Abelian.DoldKan.N
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<GOAL>CategoryTheory.Abelian.DoldKan.equivalence.inverse = CategoryTheory.Abelian.DoldKan.Γ
<VAR>I : Type u<VAR>X : I → TopCat<VAR>i : I<VAR>x₀ x₁ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))<VAR>p : x₀ ⟶ x₁<GOAL>(FundamentalGroupoidFunctor.proj X i).map p = Path.Homotopic.proj i p
<VAR>I : Type u<VAR>X : I → TopCat<VAR>g : (i : I) → ↑(π.obj (X i))<VAR>i : I<GOAL>((FundamentalGroupoidFunctor.piToPiTop X).obj g).as i = (g i).as
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>∀ {X_1 Y : (i : I) → ↑(π.obj (X i))} (p : X_1 ⟶ Y), (FundamentalGroupoidFunctor.piToPiTop X).map p = Path.Homotopic.pi p
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>(FundamentalGroupoidFunctor.piIso X).hom = FundamentalGroupoidFunctor.piToPiTop X
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>(FundamentalGroupoidFunctor.piIso X).inv = CategoryTheory.Functor.pi' (FundamentalGroupoidFunctor.proj X)
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>(FundamentalGroupoidFunctor.coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)) = CategoryTheory.Limits.Fan.mk (π.obj (TopCat.of ((i : I) → ↑(X i)))) (FundamentalGroupoidFunctor.proj X)
<VAR>A B : TopCat<VAR>x₀ x₁ : ↑(π.obj (TopCat.of (↑A × ↑B)))<VAR>p : x₀ ⟶ x₁<GOAL>(FundamentalGroupoidFunctor.projLeft A B).map p = Path.Homotopic.projLeft p
<VAR>A B : TopCat<VAR>x₀ x₁ : ↑(π.obj (TopCat.of (↑A × ↑B)))<VAR>p : x₀ ⟶ x₁<GOAL>(FundamentalGroupoidFunctor.projRight A B).map p = Path.Homotopic.projRight p
<VAR>A B : TopCat<VAR>g : ↑(π.obj A) × ↑(π.obj B)<GOAL>(FundamentalGroupoidFunctor.prodToProdTop A B).obj g = { as := (g.1.as, g.2.as) }
<VAR>A B : TopCat<VAR>x₀ x₁ : ↑(π.obj A)<VAR>y₀ y₁ : ↑(π.obj B)<VAR>p₀ : x₀ ⟶ x₁<VAR>p₁ : y₀ ⟶ y₁<GOAL>(FundamentalGroupoidFunctor.prodToProdTop A B).map (p₀, p₁) = Path.Homotopic.prod p₀ p₁
<VAR>A B : TopCat<GOAL>(FundamentalGroupoidFunctor.prodIso A B).inv = (FundamentalGroupoidFunctor.projLeft A B).prod' (FundamentalGroupoidFunctor.projRight A B)
<VAR>A B : TopCat<GOAL>(FundamentalGroupoidFunctor.prodIso A B).hom = FundamentalGroupoidFunctor.prodToProdTop A B
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.NormalizedMooreComplex.objX X 0 = ⊤
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1) = Finset.univ.inf fun k => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.NormalizedMooreComplex.objD X (n + 1) ≫ AlgebraicTopology.NormalizedMooreComplex.objD X n = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>(AlgebraicTopology.NormalizedMooreComplex.obj X).X n = CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X : CategoryTheory.SimplicialObject C<VAR>i j : ℕ<GOAL>(AlgebraicTopology.NormalizedMooreComplex.obj X).d i j = if h : i = j + 1 then CategoryTheory.eqToHom ⋯ ≫ match j with | 0 => (Finset.univ.inf fun k => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ CategoryTheory.inv ⊤.arrow | n.succ => (Finset.univ.inf fun k => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)).factorThru ((Finset.univ.inf fun k => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ else 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<VAR>n : ℕ<GOAL>(AlgebraicTopology.NormalizedMooreComplex.map f).f n = (AlgebraicTopology.NormalizedMooreComplex.objX Y n).factorThru ((AlgebraicTopology.NormalizedMooreComplex.objX X n).arrow ≫ f.app (Opposite.op (SimplexCategory.mk n))) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<GOAL>∀ {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y), (AlgebraicTopology.normalizedMooreComplex C).map f = AlgebraicTopology.NormalizedMooreComplex.map f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>(AlgebraicTopology.normalizedMooreComplex C).obj X = AlgebraicTopology.NormalizedMooreComplex.obj X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>((AlgebraicTopology.normalizedMooreComplex C).obj X).d (n + 1) n = AlgebraicTopology.NormalizedMooreComplex.objD X n
<VAR>X : TopCat<VAR>x₀ x₁ : ↑X<VAR>hx₀ : x₀ = x₁<GOAL>ContinuousMap.Homotopy.hcast hx₀ = CategoryTheory.eqToHom ⋯
<VAR>X₁ X₂ Y : TopCat<VAR>f : C(↑X₁, ↑Y)<VAR>g : C(↑X₂, ↑Y)<VAR>x₀ x₁ : ↑X₁<VAR>x₂ x₃ : ↑X₂<VAR>p : Path x₀ x₁<VAR>q : Path x₂ x₃<VAR>hfg : ∀ (t : ↑I), f (p t) = g (q t)<GOAL>(π.map f).map ⟦p⟧ = ContinuousMap.Homotopy.hcast ⋯ ≫ (π.map g).map ⟦q⟧ ≫ ContinuousMap.Homotopy.hcast ⋯
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>i : ULift.{u, 0} ↑I<VAR>x : ↑X<GOAL>H.uliftMap (i, x) = H (i.down, x)
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁<GOAL>(π.map f).map p = ContinuousMap.Homotopy.hcast ⋯ ≫ (π.map H.uliftMap).map (ContinuousMap.Homotopy.prodToProdTopI (𝟙 (FundamentalGroupoid.fromTop { down := 0 })) p) ≫ ContinuousMap.Homotopy.hcast ⋯
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁<GOAL>(π.map g).map p = ContinuousMap.Homotopy.hcast ⋯ ≫ (π.map H.uliftMap).map (ContinuousMap.Homotopy.prodToProdTopI (𝟙 (FundamentalGroupoid.fromTop { down := 1 })) p) ≫ ContinuousMap.Homotopy.hcast ⋯
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x : ↑X<GOAL>⟦H.evalAt x⟧ = ContinuousMap.Homotopy.hcast ⋯ ≫ (π.map H.uliftMap).map (ContinuousMap.Homotopy.prodToProdTopI unitInterval.uhpath01 (𝟙 (FundamentalGroupoid.fromTop x))) ≫ ContinuousMap.Homotopy.hcast ⋯
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁<GOAL>(π.map f).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧ ⟦H.evalAt x₀⟧ ≫ (π.map g).map p = H.diagonalPath' p
<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 : ℕ<VAR>hqn : n < q<GOAL>(AlgebraicTopology.DoldKan.homotopyPToId X (q + 1)).hom n (n + 1) = (AlgebraicTopology.DoldKan.homotopyPToId X q).hom n (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>i j : ℕ<GOAL>(AlgebraicTopology.DoldKan.homotopyPInftyToId X).hom i j = (AlgebraicTopology.DoldKan.homotopyPToId X (j + 1)).hom i j
<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.Abelian A<VAR>Y : CategoryTheory.SimplicialObject A<GOAL>AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyHomInvId = Homotopy.ofEq ⋯
<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.Abelian A<VAR>Y : CategoryTheory.SimplicialObject A<GOAL>AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.inv = AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y
<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.Abelian A<VAR>Y : CategoryTheory.SimplicialObject A<GOAL>AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.hom = AlgebraicTopology.inclusionOfMooreComplexMap Y
<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>CategoryTheory.Abelian A<VAR>Y : CategoryTheory.SimplicialObject A<GOAL>AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId = (Homotopy.ofEq ⋯).trans (AlgebraicTopology.DoldKan.homotopyPInftyToId Y)
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.HigherFacesVanish (n + 1) ((AlgebraicTopology.inclusionOfMooreComplexMap X).f (n + 1))
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<VAR>n : ℕ<GOAL>(AlgebraicTopology.NormalizedMooreComplex.objX X n).Factors (AlgebraicTopology.DoldKan.PInfty.f n)
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X).f n = (AlgebraicTopology.NormalizedMooreComplex.objX X n).factorThru (AlgebraicTopology.DoldKan.PInfty.f n) ⋯
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<GOAL>AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X ≫ AlgebraicTopology.inclusionOfMooreComplexMap X = AlgebraicTopology.DoldKan.PInfty
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X Y : CategoryTheory.SimplicialObject A<VAR>f : X ⟶ Y<GOAL>AlgebraicTopology.AlternatingFaceMapComplex.map f ≫ AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y = AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X ≫ AlgebraicTopology.NormalizedMooreComplex.map f
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<GOAL>AlgebraicTopology.DoldKan.PInfty ≫ AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X = AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.Abelian A<VAR>X : CategoryTheory.SimplicialObject A<GOAL>AlgebraicTopology.inclusionOfMooreComplexMap X ≫ AlgebraicTopology.DoldKan.PInfty = AlgebraicTopology.inclusionOfMooreComplexMap X
<VAR>M : ℝ<VAR>hM : M ≤ 1<GOAL>Complex.stolzSet M = ∅
<VAR>M : ℝ<VAR>hM : 1 < M<GOAL>Filter.map Complex.ofReal' (𝓝[<] 1) ≤ 𝓝[Complex.stolzSet M] 1
<VAR>s : ℝ<GOAL>∃ M ε, 0 < M ∧ 0 < ε ∧ ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>∃ M ε, 0 < M ∧ 0 < ε ∧ {z | 1 - ε < z.re} ∩ Complex.stolzCone s ⊆ Complex.stolzSet M
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>∃ M, 𝓝[Complex.stolzCone s] 1 ≤ 𝓝[Complex.stolzSet M] 1
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 l)<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>Filter.Tendsto (fun n => (1 - z) * ∑ i ∈ Finset.range n, (l - ∑ j ∈ Finset.range (i + 1), f j) * z ^ i) Filter.atTop (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 l)<VAR>M : ℝ<GOAL>Filter.Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[Complex.stolzSet M] 1) (𝓝 l)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 l)<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>Filter.Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[Complex.stolzCone s] 1) (𝓝 l)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 l)<GOAL>Filter.Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (Filter.map Complex.ofReal' (𝓝[<] 1)) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 l)<GOAL>Filter.Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n q : ℕ<GOAL>(AlgebraicTopology.DoldKan.Q q).f (n + 1) = ∑ i ∈ Finset.filter (fun i => ↑i < q) Finset.univ, (AlgebraicTopology.DoldKan.P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.MorphComponents.id X n).a = AlgebraicTopology.DoldKan.PInfty.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>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(AlgebraicTopology.DoldKan.MorphComponents.id X n).b i = X.σ i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.MorphComponents.id X n).φ = 𝟙 (X _[n + 1])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : AlgebraicTopology.DoldKan.MorphComponents X n Z<VAR>h : Z ⟶ Z'<GOAL>(f.postComp h).a = f.a ≫ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : AlgebraicTopology.DoldKan.MorphComponents X n Z<VAR>h : Z ⟶ Z'<VAR>i : Fin (n + 1)<GOAL>(f.postComp h).b i = f.b i ≫ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : AlgebraicTopology.DoldKan.MorphComponents X n Z<VAR>h : Z ⟶ Z'<GOAL>(f.postComp h).φ = f.φ ≫ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X X' : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Z : C<VAR>f : AlgebraicTopology.DoldKan.MorphComponents X n Z<VAR>g : X' ⟶ X<GOAL>(f.preComp g).a = g.app (Opposite.op [n + 1]) ≫ f.a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X X' : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Z : C<VAR>f : AlgebraicTopology.DoldKan.MorphComponents X n Z<VAR>g : X' ⟶ X<VAR>i : Fin (n + 1)<GOAL>(f.preComp g).b i = g.app (Opposite.op [n]) ≫ f.b i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X X' : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Z : C<VAR>f : AlgebraicTopology.DoldKan.MorphComponents X n Z<VAR>g : X' ⟶ X<GOAL>(f.preComp g).φ = g.app (Opposite.op [n + 1]) ≫ f.φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Preadditive.DoldKan.equivalence.functor = CategoryTheory.Preadditive.DoldKan.N
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Preadditive.DoldKan.equivalence.inverse = CategoryTheory.Preadditive.DoldKan.Γ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Preadditive.DoldKan.equivalence.unitIso = AlgebraicTopology.DoldKan.Γ₂N₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>CategoryTheory.Preadditive.DoldKan.equivalence.counitIso = AlgebraicTopology.DoldKan.N₂Γ₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<GOAL>∀ {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y), (AlgebraicTopology.DoldKan.N₁.map f).f = AlgebraicTopology.DoldKan.PInfty ≫ AlgebraicTopology.AlternatingFaceMapComplex.map f
<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.N₁.obj X).X = AlgebraicTopology.AlternatingFaceMapComplex.obj X
<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.N₁.obj X).p = AlgebraicTopology.DoldKan.PInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)} (f : X ⟶ Y) (i : ℕ), (AlgebraicTopology.DoldKan.N₂.map f).f.f i = AlgebraicTopology.DoldKan.PInfty.f i ≫ f.f.app (Opposite.op (SimplexCategory.mk i))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)<VAR>i : ℕ<GOAL>(AlgebraicTopology.DoldKan.N₂.obj P).p.f i = AlgebraicTopology.DoldKan.PInfty.f i ≫ P.p.app (Opposite.op (SimplexCategory.mk i))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)<VAR>i j : ℕ<GOAL>(AlgebraicTopology.DoldKan.N₂.obj P).X.d i j = if h : i = j + 1 then CategoryTheory.eqToHom ⋯ ≫ ∑ i : Fin (j + 2), (-1) ^ ↑i • P.X.δ i else 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.N₂.obj P).X.X n = P.X.obj (Opposite.op (SimplexCategory.mk 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.toKaroubiCompN₂IsoN₁.hom.app X).f = AlgebraicTopology.DoldKan.PInfty
<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.toKaroubiCompN₂IsoN₁.inv.app X).f = AlgebraicTopology.DoldKan.PInfty