Theorems · Definition · algebraic topology

SSet.prodStdSimplex.pairingCore.min

{m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} → (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) → {d : ℕ} → x.dim = d → Fin (d + 1)

Let x be a nondegenerate d-simplex of Δ[m + 1] ⊗ Δ[n] which does not belong to Λ[m + 1, k.castSucc].unionProd ∂Δ[n]. This is the smallest l : Fin (d + 1) such that x l is of the form (k.succ, _).

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Cited by

18 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound