English
Let g be a submodule of E × F that satisfies a compatibility condition hg. For a ∈ E in the projection g.map fst, there exists a unique b ∈ F with (a,b) ∈ g.
Русский
Пусть g — подмодуль E × F, удовлетворяющий условию совместимости hg. Для а ∈ E, попадающего в проекции g, существует единственный b ∈ F такой, что (a,b) ∈ g.
LaTeX
$$∃! b ∈ F, (a,b) ∈ g, при условии ha : a ∈ g.map (fst) и hg : ∀ {x}, x ∈ g → x.fst = 0 → x.snd = 0$$
Lean4
theorem existsUnique_from_graph {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)) :
∃! b : F, (a, b) ∈ g := by
refine existsUnique_of_exists_of_unique ?_ ?_
· convert ha
simp
intro y₁ y₂ hy₁ hy₂
have hy : ((0 : E), y₁ - y₂) ∈ g := by
convert g.sub_mem hy₁ hy₂
exact (sub_self _).symm
exact sub_eq_zero.mp (hg hy (by simp))
