Theorems · Theorem · order theory
Monotone.add_const
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [AddRightMono α],
Monotone f → ∀ (a : α), Monotone fun x => f x + a- Cited by
- 7 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
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 and proof · cited by 7,952
- Monotonestatement and proof · cited by 1,397
- AddRightMonostatement and proof · cited by 367
- Monotone.compproof · cited by 67
- add_left_monoproof · cited by 9
Cited by7
Results whose statement or proof uses this declaration.
- CircleDeg1Lift.le_iterate_of_add_int_le_mapproof · cited by 2
- max_add_add_rightproof · cited by 2
- min_add_add_rightproof · cited by 2
- CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eqproof · cited by 1
- not_summable_indicator_mod_of_antitone_of_negproof · cited by 1
- CircleDeg1Lift.iterate_le_of_map_le_add_intproof · cited by 1
- Nat.monotone_primeCountingproof · cited by 0