iInf_mem

Mathlib.Order.SupClosed

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

English

Dual to iSup_mem: if ⊤ ∈ s and all f(i) ∈ s for a finite index set, then iInf f(i) ∈ s.

Русский

Дуал к iSup_mem: если ⊤ ∈ s и все f(i) ∈ s, то iInf f(i) ∈ s.

LaTeX

$$$[Finite ι] \\Rightarrow [\\top ∈ s] ∧ (\\forall i, f(i) ∈ s) \\Rightarrow (\\\\bigwedge_i f(i) ∈ s).$$$

Lean4

theorem iInf_mem [Finite ι] (hs : InfClosed s) (htop : ⊤ ∈ s) (hf : ∀ i, f i ∈ s) : ⨅ i, f i ∈ s :=
  hs.dual.iSup_mem htop hf

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

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

Разделы

Аффилиация

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