Theorems · Theorem · order theory

ciSup_le

∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {c : α},
  (∀ (x : ι), f x ≤ c) → iSup f ≤ c

The indexed supremum of a function is bounded above by a uniform bound

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Indexed

Cited by

56 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Quot.sound

Assumes

ConditionallyCompleteLatticeNonempty