NonarchimedeanHomClass.map_add_le_max
theorem NonarchimedeanHomClass.map_add_le_max :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Add α] [inst_1 : LinearOrder β] [inst_2 : FunLike F α β]
[self : NonarchimedeanHomClass F α β] (f : F) (a b : α), f (a + b) ≤ max (f a) (f b)
This theorem, named `NonarchimedeanHomClass.map_add_le_max`, states that for any types `F`, `α`, and `β`, where `α` has an addition operation, `β` has a linear order, and `F` is a function-like type from `α` to `β`, if `f` is a non-archimedean homomorphism from `F` to `β`, then for any two elements `a` and `b` of type `α`, the image of their sum under `f` is less than or equal to the maximum of the images of `a` and `b` under `f`. In mathematical terms, this can be expressed as $f(a + b) \leq \max(f(a), f(b))$.
More concisely: Given a non-archimedean homomorphism `f` from a type `F` with an additive structure to a type `β` with a linear order, for all elements `a` and `b` in the domain of `F`, `f(a + b) ≤ max(f(a), f(b))`.
|
map_sub_rev
theorem map_sub_rev :
∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α]
[inst_2 : OrderedAddCommMonoid β] [inst_3 : AddGroupSeminormClass F α β] (f : F) (x y : α),
f (x - y) = f (y - x)
The theorem `map_sub_rev` states that for all types `F`, `α`, `β`, given an instance of `FunLike F α β` (which means `F` has an injective coercion to functions from `α` to `β`), an `AddGroup` over `α`, an `OrderedAddCommMonoid` over `β`, and an `AddGroupSeminormClass` over `F`, `α`, and `β`, for any function `f` of type `F` and any elements `x` and `y` of type `α`, applying `f` to the result of subtracting `y` from `x` yields the same result as applying `f` to the result of subtracting `x` from `y`. In other words, `f` preserves the property of negation over the subtraction operation in `α`.
More concisely: For any function `f` in a FunLike structure between AddGroups `α` and `β` with an AddGroupSeminormClass, applying `f` to the difference of two elements is commutative with respect to the subtraction operation.
|
le_map_add_map_sub
theorem le_map_add_map_sub :
∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α]
[inst_2 : AddCommSemigroup β] [inst_3 : LE β] [inst_4 : SubadditiveHomClass F α β] (f : F) (a b : α),
f a ≤ f b + f (a - b)
This theorem, called `le_map_add_map_sub`, states that for any types `F`, `α`, and `β`, given certain conditions, the value of a function `f` (of type `F` which can be injected into a function from `α` to `β`) at `a` is less than or equal to the value of `f` at `b` plus the value of `f` at `a - b`. The conditions are: `F` is a `FunLike` instance from `α` to `β`, `α` is an additive group, `β` is an additive commutative semigroup, `β` has a less than or equal to (`LE`) operation, and `F` is a subadditive homomorphism class from `α` to `β`. In mathematical terms, this theorem expresses the inequality $f(a) \leq f(b) + f(a - b)$ under the given conditions.
More concisely: For any additive group `α`, additive commutative semigroup `β` with an LE operation, and subadditive homomorphism class `F` from `α` to `β`, `F(a) LE F(b) + F(a - b)` for all `a, b` in `α`.
|
map_pos_of_ne_zero
theorem map_pos_of_ne_zero :
∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α]
[inst_2 : LinearOrderedAddCommMonoid β] [inst_3 : AddGroupNormClass F α β] (f : F) {x : α}, x ≠ 0 → 0 < f x
The theorem `map_pos_of_ne_zero` states that for all types `F`, `α`, and `β`, given an instance of `FunLike F α β` (a function-like relationship between `F`, `α`, and `β`), an `AddGroup` instance for `α` (which is a group under addition), a `LinearOrderedAddCommMonoid` instance for `β` (a commutative monoid under addition which is linearly ordered), and an `AddGroupNormClass` instance for `F α β` (a class that relates norms and addition), if we have a function `f` of type `F` and a non-zero element `x` of type `α`, then the mapped value `f x` is greater than 0. In other words, this theorem says when we map a non-zero element from an additive group to a linearly ordered additive commutative monoid using a function that respects norms and addition, the resulting element is positive.
More concisely: Given a function `f : F α → β` between additive groups with respect to `FunLike`, and a non-zero element `x ∈ α`, if `F` is an `AddGroupNormClass` over `α` and `β` is a linearly ordered `AddGroup` and `LinearOrderedAddCommMonoid`, then `f x` is positive.
|
GroupSeminormClass.map_inv_eq_map
theorem GroupSeminormClass.map_inv_eq_map :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Group α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : FunLike F α β] [self : GroupSeminormClass F α β] (f : F) (a : α), f a⁻¹ = f a
The theorem `GroupSeminormClass.map_inv_eq_map` states that for any function `f` of type `F`, where `F` is a type that can be mapped to a function from `α` to `β`, if `α` is a group, `β` is an ordered additive commutative monoid, and `F` satisfies the `GroupSeminormClass` conditions, then applying `f` to the inverse of an element `a` from the group `α` yields the same result as applying `f` to `a` itself. In other words, `f` is invariant under inversion of its argument.
More concisely: For any function `f` from a group `α` to an ordered additive commutative monoid `β`, if `f` satisfies the `GroupSeminormClass` conditions, then `f(a) = f(a^(-1))` for all `a` in `α`.
|
map_sub_le_add
theorem map_sub_le_add :
∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α]
[inst_2 : OrderedAddCommMonoid β] [inst_3 : AddGroupSeminormClass F α β] (f : F) (x y : α),
f (x - y) ≤ f x + f y
The theorem `map_sub_le_add` states that for any types `F`, `α`, and `β`, if `F` is a function-like class from `α` to `β`, `α` is an additive group, `β` is an ordered additive commutative monoid, and there exists an additive group seminorm class from `F`, `α`, and `β`, then for any function `f` of type `F` and any elements `x` and `y` of type `α`, the value of `f` applied to the difference of `x` and `y` is less than or equal to the sum of `f` applied to `x` and `f` applied to `y`. In mathematical terms, this states that for all $f: F$, $x, y: α$, $f(x - y) ≤ f(x) + f(y)$.
More concisely: For any additive group homomorphism $f: F$ from an additive group $\alpha$ to an ordered additive commutative monoid $\beta$ with an additive group seminorm, we have $f(x - y) ≤ f(x) + f(y)$ for all $x, y ∈ α$.
|
le_map_sub_add_map_sub
theorem le_map_sub_add_map_sub :
∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α]
[inst_2 : AddCommSemigroup β] [inst_3 : LE β] [inst_4 : SubadditiveHomClass F α β] (f : F) (a b c : α),
f (a - c) ≤ f (a - b) + f (b - c)
The theorem `le_map_sub_add_map_sub` states that for any types `F`, `α`, `β` where `F` is a function-like from `α` to `β`, `α` is an additive group, `β` is a commutative semigroup with an order relation (`LE`), and `F` is a subadditive homomorphism class from `α` to `β`, then for any function `f : F` and any elements `a`, `b`, `c` of type `α`, the result of mapping `a - c` through `f` is less than or equal to the sum of the results of mapping `a - b` and `b - c` through `f`. In mathematical notation, this could be expressed as $f(a - c) \leq f(a - b) + f(b - c)$.
More concisely: For any subadditive homomorphism class `F` from an additive group `α` to a commutative semigroup `β` with an order relation `LE`, and for any `f : F` and elements `a`, `b`, `c` of type `α`, we have `f(a - c) ≤ f(a - b) + f(b - c)`.
|
AddGroupSeminormClass.map_neg_eq_map
theorem AddGroupSeminormClass.map_neg_eq_map :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : AddGroup α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : FunLike F α β] [self : AddGroupSeminormClass F α β] (f : F) (a : α), f (-a) = f a
The theorem `AddGroupSeminormClass.map_neg_eq_map` states that for all types `F`, `α`, and `β`, given `α` is an additive group, `β` is an ordered additive commutative monoid, and `F` is a type which can be coercively treated as a function from `α` to `β` (i.e., it is `FunLike`), then for any instance of `F` (called `f`) and any element `a` of type `α`, the value of `f` at `-a` (the additive inverse of `a`) is the same as the value of `f` at `a`. In other words, the function `f` is invariant under negation of its argument.
More concisely: For any additive group α, ordered additive commutative monoid β, and FunLike type F from α to β, the function F is invariant under negation, i.e., F(a) = F(-a) for all a in α.
|
MulRingNormClass.eq_zero_of_map_eq_zero
theorem MulRingNormClass.eq_zero_of_map_eq_zero :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : NonAssocRing α] [inst_1 : OrderedSemiring β]
[inst_2 : FunLike F α β] [self : MulRingNormClass F α β] (f : F) {a : α}, f a = 0 → a = 0
The theorem `MulRingNormClass.eq_zero_of_map_eq_zero` states that for all types `F`, `α`, `β`, where `F` is a function-like type from `α` to `β`, `α` is a non-associative ring, and `β` is an ordered semiring, if `f` is a function from F and `a` is an element of `α` such that `f(a)` is zero, then `a` itself must be zero. This theorem is related to the multiplicative ring norm class and is applicable in the context of algebraic structures. It provides a constraint about the kernel of the function `f`.
More concisely: If `f` is a function from a non-associative ring `α` to an ordered semiring `β`, and `f(a) = 0`, then `a = 0`.
|
le_map_div_add_map_div
theorem le_map_div_add_map_div :
∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α]
[inst_2 : AddCommSemigroup β] [inst_3 : LE β] [inst_4 : MulLEAddHomClass F α β] (f : F) (a b c : α),
f (a / c) ≤ f (a / b) + f (b / c)
The theorem `le_map_div_add_map_div` states that for all types `F`, `α`, and `β`, where `F` is a `FunLike` from `α` to `β`, `α` forms a group, `β` forms an additive commutative semigroup and is orderable, and `F` is a multiplication-to-addition homomorphism, the function `f` applied to the division of `a` and `c` (i.e., `f(a/c)`) is less than or equal to the function `f` applied to the division of `a` and `b` (i.e., `f(a/b)`) plus the function `f` applied to the division of `b` and `c` (i.e., `f(b/c)`), for any elements `a`, `b`, and `c` of `α`. In mathematical notation, this is saying that for all `f`, `a`, `b`, and `c`, we have `f(a/c) ≤ f(a/b) + f(b/c)`.
More concisely: For any `FunLike` function `f` from a group `α` to an additive commutative semigroup and orderable type `β`, `f(a/c) ≤ f(a/b) + f(b/c)` for all `a, b, c` in `α`.
|
MulLEAddHomClass.map_mul_le_add
theorem MulLEAddHomClass.map_mul_le_add :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Mul α] [inst_1 : Add β] [inst_2 : LE β]
[inst_3 : FunLike F α β] [self : MulLEAddHomClass F α β] (f : F) (a b : α), f (a * b) ≤ f a + f b
The theorem `MulLEAddHomClass.map_mul_le_add` states that for any types `F`, `α`, and `β`, along with instances of multiplication on `α`, addition on `β`, a less than or equal to relation on `β`, and if `F` is function-like acting from `α` to `β`, and `F` also has a `MulLEAddHomClass` instance, then for any function `f` of type `F` and any elements `a` and `b` of type `α`, the image of the product `a * b` under `f` is less than or equal to the sum of the images of `a` and `b` under `f`. In mathematical terms, this is saying that for the particular structure on `F`, `α`, and `β`, we have the inequality $f(a*b) \leq f(a) + f(b)$. This is a property that might be expected in certain types of "homomorphisms" between algebraic structures.
More concisely: For any function-like `F` from a type `α` to a type `β` with multiplication and addition instances, and a `MulLEAddHomClass` instance, the image of the product of any two elements under `F` is less than or equal to the sum of their images. In mathematical notation, $f(a \cdot b) \leq f(a) + f(b)$.
|
AddGroupNormClass.eq_zero_of_map_eq_zero
theorem AddGroupNormClass.eq_zero_of_map_eq_zero :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : AddGroup α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : FunLike F α β] [self : AddGroupNormClass F α β] (f : F) {a : α}, f a = 0 → a = 0
This theorem states that for any types `F`, `α`, and `β`, if `α` is an additive group, `β` is an ordered additive commutative monoid, `F` is a function-like structure from `α` to `β`, and `F` satisfies the additive group norm property, then for any function `f` of type `F` and any element `a` of `α`, if the result of applying `f` to `a` is zero, then `a` must be zero. In other words, if a function from an additive group to an ordered additive commutative monoid mapped under the additive group norm property sends an element to zero, then that element itself is zero.
More concisely: If `F` is a function-like structure from an additive group `α` to an ordered additive commutative monoid `β`, and `F` satisfies the additive group norm property, then `F a = 0` implies `a = 0`.
|
GroupNormClass.eq_one_of_map_eq_zero
theorem GroupNormClass.eq_one_of_map_eq_zero :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Group α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : FunLike F α β] [self : GroupNormClass F α β] (f : F) {a : α}, f a = 0 → a = 1
The theorem `GroupNormClass.eq_one_of_map_eq_zero` states that for any types `F`, `α`, and `β`, given that `α` forms a group, `β` forms an ordered additive commutative monoid, and `F` is a function-like mapping from `α` to `β` (i.e., instances of `Group α`, `OrderedAddCommMonoid β`, and `FunLike F α β` exist), and assuming the presence of a `GroupNormClass` structure for `F`, `α`, and `β` (i.e., [self : GroupNormClass F α β]), then for any function `f` of type `F` and any element `a` of type `α`, if the function `f` maps `a` to zero in `β` (i.e., `f a = 0`), then `a` must be the identity element of the group `α` (i.e., `a = 1`).
More concisely: If `F` maps the identity element of a group `α` to zero in an ordered additive commutative monoid `β` with a `GroupNormClass` structure, then the identity element is unique and thus `α`'s identity equals `β`'s zero (i.e., `1 = 0` implies `a = 1` for all `a` in `α`).
|
GroupSeminormClass.map_one_eq_zero
theorem GroupSeminormClass.map_one_eq_zero :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Group α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : FunLike F α β] [self : GroupSeminormClass F α β] (f : F), f 1 = 0
The theorem `GroupSeminormClass.map_one_eq_zero` states that for any types `F`, `α`, and `β`, where `α` is a group, `β` is an ordered additive commutative monoid, `F` is a type that has an injective coercion to a function from `α` to `β`, and if the seminorm on the group `α` satisfies the properties of a `GroupSeminormClass`, then the image of the identity element (1) in `α` under any function of type `F` is the zero element of `β`. This is a property that arises in the context of seminorms on a group, where the image of the identity of the group is expected to be zero.
More concisely: For any group α, ordered additive commutative monoid β, and a function F from α to β with an injective coercion, if the seminorm on α is a GroupSeminormClass, then the image of the identity element of α under F is the zero element of β.
|
RingNormClass.eq_zero_of_map_eq_zero
theorem RingNormClass.eq_zero_of_map_eq_zero :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : NonUnitalNonAssocRing α] [inst_1 : OrderedSemiring β]
[inst_2 : FunLike F α β] [self : RingNormClass F α β] (f : F) {a : α}, f a = 0 → a = 0
The theorem `RingNormClass.eq_zero_of_map_eq_zero` states that for a given function `f` of type `F`, that transforms elements of type `α` into elements of type `β`, if the image of an element `a` under function `f` is zero, then the element `a` itself is zero. Here, `α` is a non-unital non-associative ring, and `β` is an ordered semiring. `F` is a type that behaves function-like from `α` to `β`. Furthermore, `F` has the `RingNormClass` property, which connects it to ring norm operations.
More concisely: If `f` is a function from a non-unital non-associative ring `α` to an ordered semiring `β` with the `RingNormClass` property, then `f(a) = 0` implies `a = 0`.
|
SubmultiplicativeHomClass.map_mul_le_mul
theorem SubmultiplicativeHomClass.map_mul_le_mul :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Mul α] [inst_1 : Mul β] [inst_2 : LE β]
[inst_3 : FunLike F α β] [self : SubmultiplicativeHomClass F α β] (f : F) (a b : α), f (a * b) ≤ f a * f b
This theorem is about submultiplicative homomorphisms. It states that for any types `F`, `α`, and `β`, where `α` and `β` are equipped with multiplication operations and `β` also has an order relation (`≤`), and where `F` is a type that can be seen as a function from `α` to `β` (due to `FunLike F α β`), if a function `f` of type `F` is a submultiplicative homomorphism (as indicated by `SubmultiplicativeHomClass F α β`), then for any two elements `a` and `b` of type `α`, the image of their product under `f` is less than or equal to the product of their images. In mathematical notation, this would be $f(a \cdot b) \leq f(a) \cdot f(b)$.
More concisely: For any submultiplicative homomorphism `f : α → β` from a type `α` equipped with multiplication and order relation to a type `β`, `f(a * b) ≤ f(a) * f(b)` for all `a, b ∈ α`, where `*` denotes multiplication in `α`.
|
SubadditiveHomClass.map_add_le_add
theorem SubadditiveHomClass.map_add_le_add :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : Add α] [inst_1 : Add β] [inst_2 : LE β]
[inst_3 : FunLike F α β] [self : SubadditiveHomClass F α β] (f : F) (a b : α), f (a + b) ≤ f a + f b
This theorem states that for any types `F`, `α`, and `β`, where `α` and `β` have addition (`Add α` and `Add β`) and `β` has a less than or equal to ordering (`LE β`), and `F` is a function type from `α` to `β` that is subadditive (`SubadditiveHomClass F α β`), then for any function `f` of type `F` and any two elements `a` and `b` of type `α`, the image of the sum `a + b` under `f` is less than or equal to the sum of the individual images `f a + f b`. In other words, the function `f` is subadditive: it preserves the property that the sum of the inputs is less than or equal to the sum of the outputs.
More concisely: For any subadditive function `F : α -> β` between additive types `α` and `β` with a least element ordering, `LE β`, we have `f (a + b) <= f a + f b` for all `a, b : α`.
|
map_div_rev
theorem map_div_rev :
∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α]
[inst_2 : OrderedAddCommMonoid β] [inst_3 : GroupSeminormClass F α β] (f : F) (x y : α), f (x / y) = f (y / x)
The theorem `map_div_rev` states that for any types `F`, `α`, and `β`, if `F` is a function-like structure from `α` to `β` (`FunLike F α β`), `α` is a group, `β` is an ordered addition commutative monoid, and the class `GroupSeminormClass` is instantiated for `F`, `α`, `β`, then for any instance `f` of type `F` and any elements `x`, `y` of type `α`, the result of applying `f` to the division of `x` by `y` is equal to the result of applying `f` to the division of `y` by `x`. In mathematical terms, $f(x/y) = f(y/x)$ under the given conditions.
More concisely: Given a function-like structure `F` from a group `α` to an ordered addition commutative monoid `β` with instantiated `GroupSeminormClass`, for all `x`, `y` in `α`, `f(x/y) = f(y/x)`.
|
AddGroupSeminormClass.map_zero
theorem AddGroupSeminormClass.map_zero :
∀ {F : Type u_7} {α : Type u_8} {β : Type u_9} [inst : AddGroup α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : FunLike F α β] [self : AddGroupSeminormClass F α β] (f : F), f 0 = 0
This theorem, named `AddGroupSeminormClass.map_zero`, states that for any types `F`, `α`, and `β`, given an `AddGroup` structure on `α`, an `OrderedAddCommMonoid` structure on `β`, a `FunLike` structure from `F` to functions from `α` to `β`, and an `AddGroupSeminormClass` structure for `F`, `α`, and `β`, the image of the zero element of `α` under any function `f : F` is the zero element of `β`. In other words, for functions that have these structures, zero is always mapped to zero.
More concisely: For any `AddGroup` `α`, `OrderedAddCommMonoid` `β`, `FunLike` `F (α → β)`, and `AddGroupSeminormClass` for `F`, `α`, and `β`, the image of the zero element of `α` under any function from `F` to `α → β` is the zero element of `β`.
|