mem_iSup_of_chain

Mathlib.LinearAlgebra.Span.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.mem_iSup_of_chain

English

For a chain a: ℕ → Submodule R M, and m ∈ M, we have m ∈ ⨆ k, a k iff ∃ k, m ∈ a k.

Русский

Для цепи a: ℕ → Submodule R M выполняется: m ∈ ⨆ k, a k ⇔ ∃ k, m ∈ a k.

LaTeX

$$$$ m \\in \\iSup_{k} a_k \\;\\iff\\; \\exists k, m \\in a_k. $$$$

Lean4

@[simp]
theorem mem_iSup_of_chain (a : ℕ →o Submodule R M) (m : M) : (m ∈ ⨆ k, a k) ↔ ∃ k, m ∈ a k :=
  mem_iSup_of_directed a a.monotone.directed_le

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru