mem_iSup — Mathlib

English

An element x lies in the iSup of a family if and only if x lies in the closure of the iSup of their submodules.

Русский

Элемент x принадлежит iSup семейства тогда и только тогда, когда x принадлежит замыканию iSup соответствующих подмодулей.

LaTeX

$$"@[simp] theorem mem_iSup {f : ι → ClosedSubmodule R N} : x ∈ ⨆ i, f i ↔ x ∈ closure (⨆ i, (f i).toSubmodule).carrier"$$

Lean4

@[simp]
theorem mem_iSup {f : ι → ClosedSubmodule R N} : x ∈ ⨆ i, f i ↔ x ∈ closure (⨆ i, (f i).toSubmodule).carrier := by
  simp [← SetLike.mem_coe]

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