coe_iSup_of_chain — Mathlib

English

If a is a monotone chain of submodules a: ℕ → Submodule R M, then the carrier of the supremum equals the union of the carriers: ↑(⨆ k, a k) = ⋃ k, (a k).

Русский

Если а: ℕ → Submodule R M является монотончной цепочкой подмодулов, то носитель их супремума равен объединению носителей: ↑(⨆ k, a k) = ⋃ k, (a k).

LaTeX

$$$$ \\uparrow\\Big(\\big\\vee_{k} a_k\\Big) = \\bigcup_{k} (a_k). $$$$

Lean4

@[norm_cast, simp]
theorem coe_iSup_of_chain (a : ℕ →o Submodule R M) : (↑(⨆ k, a k) : Set M) = ⋃ k, (a k : Set M) :=
  coe_iSup_of_directed a a.monotone.directed_le

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