English
The additive submonoid generated by the supremum of a family of submodules equals the supremum of the additive submonoids generated by each submodule.
Русский
Порождённая аддитивная подмоноида верхушка множества подмодулей равна верхушке аддитивных порождающих их поодиночке подмодулей.
LaTeX
$$$$ (\\bigvee_i p_i)^{+} = \\bigvee_i (p_i)^{+}, $$$$
Lean4
theorem iSup_toAddSubmonoid {ι : Sort*} (p : ι → Submodule R M) :
(⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid :=
by
refine le_antisymm (fun x => ?_) (iSup_le fun i => toAddSubmonoid_mono <| le_iSup _ i)
simp_rw [iSup_eq_span, AddSubmonoid.iSup_eq_closure, mem_toAddSubmonoid, coe_toAddSubmonoid]
intro hx
refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_) (fun r x _ hx => ?_) hx
· exact AddSubmonoid.subset_closure hx
· exact AddSubmonoid.zero_mem _
· exact AddSubmonoid.add_mem _ hx hy
· refine AddSubmonoid.closure_induction ?_ ?_ ?_ hx
· rintro x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩
apply AddSubmonoid.subset_closure (Set.mem_iUnion.mpr ⟨i, _⟩)
exact smul_mem _ r hix
· rw [smul_zero]
exact AddSubmonoid.zero_mem _
· intro x y _ _ hx hy
rw [smul_add]
exact AddSubmonoid.add_mem _ hx hy
