sSup_mem_of_nonempty — Mathlib

English

If s is sup-closed and t is a finite, nonempty subset with t ⊆ s, then sSup t ∈ s.

Русский

Если s — sup-замкнутое множество, и t — конечное ненулевое подмножество, содержащееся в s, то sSup t принадлежит s.

LaTeX

$$$\\text{If } hs: \\operatorname{supClosed}(s),\\ ht: t\\text{ finite},\\ ht': t \\neq \\varnothing,\\ hts: t \\subseteq s, \\text{ then } sSup(t) \\in s.$$$

Lean4

theorem sSup_mem_of_nonempty (hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty) (hts : t ⊆ s) : sSup t ∈ s :=
  by
  have := ht.to_subtype
  have := ht'.to_subtype
  rw [sSup_eq_iSup']
  exact hs.iSup_mem_of_nonempty (by simpa)

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