mem_iSup — Mathlib

English

For a family p: ι → Submodule, an element m ∈ ⨆ i, p i iff m ∈ N for all N with p i ≤ N for all i.

Русский

Для семейства p: ι → подмодуль, элемент m принадлежит ⨆ i, p i тогда и только тогда, когда m принадлежит любому N, для которого p i ≤ N для всех i.

LaTeX

$$$m \in \big\vee_i p_i \iff \forall N, (\forall i, p_i \le N) \to m \in N$$$

Lean4

theorem mem_iSup {ι : Sort*} (p : ι → Submodule R M) {m : M} : (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N :=
  by
  rw [← span_singleton_le_iff_mem, le_iSup_iff]
  simp only [span_singleton_le_iff_mem]

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