map'_id — Mathlib

English

For every x in Fin(n+2), map' applied to the identity order hom yields x; i.e., map' OrderHom.id x = x.

Русский

Для любого x ∈ Fin(n+2) отображение map' от тождества сохраняет x; то есть map' OrderHom.id x = x.

LaTeX

$$$map'\\!(\\mathrm{OrderHom.id})\\,x = x$$$

Lean4

@[simp]
theorem map'_id (x : Fin (n + 2)) : map' OrderHom.id x = x :=
  by
  obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
  · rw [map'_eq_castSucc_iff]
    aesop
  · simp

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