le_ciSup_of_le — Mathlib

English

Let f: ι → α with α a ConditionallyCompleteLattice and H: BddAbove (range f). If a ≤ f(c), then a ≤ iSup f for any c.

Русский

Пусть f: ι → α и a ≤ f(c). Если множество значений range f сверху ограничено, то a ≤ iSup f.

LaTeX

$$BddAbove((range f)) → (a ≤ f(c) → a ≤ iSup f)$$

Lean4

theorem le_ciSup_of_le {f : ι → α} (H : BddAbove (range f)) (c : ι) (h : a ≤ f c) : a ≤ iSup f :=
  le_trans h (le_ciSup H c)

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