English
Let (S_i)_{i∈I} be a directed family of submodules of M. Then the carrier of their supremum equals the union of the carriers of the S_i; in symbols, (iSup S : Set M) = ⋃ i, S i.
Русский
Пусть (S_i) для i из множества I образует направленную семью подмодулов подмодуля M. Тогда носитель их супремума равен объединению носителей всех S_i; то есть (iSup S : Set M) = ⋃ i, S i.
LaTeX
$$$$( (\\iSup_i S(i)) : \\mathrm{Set} M ) = \\bigcup_i S(i). $$$$
Lean4
@[simp]
theorem coe_iSup_of_directed {ι} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (· ≤ ·) S) :
((iSup S : Submodule R M) : Set M) = ⋃ i, S i :=
let s : Submodule R M :=
{ __ := AddSubmonoid.copy _ _ (AddSubmonoid.coe_iSup_of_directed H).symm
smul_mem' := fun r _ hx ↦
have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
Set.mem_iUnion.mpr ⟨i, (S i).smul_mem' r hi⟩ }
have : iSup S = s :=
le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set M)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
this.symm ▸ rfl
