le_ciSup — Mathlib

English

Let f: ι → α with α a ConditionallyCompleteLattice and c ∈ ι. Then f(c) ≤ iSup f; i.e., every indexed value is ≤ the supremum.

Русский

Пусть f: ι → α. Тогда для любого индекса c выполняется f(c) ≤ iSup f.

LaTeX

$$f(c) ≤ iSup f$$

Lean4

/-- The indexed supremum of a function is bounded below by the value taken at one point -/
theorem le_ciSup {f : ι → α} (H : BddAbove (range f)) (c : ι) : f c ≤ iSup f :=
  le_csSup H (mem_range_self _)

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