eq_of_le_of_domain_eq — Mathlib

English

The set of points where two partial linear maps agree forms a submodule, i.e., the locus of equality is a submodule of E.

Русский

Множество точек, на которых два частичных линейных отображения совпадают, образуют подмодуль.

LaTeX

$$eqLocus (f g) : Submodule R E$$

Lean4

theorem eq_of_le_of_domain_eq {f g : E →ₗ.[R] F} (hle : f ≤ g) (heq : f.domain = g.domain) : f = g :=
  dExt heq hle.2

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