biInf_mem_of_nonempty — Mathlib

English

Dual to the SupClosed case: a finite inf-closed index yields a contained infimum.

Русский

Двойственно случаю SupClosed: для конечного множества интовых индексов инфимум включён в s.

LaTeX

$$$\\text{Given } hs: \\operatorname{InfClosed}(s),\\ ht: t.Finite,\\ ht': t.Nonempty,\\ hf: \\forall i\\in t, f(i)\\in s,\\text{ then } iInf_{i\\in t} f(i) \\in s.$$$

Lean4

theorem biInf_mem_of_nonempty {ι : Type*} {t : Set ι} {f : ι → α} (hs : InfClosed s) (ht : t.Finite) (ht' : t.Nonempty)
    (hf : ∀ i ∈ t, f i ∈ s) : ⨅ i ∈ t, f i ∈ s :=
  hs.dual.biSup_mem_of_nonempty ht ht' hf

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