ciSup_le_iff — Mathlib

English

For a nonempty set s and a bounded above f, ⨆ i∈s, f(i) ≤ a iff ∀ i∈s, f(i) ≤ a.

Русский

Для непустого множества s и ограниченной сверху функции f: ⨆ i∈s f(i) ≤ a тогда и только тогда, когда ∀ i∈s, f(i) ≤ a.

LaTeX

$$$\displaystyle \bigvee_{i\in s} f(i) \le a \quad\iff\quad \forall i\in s,\ f(i) \le a$$$

Lean4

theorem ciSup_le_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddAbove (range f)) : iSup f ≤ a ↔ ∀ i, f i ≤ a :=
  (isLUB_le_iff <| isLUB_ciSup hf).trans forall_mem_range

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