mem_iSup_of_mem

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.mem_iSup_of_mem

English

If b ∈ N i for some i, then b ∈ ⨆ i, N i.

Русский

Если b ∈ N_i для некоторого i, то b ∈ ⨆ i, N_i.

LaTeX

$$$b \in N_i \;\Rightarrow\; b \in \big\lceil\,\big\lbrace N_j \mid j \rbrace\rceil$$$

Lean4

theorem mem_iSup_of_mem {ι} {b : M} {N : ι → LieSubmodule R L M} (i : ι) (h : b ∈ N i) : b ∈ ⨆ i, N i :=
  (le_iSup N i) h

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

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

Разделы

Аффилиация

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