exists_forall_le — Mathlib

English

If β is a directed preorder with a nonempty β, then every simple function has an upper bound C with f(x) ≤ C for all x.

Русский

Пусть β упорядоченное по направлению множество, не пустое; тогда для каждой простой функции найдётся общий верхний предел C, такой что f(x) ≤ C для всех x.

LaTeX

$$$\\exists C, \\forall x, f(x) \\le C$$$

Lean4

theorem exists_forall_le [Nonempty β] [Preorder β] [IsDirected β (· ≤ ·)] (f : α →ₛ β) : ∃ C, ∀ x, f x ≤ C :=
  f.range.exists_le.imp fun _ => forall_mem_range.1

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