Theorems · Definition · algebraic topology

SSet.Subcomplex.PairingCore.IsProper.recOn

{X : SSet} →
  {A : X.Subcomplex} →
    {h : A.PairingCore} →
      {motive : h.IsProper → Sort u_2} →
        (t : h.IsProper) →
          ((isUniquelyCodimOneFace : ∀ (s : h.ι), (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS) → motive ⋯) →
            motive t

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Cited by: 0 results in Mathlib
Foundations: Depth 41 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

SSetstatement and proof · cited by 1,283
SSet.Subcomplexstatement and proof · cited by 461
SSet.N.toSstatement and proof · cited by 171
SSet.Subcomplex.N.toNstatement and proof · cited by 126
SSet.Subcomplex.PairingCorestatement and proof · cited by 50
SSet.Subcomplex.PairingCore.ιstatement and proof · cited by 42
SSet.S.IsUniquelyCodimOneFacestatement and proof · cited by 19
SSet.Subcomplex.PairingCore.type₁statement and proof · cited by 13
SSet.Subcomplex.PairingCore.type₂statement and proof · cited by 12
SSet.Subcomplex.PairingCore.IsProperstatement and proof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.