graph_eq_range_prod — Mathlib

English

If a linear map f: G → H × I is surjective onto the first coordinate and satisfies a vertical-line separation property, then the range of f is the graph of some linear map f': H → I.

Русский

Пусть линейное отображение f: G → H × I сюръективно по первой координате и удовлетворяет условию разделения по «вертикальной линии»; тогда образ f равен графику некоторого линейного отображения f': H → I.

LaTeX

$$$\\exists f': H \\to I\\,\\text{linear},\\quad \\operatorname{range} f = \\text{graph}(f')$$$

Lean4

theorem graph_eq_range_prod : f.graph = range (LinearMap.id.prod f) :=
  by
  ext x
  exact ⟨fun hx => ⟨x.1, Prod.ext rfl hx.symm⟩, fun ⟨u, hu⟩ => hu ▸ rfl⟩

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