English
If the domains of f and g are disjoint, then whenever x ∈ dom f and y ∈ dom g satisfy (x:E) = y, we have f x = g y.
Русский
Если области определения f и g взаимно не пересекаются, то при любых x ∈ dom f, y ∈ dom g, для которых (x:E) = y, выполняется f x = g y.
LaTeX
$$Disjoint(f.domain, g.domain) → ∀ x ∈ f.domain, ∀ y ∈ g.domain, (x:E) = y → f x = g y$$
Lean4
/-- Hypothesis for `LinearPMap.sup` holds, if `f.domain` is disjoint with `g.domain`. -/
theorem sup_h_of_disjoint (f g : E →ₗ.[R] F) (h : Disjoint f.domain g.domain) (x : f.domain) (y : g.domain)
(hxy : (x : E) = y) : f x = g y := by
rw [disjoint_def] at h
have hy : y = 0 := Subtype.eq (h y (hxy ▸ x.2) y.2)
have hx : x = 0 := Subtype.eq (hxy.trans <| congr_arg _ hy)
simp [*]
