Mathlib Map

Theorems · Theorem · algebraic topology

SSet.Subcomplex.Pairing.innerAnodyneExtensions

∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [inst : P.IsRegular] [P.IsInner], SSet.innerAnodyneExtensions A.ι
Defined in
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
Cited by
2 results in Mathlib
Foundations
Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SSet.Subcomplex.Pairing.IsRegularSSet.Subcomplex.Pairing.IsInner
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.prodStdSimplex.innerAnodyneExtensions_unionProd_ι · cited by 1prodStdSimplex.innerAnody…SSet.strongInnerAnodyneExtensions_le_innerAnodyneExtensions · cited by 0SSet.strongInnerAnodyneEx…Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.Functor.obj · cited by 19642Functor.objCategoryTheory.Functor.map · cited by 8698Functor.mapSSet · cited by 1283SSetOrder.succ · cited by 633Order.succCategoryTheory.homOfLE · cited by 554CategoryTheory.homOfLESSet.stdSimplex · cited by 499SSet.stdSimplexSSet.Subcomplex · cited by 461SSet.SubcomplexIsMax · cited by 372IsMaxSSet.Subcomplex.toSSet · cited by 315Subcomplex.toSSetSSet.N.toS · cited by 171N.toSSSet.S.dim · cited by 162S.dimSSet.Subcomplex.ι · cited by 136Subcomplex.ιSSet.Subcomplex.N.toN · cited by 126N.toNSSet.Subcomplex.Pairing · cited by 117Subcomplex.PairingPairing.innerAnodyneExtensionsCITED BYCITES

Cites39

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.