cast_eq_self — Mathlib

English

Casting along the identity equality acts as the identity map: for every a in Fin(n), a.cast rfl = a.

Русский

Кастинг по тождественному равенству действует как тождественный отображение: для каждого a ∈ Fin(n) выполняется a.cast rfl = a.

LaTeX

$$$$\forall a:\\mathrm{Fin}(n),\\mathrm{Fin.cast}(\\mathrm{id}_n)\,a = a.$$$$

Lean4

@[simp]
theorem cast_eq_self (a : Fin n) : a.cast rfl = a :=
  rfl

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