coe_iSup — Mathlib

English

For any S, an element x belongs to sSup S if and only if x belongs to the closure of the carrier of the supremum of s.toSubmodule over S.

Русский

Для множества S выполняется: x ∈ sSup S тогда и только тогда, когда x ∈ замыканию носителя супа подмодулей.

LaTeX

$${S : Set (ClosedSubmodule R N)} : x ∈ sSup S \iff x ∈ closure (iSup fun s => iSup fun h => s.toSubmodule).carrier$$

Lean4

@[simp, norm_cast]
theorem coe_iSup (f : ι → ClosedSubmodule R N) : ↑(⨆ i, f i) = closure (⨆ i, (f i).toSubmodule).carrier :=
  by
  simp only [← coe_toSubmodule, toSubmodule_iSup, Submodule.carrier_eq_coe]
  rfl

Похожие утверждения