supClosed_iInter

Mathlib.Order.SupClosed

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

English

If each f(i) is sup-closed, then the intersection over i is sup-closed.

Русский

Если каждый f(i) sup-замкнут, то ⋂ i f(i) sup-замкнуто.

LaTeX

$$$$ (\forall i, \operatorname{supClosed}(f(i))) \rightarrow \operatorname{supClosed}(\bigcap_i f(i)) $$$$

Lean4

theorem supClosed_iInter (hf : ∀ i, SupClosed (f i)) : SupClosed (⋂ i, f i) :=
  supClosed_sInter <| forall_mem_range.2 hf

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

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

Разделы

Аффилиация

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