OrderAddMonoidHom.monotone'
theorem OrderAddMonoidHom.monotone' :
∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
[inst_3 : AddZeroClass β] (self : α →+o β), Monotone self.toFun
The theorem `OrderAddMonoidHom.monotone'` states that for any types `α` and `β` with both a preorder and an AddZeroClass structure, any function that is an `OrderAddMonoidHom` (an additive monoid homomorphism that preserves ordering) from `α` to `β` is monotone. In other words, if `a` and `b` are elements of `α` such that `a ≤ b`, then the image of `a` under the function is less than or equal to the image of `b`. This theorem captures the notion that an order-preserving additive monoid homomorphism respects the order of the original set.
More concisely: If `f` is an OrderAddMonoidHom from a preordered type `α` with AddZeroClass structure to a preordered type `β` with AddZeroClass structure, then `a ≤ b` implies `f a ≤ f b`.
|
OrderAddMonoidHom.ext
theorem OrderAddMonoidHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
[inst_3 : AddZeroClass β] {f g : α →+o β}, (∀ (a : α), f a = g a) → f = g
This theorem, titled `OrderAddMonoidHom.ext`, states that for any two order-preserving additive monoid homomorphisms `f` and `g` from a preordered additive monoid `α` to another preordered additive monoid `β`, if for every element 'a' in `α`, the result of applying `f` to 'a' is equal to the result of applying `g` to 'a', then `f` and `g` are the same homomorphism. This is essentially a uniqueness property, asserting that two such homomorphisms are uniquely determined by their action on elements of `α`.
More concisely: If two order-preserving additive homomorphisms from a preordered additive monoid to another with the same action on elements agree on all elements, then they are equal.
|
OrderMonoidWithZeroHom.ext
theorem OrderMonoidWithZeroHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
[inst_3 : MulZeroOneClass β] {f g : α →*₀o β}, (∀ (a : α), f a = g a) → f = g
This theorem states that for any two order-preserving monoid homomorphisms `f` and `g` from a preorder `α` to a preorder `β` (where `α` and `β` are additionally equipped with multiplication, zero and one), if `f` and `g` are equal for all elements of `α`, then `f` and `g` are identical functions. In other words, two such homomorphisms are considered identical if they map each element of `α` to the same element in `β`.
More concisely: If two order-preserving monoid homomorphisms from a preordered monoid to another with multiplication, zero, and one agree on all elements, then they are equal as functions.
|
OrderMonoidHom.ext
theorem OrderMonoidHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
[inst_3 : MulOneClass β] {f g : α →*o β}, (∀ (a : α), f a = g a) → f = g
This theorem, `OrderMonoidHom.ext`, asserts that for any two ordered monoid homomorphisms `f` and `g` from a preordered `mul_one_class` α to another preordered `mul_one_class` β, if for every element `a` in α, `f(a)` equals `g(a)`, then `f` and `g` are the same function. In simpler terms, it states that two monoid homomorphisms are equal if they give the same result for every input.
More concisely: Two ordered monoid homomorphisms between preordered mul_one_classes are equal if they map each element to the same image.
|
OrderMonoidWithZeroHom.monotone'
theorem OrderMonoidWithZeroHom.monotone' :
∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
[inst_3 : MulZeroOneClass β] (self : α →*₀o β), Monotone self.toFun
The theorem `OrderMonoidWithZeroHom.monotone'` states that for any types `α` and `β`, given that `α` and `β` are both preordered and each is a multiplication zero one class (a structure with a multiplication operation, a zero, and a one such that multiplication is associative, one is a multiplicative identity, and zero is a multiplicative annihilator), then any function `self` from `α` to `β` that is an order monoid with zero homomorphism is a monotone function. In other words, if `a` and `b` are elements of `α` and `a ≤ b`, then `self(a) ≤ self(b)`. This theorem guarantees that order monoid with zero homomorphisms preserve the order structure of their domain.
More concisely: Given types `α` and `β` with preordered multiplication zero one classes, any order monoid with zero homomorphism from `α` to `β` is a monotone function.
|
OrderMonoidHom.monotone'
theorem OrderMonoidHom.monotone' :
∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
[inst_3 : MulOneClass β] (self : α →*o β), Monotone self.toFun
The theorem `OrderMonoidHom.monotone'` states that for any ordered monoid homomorphism function, denoted as `self`, from a preordered type `α` to another preordered type `β`, which also have multiplication and identity element (`MulOneClass`), this function is monotone. In other words, if `a` and `b` are elements of type `α` such that `a` is less than or equal to `b`, then the result of applying the `self` function to `a` is less than or equal to the result of applying `self` to `b`.
More concisely: For any ordered monoid homomorphism `self` from a preordered type `α` to another preordered type `β` with multiplication and identity element, `self(a) ≤ self(b)` whenever `a ≤ b` in `α`.
|
monotone_iff_map_nonneg
theorem monotone_iff_map_nonneg :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommMonoid β]
[i : FunLike F α β] [iamhc : AddMonoidHomClass F α β] (f : F), Monotone ⇑f ↔ ∀ (a : α), 0 ≤ a → 0 ≤ f a
The theorem `monotone_iff_map_nonneg` establishes an equivalence between two properties of a function `f` of type `F`, which has an injective coercion to a function from type `α` to `β`. The theorem states that, given an ordered additive commutative group `α` and an ordered additive commutative monoid `β`, the function `f` is monotone (i.e., for all `a` and `b` in `α`, if `a` is less than or equal to `b` then `f(a)` is less than or equal to `f(b)`) if and only if for all `a` in `α`, if `a` is nonnegative (greater than or equal to zero) then `f(a)` is also nonnegative. The theorem thereby provides a characterization of monotonicity in terms of nonnegativity preservation.
More concisely: A function `f` from an ordered additive commutative group to an ordered additive commutative monoid is monotone if and only if for all non-negative elements `a` in the domain of `f`, `f(a)` is also non-negative.
|