le_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 α (\le)] [Finite β] \Rightarrow IsBoundedUnder (\le) f u $$$

Lean4

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

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