mem_graph_toLinearPMap

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#Submodule.mem_graph_toLinearPMap

← MathLib Explorer

English

Under hg, the graph of g.toLinearPMap equals g.

Русский

При условии hg график g.toLinearPMap равен g.

LaTeX

$$g.toLinearPMap.graph = g$$

Lean4

theorem mem_graph_toLinearPMap {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) (x : g.map (LinearMap.fst R E F)) :
    (x.val, g.toLinearPMap x) ∈ g := by
  rw [toLinearPMap_apply_aux hg]
  exact valFromGraph_mem hg x.2

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

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

Разделы

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

Аффилиация

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