supClosed_sInter

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#supClosed_sInter

English

If every member s in S is sup-closed, then the intersection ⋂ S is sup-closed.

Русский

Если каждый элемент множества S суп-замкнут, то ⋂ S суп-замкнуто.

LaTeX

$$$$ (\forall s \in S, \operatorname{supClosed}(s)) \rightarrow \operatorname{supClosed}(\bigcap S) $$$$

Lean4

theorem supClosed_sInter (hS : ∀ s ∈ S, SupClosed s) : SupClosed (⋂₀ S) := fun _a ha _b hb _s hs ↦
  hS _ hs (ha _ hs) (hb _ hs)

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

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

Разделы

Аффилиация

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