biSup_mem — Mathlib

English

In a complete lattice, if s is sup-closed and every f(i) ∈ s for i ∈ t with t finite, then the iSup over i ∈ t lies in s.

Русский

В полной решётке, если s суп-замкнуто и все f(i) ∈ s, то iSup по i ∈ t принадлежит s.

LaTeX

$$$\\text{SupClosed}(s) \\land t.Finite \\land (\\forall i \\in t, f(i) \\in s) \\Rightarrow (\\\\iSup_{i \\in t} f(i)) \\in s.$$$

Lean4

theorem biSup_mem {ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s) (ht : t.Finite) (hbot : ⊥ ∈ s)
    (hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i ∈ s := by
  rw [← sSup_image]
  exact hs.sSup_mem (ht.image _) hbot (by simpa)

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