isBoundedUnder_ge_finset_inf' — Mathlib

English

For a linear order with top, the infimum over a finite set of functions is bounded above when each function is bounded above.

Русский

Для линейного порядка с верхой верхней границей инфимум над конечным набором функций ограничен сверху при условии, что каждая функция ограничена сверху.

LaTeX

$$$\forall i \in s,\; f.IsBoundedUnder(≤)(F i) \Rightarrow f.IsBoundedUnder(≤)(\lambda a. inf s (\lambda i. F i a))$$$

Lean4

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

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