GroupSeminorm.ext
theorem GroupSeminorm.ext : ∀ {E : Type u_4} [inst : Group E] {p q : GroupSeminorm E}, (∀ (x : E), p x = q x) → p = q
This theorem, called `GroupSeminorm.ext`, states that given a type `E` which forms a group, and two group seminorms `p` and `q` on this group, if for every element `x` in the group, the value of seminorm `p` at `x` equals the value of seminorm `q` at `x`, then the seminorms `p` and `q` are equal. Essentially, it asserts the uniqueness of group seminorms: two group seminorms are identical if they produce the same value for each element in the group.
More concisely: If two functions define the same value for every element in a group, then they are equal as group seminorms.
|
NonarchAddGroupNormClass.eq_zero_of_map_eq_zero
theorem NonarchAddGroupNormClass.eq_zero_of_map_eq_zero :
∀ {F : Type u_7} {α : outParam (Type u_8)} [inst : AddGroup α] [inst_1 : FunLike F α ℝ]
[self : NonarchAddGroupNormClass F α] (f : F) {a : α}, f a = 0 → a = 0
The theorem `eq_zero_of_map_eq_zero` states that for any type `F`, any type `α` that forms an additive group, and any term `f` of type `F` that behaves like a function from `α` to the real numbers ℝ (i.e., `F` is `FunLike` to ℝ), if for a given element `a` of `α`, the value of function `f` at `a` is zero, then `a` itself is zero. This property is under the context of `F` and `α` forming a non-Archimedean additive group norm, which means that the norms satisfy certain properties related to the structure of an additive group in non-Archimedean fields.
More concisely: In a non-Archimedean additive group norm, if a function mapping an additive group to real numbers maps an element to zero, then that element is the additive identity.
|
NonarchAddGroupNorm.eq_zero_of_map_eq_zero'
theorem NonarchAddGroupNorm.eq_zero_of_map_eq_zero' :
∀ {G : Type u_7} [inst : AddGroup G] (self : NonarchAddGroupNorm G) (x : G), self.toFun x = 0 → x = 0
This theorem states that for any type `G` that has an `AddGroup` structure, and for any `NonarchAddGroupNorm` on `G`, if the application of the `NonarchAddGroupNorm` function to an element `x` of `G` results in zero, then the element `x` must be the zero element of `G`. In other words, within this mathematical structure, only the zero element gets mapped to zero under the norm.
More concisely: For any AddGroup `G` and `NonarchAddGroupNorm` function on `G`, if `NonarchAddGroupNorm x = 0`, then `x` is the zero element of `G`.
|
AddGroupSeminorm.ext
theorem AddGroupSeminorm.ext :
∀ {E : Type u_4} [inst : AddGroup E] {p q : AddGroupSeminorm E}, (∀ (x : E), p x = q x) → p = q
This theorem states that for any type `E` that has a structure of an additive group, if we have two additive group semi-norms `p` and `q`, then if for every element `x` in `E` the semi-norm `p` of `x` is equal to the semi-norm `q` of `x`, we can conclude that `p` and `q` are the same semi-norm. In other words, two additive group semi-norms on a given additive group are equal if and only if they give the same value for every element of the group.
More concisely: Two additive group semi-norms on an additive group are equal if and only if they agree on all group elements.
|
GroupNorm.eq_one_of_map_eq_zero'
theorem GroupNorm.eq_one_of_map_eq_zero' :
∀ {G : Type u_7} [inst : Group G] (self : GroupNorm G) (x : G), self.toFun x = 0 → x = 1
This theorem states that for any group `G` and any element `x` in `G`, if the norm of `x` (as computed by the `GroupNorm` function `toFun`) is zero, then `x` must be the identity element of the group (`1`). In other words, the only group element with zero norm is the identity.
More concisely: In a group `G`, if `GroupNorm x = 0`, then `x` is the identity element `1` of `G`.
|
NonarchAddGroupSeminorm.add_le_max'
theorem NonarchAddGroupSeminorm.add_le_max' :
∀ {G : Type u_7} [inst : AddGroup G] (self : NonarchAddGroupSeminorm G) (r s : G),
self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
This theorem states that for any additive group `G` and any seminorm on this group, the value of the seminorm at the sum of two elements `r` and `s` from this group is less than or equal to the maximum of the values of the seminorm at `r` and `s`. This is to say, the seminorm of a sum is dominated by the maximum of the seminorms of the summands.
More concisely: For any additive group G and seminorm on G, the seminorm of the sum of any two elements is less than or equal to the maximum of the seminorms of the summands.
|
AddGroupSeminorm.map_zero'
theorem AddGroupSeminorm.map_zero' :
∀ {G : Type u_7} [inst : AddGroup G] (self : AddGroupSeminorm G), self.toFun 0 = 0
For any additive group `G` and any semi-norm `self` on this group, the value of `self` at the zero element of `G` is zero. In other words, the image of zero under the semi-norm is zero. This theorem is a basic property of semi-norms in the context of additive groups.
More concisely: For any additive group G and semi-norm self, self (0) = 0.
|
AddGroupSeminorm.neg'
theorem AddGroupSeminorm.neg' :
∀ {G : Type u_7} [inst : AddGroup G] (self : AddGroupSeminorm G) (r : G), self.toFun (-r) = self.toFun r
This theorem states that the seminorm of a group element under negation is equal to the seminorm of the original element. In other words, for any given type `G` that has an additive group structure and a seminorm defined on it, the value of the seminorm at `-r` (the additive inverse of `r`) is the same as the value of the seminorm at `r` itself.
More concisely: For any additive group `G` equipped with a seminorm, the seminorm of the additive inverse `-r` is equal to the seminorm of `r`: `‖-r‖ = ‖r‖`.
|
NonarchAddGroupSeminorm.neg'
theorem NonarchAddGroupSeminorm.neg' :
∀ {G : Type u_7} [inst : AddGroup G] (self : NonarchAddGroupSeminorm G) (r : G), self.toFun (-r) = self.toFun r
This theorem states that the seminorm is invariant under negation. In other words, for any given AddGroup `G` and a Nonarchimedean group seminorm `self` defined on `G`, the seminorm of any element `r` in `G` is equal to the seminorm of the negation of `r`. This implies that seminorms are not affected by the sign of the elements in the AddGroup `G`.
More concisely: For any AddGroup `G` and Nonarchimedean group seminorm `self` on `G`, the seminorm of an element `r` is equal to the seminorm of the negation of `r`.
|
GroupSeminorm.mul_bddBelow_range_add
theorem GroupSeminorm.mul_bddBelow_range_add :
∀ {E : Type u_4} [inst : CommGroup E] {p q : GroupSeminorm E} {x : E},
BddBelow (Set.range fun y => p y + q (x / y))
The theorem `GroupSeminorm.mul_bddBelow_range_add` states that for any type `E` forming a commutative group, and for any two group seminorms `p` and `q` on `E`, and for any element `x` in `E`, the set of all values resulting from applying the function `y => p y + q (x / y)` to all possible `y` values is bounded below. Here, `BddBelow` denotes the property of a set being bounded below, `Set.range` denotes the range of a function, and `y => p y + q (x / y)` is a function mapping a group element `y` to the sum of `p y` and `q (x / y)`.
More concisely: For any commutative group `E`, and group seminorms `p` and `q` on `E`, the set of values `{p y + q (x / y) | y ∈ E\*\*:1}` is bounded below for all `x` in `E`.
|
AddGroupNorm.eq_zero_of_map_eq_zero'
theorem AddGroupNorm.eq_zero_of_map_eq_zero' :
∀ {G : Type u_7} [inst : AddGroup G] (self : AddGroupNorm G) (x : G), self.toFun x = 0 → x = 0
This theorem states that for any additive group `G`, given an additive group norm `self` and an element `x` of `G`, if the image of `x` under the norm function is zero, then `x` itself must be zero. In other words, in the context of additive group norms, only the zero element can map to zero under the norm function.
More concisely: In an additive group with a norm function, if the norm of an element is zero, then the element is the additive identity (zero).
|
NonarchAddGroupSeminormClass.map_neg_eq_map'
theorem NonarchAddGroupSeminormClass.map_neg_eq_map' :
∀ {F : Type u_7} {α : outParam (Type u_8)} [inst : AddGroup α] [inst_1 : FunLike F α ℝ]
[self : NonarchAddGroupSeminormClass F α] (f : F) (a : α), f (-a) = f a
The theorem `NonarchAddGroupSeminormClass.map_neg_eq_map'` states that for any type `F` and an out-parameter type `α` which is an additive group, if `F` has a function-like relationship with `α` and real numbers `ℝ` and `F` is in the `NonarchAddGroupSeminormClass`, then the seminorm of `F` is invariant under negation. In other words, for any element `a` from `α` and function `f` from `F`, applying `f` to the negation of `a` (`-a`) is equal to applying `f` to `a` itself.
More concisely: For any additive group `α`, function-like type `F` with seminorm in `NonarchAddGroupSeminormClass`, and elements `a` from `α` and `f` from `F`, `����f a���� = ����f (-a)����`.
|
AddGroupSeminorm.add_le'
theorem AddGroupSeminorm.add_le' :
∀ {G : Type u_7} [inst : AddGroup G] (self : AddGroupSeminorm G) (r s : G),
self.toFun (r + s) ≤ self.toFun r + self.toFun s
This theorem, titled "AddGroupSeminorm.add_le'", states that for any add group "G" and any two elements "r" and "s" of this group, the seminorm of the sum of "r" and "s" is less than or equal to the sum of the seminorms of "r" and "s". In other words, it expresses the subadditivity property of the seminorm in an add group.
More concisely: For any add group (G : Type) and all elements r, s in G, the seminorm of r + s is less than or equal to the sum of the seminorms of r and s.
|
GroupSeminorm.map_one'
theorem GroupSeminorm.map_one' : ∀ {G : Type u_7} [inst : Group G] (self : GroupSeminorm G), self.toFun 1 = 0 := by
sorry
This theorem states that for any group `G`, and any seminorm defined on this group, the image of the identity element (denoted by `1`) under this seminorm is `0`. In other words, when the identity of the group is passed through the seminorm function, it maps to zero. This is a property that must hold for any seminorm on a group.
More concisely: For any seminorm `p` on a group `G`, we have `p 1 = 0`.
|
NonarchAddGroupSeminormClass.map_zero
theorem NonarchAddGroupSeminormClass.map_zero :
∀ {F : Type u_7} {α : outParam (Type u_8)} [inst : AddGroup α] [inst_1 : FunLike F α ℝ]
[self : NonarchAddGroupSeminormClass F α] (f : F), f 0 = 0
The theorem `NonarchAddGroupSeminormClass.map_zero` states that for any type `F`, any type `α` which is an additive group, and any function `f` of type `F` that has a `FunLike` relationship to functions from `α` to the real numbers ℝ, if `f` also belongs to the class `NonarchAddGroupSeminormClass`, then the application of `f` to the group's zero element will yield zero. In simpler terms, this theorem says that a function which is a seminorm on an additive group will map the group's zero element to the real number zero.
More concisely: If `f` is a seminorm on an additive group `α` and belongs to `NonarchAddGroupSeminormClass`, then `f(0) = 0` where `0` is the additive identity of `α`.
|
AddGroupSeminorm.add_bddBelow_range_add
theorem AddGroupSeminorm.add_bddBelow_range_add :
∀ {E : Type u_4} [inst : AddCommGroup E] {p q : AddGroupSeminorm E} {x : E},
BddBelow (Set.range fun y => p y + q (x - y))
This theorem states that for any type `E` that forms an additive commutative group, and for any two additive group seminorms `p` and `q` on `E`, and for any element `x` from `E`, the set of all values obtained by applying the function `y => p y + q (x - y)` is bounded below. In other words, there exists a lower bound for the set of these function values. The function takes an element `y` from `E`, applies the seminorm `p` to `y`, subtracts `y` from `x`, applies the seminorm `q` to the result, and adds these two seminorm values together.
More concisely: For any additive commutative group `E`, any two additive group seminorms `p` and `q` on `E`, and any `x` in `E`, there exists a real number `b` such that for all `y` in `E`, `p y + q (x - y) ≥ b`.
|
GroupSeminorm.mul_le'
theorem GroupSeminorm.mul_le' :
∀ {G : Type u_7} [inst : Group G] (self : GroupSeminorm G) (x y : G),
self.toFun (x * y) ≤ self.toFun x + self.toFun y
This theorem states that for any group `G` and any two elements `x` and `y` of `G`, the seminorm of the product of `x` and `y` is less than or equal to the sum of the seminorm of `x` and the seminorm of `y`. In mathematical terms, if `self` is a seminorm on a group `G`, then the inequality `self(x * y) ≤ self(x) + self(y)` holds for all `x, y` in `G`. This is a property of seminorms in group theory and is an example of a subadditivity condition.
More concisely: For any seminorm `self` on a group `G` and any elements `x, y` in `G`, `self(x * y) ≤ self(x) + self(y)`.
|
GroupSeminorm.inv'
theorem GroupSeminorm.inv' :
∀ {G : Type u_7} [inst : Group G] (self : GroupSeminorm G) (x : G), self.toFun x⁻¹ = self.toFun x
This theorem states that the seminorm of a group element and its inverse are the same. More specifically, for any group `G` and any element `x` in `G`, applying the group seminorm to `x` and to the inverse of `x` (`x⁻¹`) yields the same result. This property characterizes the invariance of the group seminorm under inversion.
More concisely: For any group `G` and element `x` in `G`, the group seminorm of `x` equals the group seminorm of `x⁻¹`.
|