graph_map_snd_eq_range

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.graph_map_snd_eq_range

English

The map of the graph by the snd projection equals the range of f.toFun.

Русский

Образ графа по проекции snd равен множеству образов функции f.

LaTeX

$$$\mathrm{graph}(f) \xrightarrow{\text{snd}} \mathrm{range}(f).$$$

Lean4

theorem graph_map_snd_eq_range (f : E →ₗ.[R] F) : f.graph.map (LinearMap.snd R E F) = LinearMap.range f.toFun := by ext;
  simp

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

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

Разделы

Аффилиация

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