le_ciSup_iff' — Mathlib

English

Let f : ι → α and a ∈ α with BddAbove (range f). Then a ≤ iSup f iff ∀ i, f i ≤ a.

Русский

Пусть f : ι → α и a ∈ α, при условии, что диапазон f ограничен сверху, тогда a ≤ iSup f тогда и только если для всех i выполняется f(i) ≤ a.

LaTeX

$$"$$ a \le iSup f \iff \forall i, f(i) \le a $$" (при BddAbove (range f))$$

Lean4

theorem le_ciSup_iff' {s : ι → α} {a : α} (h : BddAbove (range s)) : a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b := by
  simp [iSup, h, le_csSup_iff', upperBounds]

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