toSubmodule_iSup — Mathlib

English

The toSubmodule of the supremum over an indexed family equals the closure of the supremum of the corresponding submodules.

Русский

toSubmodule(⨆ i, f i) равен замыканию надмодуля ⨆ i (f i).toSubmodule.

LaTeX

$$$toSubmodule\left(\bigvee_i f(i)\right) = (\bigvee_i (f(i).toSubmodule)).closure.toSubmodule$$$

Lean4

@[simp]
theorem toSubmodule_iSup (f : ι → ClosedSubmodule R N) : toSubmodule (⨆ i, f i) = (⨆ i, (f i).toSubmodule).closure := by
  rw [iSup, toSubmodule_sSup, iSup_range]

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