exists_le — Mathlib

English

Assume the index set is directed under ≤ and f: β → α. Then there exists M ∈ α such that f(i) ≤ M for all i ∈ β.

Русский

Пусть множество индексов ориентировано относительно отношения ≤ и дана функция f: β → α. Тогда существует M ∈ α such that f(i) ≤ M для всех i.

LaTeX

$$$\\\\exists M \\\\in \\\\alpha, \\\\forall i, \\\\ f(i) \\\\le M.$$$

Lean4

theorem exists_le [IsDirected α (· ≤ ·)] (f : β → α) : ∃ M, ∀ i, f i ≤ M :=
  directed_id.finite_le _

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