Mathlib Map

Theorems · Theorem · order theory

Monotone.comp_antitone

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, Monotone g → Antitone f → Antitone (g ∘ f)
Defined in
Mathlib.Order.Monotone.Defs
Cited by
16 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
PreorderPreorderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Monotone.measure_iInter · cited by 4Monotone.measure_iInterLinearMap.IsSymmetric.eigenvalues_antitone · cited by 3IsSymmetric.eigenvalues_a…Antitone.Iic · cited by 2Antitone.IicAntitone.Iio · cited by 2Antitone.IiocantorSet_eq_union_halves · cited by 1cantorSet_eq_union_halvesBoxIntegral.Box.subbox_induction_on' · cited by 1Box.subbox_induction_on'ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero · cited by 1IsRatCondKernelCDFAux.ten…Antitone.smul_const · cited by 0Antitone.smul_constBoxIntegral.Box.iUnion_Ioo_of_tendsto · cited by 0Box.iUnion_Ioo_of_tendstoAntitone.add_const · cited by 0Antitone.add_constAntitone.mul_const · cited by 0Antitone.mul_constAntitone.mul_const' · cited by 0Antitone.mul_const'Antitone.const_add · cited by 0Antitone.const_addAntitone.const_mul · cited by 0Antitone.const_mulAntitone.const_mul' · cited by 0Antitone.const_mul'Preorder · cited by 7952PreorderMonotone · cited by 1397MonotoneAntitone · cited by 563AntitoneMonotone.comp_antitoneCITED BYCITES

Cites3

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

  • Preorderstatement and proof · cited by 7,952
  • Monotonestatement and proof · cited by 1,397
  • Antitonestatement and proof · cited by 563

Cited by16

Results whose statement or proof uses this declaration.