English
The extension is additive: (I + J).extended = I.extended + J.extended.
Русский
Расширение сохраняет сложение: (I+J).extended = I.extended + J.extended.
LaTeX
$$$ (I+J).extended L hf = (I.extended L hf) + (J.extended L hf) $$$
Lean4
theorem extended_add : (I + J).extended L hf = (I.extended L hf) + (J.extended L hf) :=
by
apply coeToSubmodule_injective
simp only [coe_extended_eq_span, coe_add, Submodule.add_eq_sup, ← span_union, ← Set.image_union]
apply Submodule.span_eq_span
· rintro _ ⟨y, hy, rfl⟩
obtain ⟨i, hi, j, hj, rfl⟩ := (mem_add I J y).mp <| SetLike.mem_coe.mp hy
rw [RingHom.map_add]
exact
add_mem (Submodule.subset_span ⟨i, Set.mem_union_left _ hi, by simp⟩)
(Submodule.subset_span ⟨j, Set.mem_union_right _ hj, by simp⟩)
· rintro _ ⟨y, hy, rfl⟩
suffices y ∈ I + J from SetLike.mem_coe.mpr <| Submodule.subset_span ⟨y, by simp [this]⟩
exact
hy.elim (fun h ↦ (mem_add I J y).mpr ⟨y, h, 0, zero_mem J, add_zero y⟩)
(fun h ↦ (mem_add I J y).mpr ⟨0, zero_mem I, y, h, zero_add y⟩)
