sInf_mem_of_nonempty — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sInf_mem_of_nonempty (hs : InfClosed s) (ht : t.Finite) (ht' : t.Nonempty) (hts : t ⊆ s) : sInf t ∈ s :=
  hs.dual.sSup_mem_of_nonempty ht ht' hts

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