ciSup_le' — Mathlib

English

Let s : ι → α. If s is bounded above, then a ≤ iSup s iff ∀ b, (∀ i, s i ≤ b) → a ≤ b.

Русский

Пусть s : ι → α. При условии ограниченности сверху: a ≤ iSup s эквивалентно ∀ b, если b верхняя граница множества {s i}, то a ≤ b.

LaTeX

$$$ a \le iSup s \iff \forall b, (\forall i, s(i) \le b) \rightarrow a \le b $$$

Lean4

theorem ciSup_le' {f : ι → α} {a : α} (h : ∀ i, f i ≤ a) : ⨆ i, f i ≤ a :=
  csSup_le' <| forall_mem_range.2 h

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