σ_mem_degenerate — Mathlib

English

For i in Fin(n+1), the degeneracy σ_i applied to x is degenerate in dimension n+1.

Русский

Для любого i в Fin(n+1) отображение σ_i примененное к x есть degenerate в размерности n+1.

LaTeX

$$$ \forall i \in \mathrm{Fin}(n+1), \; X.\sigma_i(x) \in X.degenerate(n+1) $$$

Lean4

theorem σ_mem_degenerate (i : Fin (n + 1)) (x : X _⦋n⦌) : X.σ i x ∈ X.degenerate (n + 1) :=
  ⟨n, by cutsat, SimplexCategory.σ i, Set.mem_range_self x⟩

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