English
Let t_i be submodules of M and N a submodule of M. Supremum left action distributes: (⨆ i, t_i) • N = ⨆ i, t_i • N.
Русский
Пусть t_i — подмодули M, N — подмодуль M. Применение верхнего предела слева распределяется: (⨆ i, t_i) • N = ⨆ i, t_i • N.
LaTeX
$$$ (\bigvee_i t_i) \cdot N = \bigvee_i (t_i \cdot N) $$$
Lean4
theorem iSup_smul {ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} : (⨆ i, t i) • N = ⨆ i, t i • N :=
le_antisymm
(smul_le.mpr fun t ht s hs ↦
iSup_induction _ (motive := (· • s ∈ _)) ht (fun i t ht ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
(by simp_rw [zero_smul]; apply zero_mem) fun x y ↦ by simp_rw [add_smul]; apply add_mem)
(iSup_le fun i ↦ Submodule.smul_mono_left <| le_iSup _ i)
