objEquiv_toOrderHom_apply — Mathlib

English

For f: ⟨m⟩ ⟶ ⟨n⟩, the symmetrized equivalence sends f to the corresponding element; its value on i-th coordinate equals the i-th component of f.

Русский

Для f: ⟨m⟩ ⟶ ⟨n⟩ симметрическая эквив отправляет f к соответствующему элементу; значение на i-ой координате равно i-й компоненте f.

LaTeX

$$$(\text{objEquiv}.symm f)_{i} = f_{i}$$$

Lean4

@[simp]
theorem objEquiv_toOrderHom_apply {n i : ℕ} (x : (stdSimplex.{u} ^⦋n⦌).obj (op ⦋i⦌)) (j : Fin (i + 1)) :
    DFunLike.coe (F := Fin (i + 1) →o Fin (n + 1))
        ((DFunLike.coe (F := Δ[n].obj (op ⦋i⦌) ≃ (⦋i⦌ ⟶ ⦋n⦌)) objEquiv x)).toOrderHom j =
      x j :=
  rfl

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