coe_sSup — Mathlib

English

The underlying set of sSup equals the closure of the supremum of submodules.

Русский

Носитель sSup равен замыканию супа подмодулей.

LaTeX

$$$\uparrow(sSup(S)) = closure (\bigvee_{s\in S} s.toSubmodule).carrier$$$

Lean4

@[simp, norm_cast]
theorem coe_sSup (S : Set (ClosedSubmodule R N)) : ↑(sSup S) = closure (⨆ s ∈ S, s.toSubmodule).carrier :=
  by
  simp only [← coe_toSubmodule, toSubmodule_sSup]
  simp only [coe_toSubmodule, Submodule.coe_closure, Submodule.carrier_eq_coe]

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