ciSup_le_iff' — Mathlib

English

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

Русский

Для f : ι → α и a, если BddAbove(range f), то iSup f ≤ a эквивалентно ∀ i, f(i) ≤ a.

LaTeX

$$$ \big( \sup_{i} f(i) \le a \big) \iff \forall i, f(i) \le a $$$

Lean4

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `ciSup_le_iff`. -/
theorem ciSup_le_iff' {f : ι → α} (h : BddAbove (range f)) {a : α} : ⨆ i, f i ≤ a ↔ ∀ i, f i ≤ a :=
  (csSup_le_iff' h).trans forall_mem_range

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