English
If two partial linear maps f and g agree on the intersection of their domains, there exists a unique partial linear map on the join of their domains that extends both f and g.
Русский
Если два частичных линейных отображения f и g согласованы на пересечении их областей определения, существует единственный частичный линейный отображение на объединении областей, которое extends как f, так и g.
LaTeX
$$$\\text{If } f,g:\\ E \\to\\!_{R} F\\text{ satisfy }\\forall x\\in\\operatorname{dom}(f),\\forall y\\in\\operatorname{dom}(g),\\ x=y\\Rightarrow f(x)=g(y),\\ \\exists!\\; h: E\\to\\!_{R} F\\text{ with }\\operatorname{dom}(h)=\\operatorname{dom}(f)\\lor\\operatorname{dom}(g) \\text{ and } h|_{\\operatorname{dom}(f)}=f,\\ h|_{\\operatorname{dom}(g)}=g.$$$
Lean4
/-- Given two partial linear maps that agree on the intersection of their domains,
`f.sup g h` is the unique partial linear map on `f.domain ⊔ g.domain` that agrees
with `f` and `g`. -/
protected noncomputable def sup (f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) :
E →ₗ.[R] F :=
⟨_, Classical.choose (sup_aux f g h)⟩
