obj₀Equiv — Mathlib

English

For every n, the set of 0-simplices of the standard n-simplex Δ[n] is in bijection with Fin(n+1).

Русский

Для каждого n множество нулевых симплектов стандартного симплекса Δ[n] сопоставимо с Fin(n+1).

LaTeX

$$$(\Delta[n])_0 \\cong \\mathrm{Fin}(n+1)$$$

Lean4

/-- The `0`-simplices of `Δ[n]` identify to the elements in `Fin (n + 1)`. -/
@[simps]
def obj₀Equiv {n : ℕ} : Δ[n] _⦋0⦌ ≃ Fin (n + 1) where
  toFun x := x 0
  invFun i := const _ i _
  left_inv x := by ext i : 1; fin_cases i; rfl

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