English
A compatibility lemma about eqLocus: equality of two partial maps propagates through sums and additions.
Русский
Лемма совместимости eqLocus: равенство двух частичных отображений сохраняется под сложением.
LaTeX
$$eqLocus (f g) x → eqLocus (f g) y → eqLocus (f g) (x+y)$$
Lean4
/-- Given two partial linear maps `f`, `g`, the set of points `x` such that
both `f` and `g` are defined at `x` and `f x = g x` form a submodule. -/
def eqLocus (f g : E →ₗ.[R] F) : Submodule R E
where
carrier := {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), f ⟨x, hf⟩ = g ⟨x, hg⟩}
zero_mem' := ⟨zero_mem _, zero_mem _, f.map_zero.trans g.map_zero.symm⟩
add_mem'
{x
y} := fun ⟨hfx, hgx, hx⟩ ⟨hfy, hgy, hy⟩ ↦
⟨add_mem hfx hfy, add_mem hgx hgy, by simp_all [← AddMemClass.mk_add_mk, f.map_add, g.map_add]⟩
smul_mem' c
x := fun ⟨hfx, hgx, hx⟩ ↦
⟨smul_mem _ c hfx, smul_mem _ c hgx,
by
have {f : E →ₗ.[R] F} (hfx) : (⟨c • x, smul_mem _ c hfx⟩ : f.domain) = c • ⟨x, hfx⟩ := by simp
rw [this hfx, this hgx, f.map_smul, g.map_smul, hx]⟩
