ge_of_finite — Mathlib

English

If α is nonempty, directed under ≥, and β is finite, then for any f : Filter β and u : β → α, IsBoundedUnder (≥) f u.

Русский

Пусть α непусто и направлено относительно ≥, β конечно; тогда для любого фильтра f на β и отображения u: β → α, u ограничен снизу по ≥ вдоль f.

LaTeX

$$$ [Nonempty α] [IsDirected α (\ge)] [Finite β] \Rightarrow IsBoundedUnder (\ge) f u $$$

Lean4

theorem ge_of_finite [Nonempty α] [IsDirected α (· ≥ ·)] [Finite β] {f : Filter β} {u : β → α} :
    IsBoundedUnder (· ≥ ·) f u :=
  (Set.toFinite _).bddBelow.isBoundedUnder_of_range

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