English
The span of the union of single_R i images over all i equals the span of F.N i in the appropriate tower, i.e., submodule_span_single.
Русский
Обобщенное замыкание по всем уровням фиксирует, что порождающее множество даёт тот же подпространственный каркас.
LaTeX
$$Submodule.span (reesAlgebra I) (⋃ i, single R i '' (F.N i : Set M)) = F.submodule$$
Lean4
theorem submodule_closure_single :
AddSubmonoid.closure (⋃ i, single R i '' (F.N i : Set M)) = F.submodule.toAddSubmonoid :=
by
apply le_antisymm
· rw [AddSubmonoid.closure_le, Set.iUnion_subset_iff]
rintro i _ ⟨m, hm, rfl⟩ j
rw [single_apply]
split_ifs with h
· rwa [← h]
· exact (F.N j).zero_mem
· intro f hf
rw [← f.sum_single]
apply AddSubmonoid.sum_mem _ _
rintro c -
exact AddSubmonoid.subset_closure (Set.subset_iUnion _ c <| Set.mem_image_of_mem _ (hf c))
