mem_sSup_of_directed — Mathlib

English

Let s be a nonempty set of submodules of M, directed under inclusion. Then z ∈ sSup s if and only if there exists y ∈ s with z ∈ y.

Русский

Пусть s — непустое множество подмодулей пространства M, упорядоченное по включению и направленное. Тогда z принадлежит sSup s тогда, когда существует y ∈ s такое, что z ∈ y.

LaTeX

$$$$ z \\in sSup\\,s \\;\\iff\\; \\exists y \\in s,\\ z \\in y. $$$$

Lean4

theorem mem_sSup_of_directed {s : Set (Submodule R M)} {z} (hs : s.Nonempty) (hdir : DirectedOn (· ≤ ·) s) :
    z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y := by
  have : Nonempty s := hs.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists, exists_prop]

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