mem_iSup_of_mem — Mathlib

English

If b ∈ p(i) for some index i, then b ∈ ⨆ i, p(i), i.e., an element belonging to one of the submodules lies in the supremum over all p(i).

Русский

Если b ∈ p(i) для некоторого индекса i, тогда b ∈ ⨆_i p(i), то есть элемент, принадлежащий одному из подмодулей, принадлежит их верхнему объединению.

LaTeX

$$$\\forall i,\\; b \\in p(i) \\Rightarrow b \\in \\bigvee_i p(i)$$$

Lean4

theorem mem_iSup_of_mem {ι : Sort*} {b : M} {p : ι → Submodule R M} (i : ι) (h : b ∈ p i) : b ∈ ⨆ i, p i :=
  (le_iSup p i) h

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