English
Let f,g be linear partial maps with a compatibility condition H. Then for any x in the domain of f, any y in the domain of g, and any z in the join of the two domains, such that the underlying vectors satisfy (x : E) + (y : E) = (z : E), we have (f ⊔ g) z = f x + g y.
Русский
Пусть f,g — линейные частичные отображения и дано условие совместимости H. Тогда для любого x из домена f, любого y из домена g и любого z в объединении доменов, если векторные representatives удовлетворяют (x : E) + (y : E) = (z : E), выполняется (f ⊔ g) z = f x + g y.
LaTeX
$$$\forall f,g : E \to_{R}^{\mathrm{LinearPMap}} F\;\forall H\;\forall x \in \mathrm{dom}(f)\;\forall y \in \mathrm{dom}(g)\;\forall z \in \mathrm{dom}(f) \sqcup \mathrm{dom}(g),\; (x:E)+(y:E)= (z:E)\; \Rightarrow \ (f \sup g H)\, z = f\, x + g\, y.$$$
Lean4
theorem sup_apply {f g : E →ₗ.[R] F} (H : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) (x : f.domain)
(y : g.domain) (z : ↥(f.domain ⊔ g.domain)) (hz : (↑x : E) + ↑y = ↑z) : f.sup g H z = f x + g y :=
Classical.choose_spec (sup_aux f g H) x y z hz
