Theorems · Definition · order theory

MonovaryOn

{ι : Type u_1} → {α : Type u_3} → {β : Type u_4} → [Preorder α] → [Preorder β] → (ι → α) → (ι → β) → Set ι → Prop

f monovaries with g on s if g i < g j implies f i ≤ f j for all i, j ∈ s.

Defined in

Mathlib.Order.Monotone.Monovary

Cited by

139 results in Mathlib

Foundations

Depth 4 from the axioms, rests on 14 definitions · uses no axioms

Assumes

PreorderPreorder