map_eq

Mathlib.Data.Fin.Tuple.Reflection

URI: https://scilib.ai/kg/mathlib#FinVec.map_eq

← MathLib Explorer

English

For any f: α → β and v: Fin m → α, map f v = f ∘ v.

Русский

Для любого f: α → β и v: Fin m → α, map f v = f ∘ v.

LaTeX

$$$\mathrm{map}(f,v) = f \circ v$$$

Lean4

/-- This can be used to prove
```lean
example {f : α → β} (a₁ a₂ : α) : f ∘ ![a₁, a₂] = ![f a₁, f a₂] :=
  (map_eq _ _).symm
```
-/
@[simp]
theorem map_eq (f : α → β) {m} (v : Fin m → α) : map f v = f ∘ v :=
  seq_eq _ _

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

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

Разделы

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

Аффилиация

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