Theorems · Theorem · order theory

Monotone.csInf_image_le

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

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLatticePreorder