ciSup_le — Mathlib

English

Let f: ι → α with α a ConditionallyCompleteLattice and c ∈ α. If f is bounded above by c (i.e., f(x) ≤ c for all x), then the indexed supremum iSup f is ≤ c.

Русский

Пусть f: ι → α, где α — условно полная решетка, и задано верхнее ограничение c. Если для всех x выполняется f(x) ≤ c, то $\iSup f ≤ c$.

LaTeX

$$$(\forall x, f(x) \le c) \implies iSup f \le c.$$$

Lean4

/-- The indexed supremum of a function is bounded above by a uniform bound -/
theorem ciSup_le [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, f x ≤ c) : iSup f ≤ c :=
  csSup_le (range_nonempty f) (by rwa [forall_mem_range])

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