isBoundedUnder_ge_finset_inf — Mathlib

English

For a linear order, if every F_i is bounded above, the infimum over a Finset s is bounded below (≥) along the filter.

Русский

Для линейного порядка, если каждый F_i ограничен сверху, инфимум по Finset s ограничен снизу вдоль фильтра.

LaTeX

$$[LinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h : ∀ i ∈ s, f.IsBoundedUnder (≥) (F i)) : f.IsBoundedUnder (≥) (fun a ↦ inf s (fun i ↦ F i a))$$

Lean4

theorem isBoundedUnder_ge_finset_inf [LinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
    (h : ∀ i ∈ s, f.IsBoundedUnder (· ≥ ·) (F i)) : f.IsBoundedUnder (· ≥ ·) (fun a ↦ inf s (fun i ↦ F i a)) :=
  isBoundedUnder_le_finset_sup (β := βᵒᵈ) h

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