le_of_eqLocus_ge — Mathlib

English

If two partial linear maps f and g agree on the domain of f (i.e., f = g on f.domain), then f ≤ g in the partial-map order.

Русский

Если два частичных линейных отображения f и g совпадают на области определения f (то есть f и g совпадают на dom(f)), то f ≤ g в соответствующем порядке.

LaTeX

$$$\\text{If } f,g:\\ E \\to\\!_{R} F\\text{ with } f(\\mathrm{dom}\\,f) \\subseteq \\{x: f(x)=g(x)\\},\\ \\text{then } f \\le g.$$$

Lean4

theorem le_of_eqLocus_ge {f g : E →ₗ.[R] F} (H : f.domain ≤ f.eqLocus g) : f ≤ g :=
  suffices f ≤ f ⊓ g from le_trans this inf_le_right
  ⟨H, fun _x _y hxy => ((inf_le_left : f ⊓ g ≤ f).2 hxy.symm).symm⟩

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