graph — Mathlib

English

The graph of a linear partially defined map f is a submodule of E × F.

Русский

Граф линейного частично заданного отображения f является подмодулем множества E × F.

LaTeX

$$$\mathrm{graph}(f) \leq \mathrm{Submodule}(E \times F)$$$

Lean4

/-- The graph of a `LinearPMap` viewed as a submodule on `E × F`. -/
def graph (f : E →ₗ.[R] F) : Submodule R (E × F) :=
  f.toFun.graph.map (f.domain.subtype.prodMap (LinearMap.id : F →ₗ[R] F))

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