antitone_of_odd_of_monotoneOn_nonneg
theorem antitone_of_odd_of_monotoneOn_nonneg :
∀ {G : Type u_1} {H : Type u_2} [inst : LinearOrderedAddCommGroup G] [inst_1 : OrderedAddCommGroup H] {f : G → H},
(∀ (x : G), f (-x) = -f x) → AntitoneOn f (Set.Ici 0) → Antitone f
This theorem states that for any odd function `f` mapping from a linear ordered additive commutative group `G` to another ordered additive commutative group `H`, if the function `f` is monotone (non-decreasing) on the half-open interval from 0 to infinity in `G`, then the function `f` is antitone (non-increasing) on the whole group `G`. Here, an odd function is defined as a function `f` for which `f(-x)` equals `-f(x)` for all `x` in the domain, and an antitone function is one that reverses the order: if `a ≤ b` then `f(b) ≤ f(a)`.
More concisely: If `f` is an odd function mapping from an ordered additive commutative group to another such group and is monotone on the half-open interval from 0 to infinity, then `f` is antitone on the entire group.
|
strictAnti_of_odd_strictAntiOn_nonneg
theorem strictAnti_of_odd_strictAntiOn_nonneg :
∀ {G : Type u_1} {H : Type u_2} [inst : LinearOrderedAddCommGroup G] [inst_1 : OrderedAddCommGroup H] {f : G → H},
(∀ (x : G), f (-x) = -f x) → StrictAntiOn f (Set.Ici 0) → StrictAnti f
This theorem states that for any odd function `f` from a group `G` to a group `H`, where `G` is a linear ordered additive commutative group and `H` is an ordered additive commutative group, if the function `f` is strictly decreasing on the interval that includes all numbers greater than or equal to zero (denoted as `Set.Ici 0`), then `f` is strictly decreasing on the entire group `G`. Here, an odd function is defined as a function such that for every `x` in `G`, `f(-x) = -f(x)`, and a strictly decreasing function is one that for any two elements `a` and `b` from the set, if `a < b`, then `f(b) < f(a)`.
More concisely: If `f` is an odd function from a linear ordered additive commutative group `G` to another linear ordered additive commutative group `H`, and `f` is strictly decreasing on the interval `Set.Ici 0`, then `f` is strictly decreasing on the entire group `G`.
|
monotone_of_odd_of_monotoneOn_nonneg
theorem monotone_of_odd_of_monotoneOn_nonneg :
∀ {G : Type u_1} {H : Type u_2} [inst : LinearOrderedAddCommGroup G] [inst_1 : OrderedAddCommGroup H] {f : G → H},
(∀ (x : G), f (-x) = -f x) → MonotoneOn f (Set.Ici 0) → Monotone f
The theorem `monotone_of_odd_of_monotoneOn_nonneg` asserts that for any odd function `f` mapping from a linearly ordered additive commutative group `G` to an ordered additive commutative group `H`, if `f` is monotone on the left-closed right-infinite interval starting from `0` (denoted by `Set.Ici 0`), then `f` is monotone on the whole group `G`. In mathematical terms, this means if `f` satisfies `f(-x) = -f(x)` for all `x` in `G`, and for all `a, b` in `Set.Ici 0`, `a ≤ b` implies `f(a) ≤ f(b)`, then for any `a, b` in `G`, `a ≤ b` implies `f(a) ≤ f(b)`.
More concisely: If an odd function `f` is monotone on the left-closed right-infinite interval of an additive commutative group and satisfies `f(-x) = -f(x)`, then `f` is monotone on the entire group.
|
strictMono_of_odd_strictMonoOn_nonneg
theorem strictMono_of_odd_strictMonoOn_nonneg :
∀ {G : Type u_1} {H : Type u_2} [inst : LinearOrderedAddCommGroup G] [inst_1 : OrderedAddCommGroup H] {f : G → H},
(∀ (x : G), f (-x) = -f x) → StrictMonoOn f (Set.Ici 0) → StrictMono f
The theorem `strictMono_of_odd_strictMonoOn_nonneg` states that for any linear ordered additive commutative group `G` and any ordered additive commutative group `H`, if we have a function `f` from `G` to `H` that is odd (i.e., for all `x` in `G`, `f(-x)` equals `-f(x)`), and this function `f` is strictly monotone on the interval `Set.Ici 0` (i.e., the set of all `x` in `G` such that `0 <= x`), then `f` is strictly monotone on the whole group `G`. In other words, if `a` and `b` are elements of `G` such that `a < b`, then `f(a) < f(b)`. This theorem thus establishes a condition under which an odd function on a group is strictly monotone.
More concisely: If `f` is an odd function from a linear ordered additive commutative group `G` that is strictly monotone on the non-negative part `Set.Ici 0`, then `f` is strictly monotone on the entire group `G`.
|