valFromGraph — Mathlib

English

In the Submodule setting, the same existence-uniqueness property from graph holds for the projected map.

Русский

В рамках Submodule сохраняется свойство существования и уникальности, вытекающее из графа для проекции отображения.

LaTeX

$$∀ g hg ha, ∃! b : F, (a,b) ∈ g$$

Lean4

/-- Auxiliary definition to unfold the existential quantifier. -/
noncomputable def valFromGraph {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) {a : E} (ha : a ∈ g.map (LinearMap.fst R E F)) :
    F :=
  (ExistsUnique.exists (existsUnique_from_graph (@hg) ha)).choose

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