biInf_mem — Mathlib

English

Dual to SupClosed.biSup_mem: the iInf over a finite index set lies in s when each f(i) ∈ s.

Русский

Дуал к SupClosed.biSup_mem: инфимум по конечному множеству индексов принадлежит s, если каждый f(i) ∈ s.

LaTeX

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

Lean4

theorem biInf_mem {ι : Type*} {t : Set ι} {f : ι → α} (hs : InfClosed s) (ht : t.Finite) (htop : ⊤ ∈ s)
    (hf : ∀ i ∈ t, f i ∈ s) : ⨅ i ∈ t, f i ∈ s :=
  hs.dual.biSup_mem ht htop hf

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