nonDegenerateEquiv — Mathlib

English

There is an equivalence between nondegenerate d-simplices of Δ[n] and order embeddings Fin(d+1) ↪o Fin(n+1).

Русский

Существует эквивалентность между неdegenerate d-симплексами Δ[n] и порядковыми вложениями Fin(d+1) ↪o Fin(n+1).

LaTeX

$$(Δ[n] : SSet).nonDegenerate d ≃ (Fin (d+1) ↪o Fin (n+1))$$

Lean4

/-- Nondegenerate `d`-dimensional simplices of the standard simplex `Δ[n]`
identify to order embeddings `Fin (d + 1) ↪o Fin (n + 1)`. -/
@[simps! apply_apply symm_apply_coe]
def nonDegenerateEquiv {n d : ℕ} : (Δ[n] : SSet.{u}).nonDegenerate d ≃ (Fin (d + 1) ↪o Fin (n + 1))
    where
  toFun s := OrderEmbedding.ofStrictMono _ ((mem_nonDegenerate_iff_strictMono _).1 s.2)
  invFun s := ⟨objEquiv.symm (.mk s.toOrderHom), by simpa [mem_nonDegenerate_iff_strictMono] using s.strictMono⟩
  left_inv _ := by aesop

Похожие утверждения