equiv_apply

Mathlib.LinearAlgebra.Basis.Defs

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

English

If g(i) = f(b i) for all i, then constr b S g = f.

Русский

Если g(i) = f(b i) для всех i, то constr b S g = f.

LaTeX

$$$\\forall i,\\; g(i) = f(b i) \\Rightarrow \\mathrm{constr}\\, b\\ S\\ g = f.$$$

Lean4

@[simp]
theorem equiv_apply : b.equiv b' e (b i) = b' (e i) := by simp [Basis.equiv]

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

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

Разделы

Аффилиация

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