BddAbove.range_comp

Deprecated since 2026-06-07Use BddAbove.range_comp_left instead.

∀ {α : 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))

Alias of BddAbove.range_comp_left.

Defined in: Mathlib.Order.Bounds.Image
Cited by: 0 results in Mathlib
Foundations: Depth 11 from the axioms · uses propext, Quot.sound
Assumes: Preorder Preorder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Preorderstatement · cited by 7,952
Set.rangestatement · cited by 4,705
Monotonestatement · cited by 1,397
BddAbovestatement · cited by 620
BddAbove.range_comp_leftproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.