Theorems · Theorem · order theory

BddAbove.range_comp_left

∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {g : β → γ},
  BddAbove (Set.range f) → Monotone g → BddAbove (Set.range fun x => g (f x))

Defined in

Mathlib.Order.Bounds.Image

Cited by

3 results in Mathlib

Foundations

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

Assumes

PreorderPreorder