isCoboundedUnder_ge_finset_inf' — Mathlib

English

If there exists an i ∈ s with F_i cobounded above, then the finite infimum inf' s hs (F i a) is cobounded above.

Русский

Если существует i ∈ s такое, что F_i кобounded выше, то инфимум над финитным множеством инф' s hs (F i a) кобounded выше.

LaTeX

$$$\text{hs: } s.\Nonempty \Rightarrow f.IsCoboundedUnder(≤)(inf' s hs (\lambda i. F i a))$$$

Lean4

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

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