Theorems · Theorem · order theory

Monotone.le_csSup_image

∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] [inst_1 : Preorder α] {f : α → β},
  Monotone f → ∀ {s : Set α} {c : α}, c ∈ s → BddAbove s → f c ≤ sSup (f '' s)

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLatticePreorder