map_apply

Mathlib.LinearAlgebra.Basis.Defs

URI: https://scilib.ai/kg/mathlib#Module.Basis.map_apply

English

The i-th vector of the mapped basis equals the image under f of the i-th vector of the original basis: (b.map f)_i = f(b_i).

Русский

i-й вектор нового базиса равен image под действием f от i-го вектора исходного базиса: (b.map f)_i = f(b_i).

LaTeX

$$$b.map\ f\ i = f(b_i)$$$

Lean4

@[simp]
theorem map_apply (i) : b.map f i = f (b i) :=
  rfl

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

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

Разделы

Аффилиация

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