Theorems · Definition · order theory
AntitoneOn
{α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Set α → PropA function f is antitone on s if, for all a, b ∈ s, a ≤ b implies f b ≤ f a.
- Defined in
- Mathlib.Order.Monotone.Defs
- Cited by
- 266 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 11 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by266
Results whose statement or proof uses this declaration.
- AntitoneOn.dual_rightstatement · cited by 29
- antitoneOn_of_deriv_nonposstatement · cited by 25
- Antitone.antitoneOnstatement · cited by 21
- AntitoneOn.monostatement and proof · cited by 9
- AntitoneOn.negstatement and proof · cited by 8
- MonotoneOn.negstatement · cited by 8
- StrictAntiOn.antitoneOnstatement · cited by 6
- antitoneOn_iff_forall_ltstatement and proof · cited by 6
- Monotone.comp_antitoneOnstatement and proof · cited by 6
- AntitoneOn.dual_leftstatement · cited by 4
- AntitoneOn.interstatement and proof · cited by 4
- Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Icistatement and proof · cited by 3
Showing the 200 most cited of 266.