mem_iSup_of_directed — Mathlib

English

For a directed family S : ι → Submodule R M, and x ∈ M, x ∈ iSup S if and only if there exists i with x ∈ S i.

Русский

Для направленной семейной функции S: ι → Submodule R M выполняется: x принадлежит iSup S тогда и только тогда, когда существует индекс i такой, что x ∈ S_i.

LaTeX

$$$$ x \\in iSup S \\;\\iff\\; \\exists i, x \\in S(i). $$$$

Lean4

@[simp]
theorem mem_iSup_of_directed {ι} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (· ≤ ·) S) {x} :
    x ∈ iSup S ↔ ∃ i, x ∈ S i :=
  by
  rw [← SetLike.mem_coe, coe_iSup_of_directed S H, mem_iUnion]
  rfl

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