Theorems · Theorem · order theory
Antitone.dual_left
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → Monotone (f ∘ ⇑OrderDual.ofDual)Alias of the reverse direction of monotone_comp_ofDual_iff.
- Defined in
- Mathlib.Order.Monotone.Basic
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement · cited by 8,337
- Preorderstatement and proof · cited by 7,952
- Monotonestatement · cited by 1,397
- OrderDualstatement · cited by 927
- Antitonestatement · cited by 563
- OrderDual.ofDualstatement · cited by 400
- monotone_comp_ofDual_iffproof · cited by 3
Cited by33
Results whose statement or proof uses this declaration.
- iInf_iSup_of_antitoneproof · cited by 2
- Antitone.measure_iInterproof · cited by 2
- Antitone.ciSup_comp_tendsto_atBotproof · cited by 2
- iSup_iInf_of_antitoneproof · cited by 2
- iSup_inf_of_antitoneproof · cited by 1
- iInf_sup_of_antitoneproof · cited by 1
- isGLB_of_tendsto_atTopproof · cited by 1
- MeasureTheory.tendsto_measure_iUnion_atBotproof · cited by 1
- tendsto_atBot_isLUBproof · cited by 1
- MeasureTheory.measure_iInter_of_ae_antitoneproof · cited by 0
- Set.Finite.iInf_biSup_of_antitoneproof · cited by 0
- Set.Finite.iSup_biInf_of_antitoneproof · cited by 0