English
Let f be an R-endomorphism of M. If for every i in a given finite set s we have f(N_i) ⊆ N_i, then f maps the supremum of the N_i (over i in s) into itself. In symbols, f(⨆_{i∈s} N_i) ⊆ ⨆_{i∈s} N_i.
Русский
Пусть f — R-однозначный оператор над M. Если для каждого i из конечного множества s выполняется f(N_i) ⊆ N_i, тогда f отображает верхнюю грань сумм N_i (по i из s) в саму эту верхнюю грань; то есть f(⨆_{i∈s} N_i) ⊆ ⨆_{i∈s} N_i.
LaTeX
$$$\\displaystyle \\forall f \\in \\mathrm{End}_R(M),\\; (\\forall i \\in s,\\; f(N_i) \\subseteq N_i) \\Rightarrow f\\left(\\bigvee_{i\\in s} N_i\\right) \\subseteq \\bigvee_{i\\in s} N_i$$$
Lean4
theorem mapsTo_biSup_of_mapsTo {ι : Type*} {N : ι → Submodule R M} (s : Set ι) {f : Module.End R M}
(hf : ∀ i, MapsTo f (N i) (N i)) : MapsTo f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i) :=
by
replace hf : ∀ i, (N i).map f ≤ N i := fun i ↦ Submodule.map_le_iff_le_comap.mpr (hf i)
suffices (⨆ i ∈ s, N i).map f ≤ ⨆ i ∈ s, N i from Submodule.map_le_iff_le_comap.mp this
simpa only [Submodule.map_iSup] using iSup₂_mono <| fun i _ ↦ hf i
