sInf_mem

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#InfClosed.sInf_mem

English

Dual of SupClosed biInf_mem_of_nonempty: lower bounds of a finite index set lie in s.

Русский

Дуал к предыдущему: для конечного множества индексов нижние границы принадлежат s.

LaTeX

$$$\\text{InfClosed}(s) \\Rightarrow \\text{biInfMem}(s).$$$$

Lean4

theorem sInf_mem (hs : InfClosed s) (ht : t.Finite) (htop : ⊤ ∈ s) (hts : t ⊆ s) : sInf t ∈ s :=
  hs.dual.sSup_mem ht htop hts

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru