sSup_mem — Mathlib

English

If s is sup-independent and t ⊆ s and ⊥ ∈ s with f(i) ∈ s for i ∈ t, then s is closed under sup over i ∈ t.

Русский

Если s является SupIndep и t ⊆ s, а ⊥ ∈ s и все f(i) ∈ s, то sup по i ∈ t принадлежит s.

LaTeX

$$$\\text{SupIndep}(s) \\land t ⊆ s \\land ⊥ \\in s \\Rightarrow sSup_{i\\in t} f(i) \\in s.$$$

Lean4

theorem sSup_mem (hs : SupClosed s) (ht : t.Finite) (hbot : ⊥ ∈ s) (hts : t ⊆ s) : sSup t ∈ s :=
  by
  have := ht.to_subtype
  rw [sSup_eq_iSup']
  exact hs.iSup_mem hbot (by simpa)

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