Theorems · Theorem · order theory

strictMono_of_odd_strictMonoOn_nonneg

∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup H] [inst_4 : PartialOrder H] [IsOrderedAddMonoid H] {f : G → H},
  (∀ (x : G), f (-x) = -f x) → StrictMonoOn f (Set.Ici 0) → StrictMono f

An odd function on a linear ordered additive commutative group is strictly monotone on the whole group provided that it is strictly monotone on Set.Ici 0.

Defined in

Mathlib.Order.Monotone.Odd

Cited by

2 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidAddCommGroupPartialOrderIsOrderedAddMonoid