map'_zero — Mathlib

English

Let f be an order-preserving map from Fin(n+1) to Fin(m+1). Then the induced map map' f sends 0 to 0, i.e. map'(f)(0) = 0.

Русский

Пусть f — порядок-сохранное отображение из Fin(n+1) в Fin(m+1). Тогда порожденное отображение map' f отправляет 0 в 0, то есть map'(f)(0) = 0.

LaTeX

$$$map'(f)(0)=0$$$

Lean4

@[simp]
theorem map'_zero (f : Fin (n + 1) →o Fin (m + 1)) : map' f 0 = 0 := by
  simp [← Fin.castSucc_zero, -Fin.castSucc_zero', map'_eq_castSucc_iff]

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