ofFn_congr

Mathlib.Data.List.OfFn

URI: https://scilib.ai/kg/mathlib#List.ofFn_congr

← MathLib Explorer

English

Same as above: when m = n, ofFn f = ofFn (f ∘ Fin.cast h.symm).

Русский

То же самое: если m = n, то ofFn f = ofFn (f ∘ Fin.cast h.symm).

LaTeX

$$$ \\operatorname{ofFn} f = \\operatorname{ofFn} (f \\circ \\operatorname{Fin.cast} (h^{-1})) $$$

Lean4

@[congr]
theorem ofFn_congr {m n : ℕ} (h : m = n) (f : Fin m → α) : ofFn f = ofFn fun i : Fin n => f (Fin.cast h.symm i) :=
  by
  subst h
  simp_rw [Fin.cast_refl, id]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru