AddMonoidHom.mkNormedAddGroupHom_norm_le'
theorem AddMonoidHom.mkNormedAddGroupHom_norm_le' :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ max C 0
The theorem `AddMonoidHom.mkNormedAddGroupHom_norm_le'` states that for any group homomorphism `f` from a semi-normed addition commutative group `V₁` to another one `V₂`, if a bounded group homomorphism map is created from `f` using the constructor `AddMonoidHom.mkNormedAddGroupHom` with a given real number `C` as bound, the norm of the created bounded homomorphism map is less than or equal to the maximum of `C` and zero. It's also given that the norm of the group homomorphism `f` applied to any element `x` of `V₁` is less than or equal to `C` times the norm of `x`.
More concisely: For any semi-normed additive commutative group homomorphism `f` from `V₁` to `V₂` and real number `C` such that the norm of `f(x)` is bounded by `C` for all `x` in `V₁`, the norm of the resulting bounded homomorphism `AddMonoidHom.mkNormedAddGroupHom f C` is less than or equal to `C`.
|
NormedAddGroupHom.norm_id
theorem NormedAddGroupHom.norm_id :
∀ {V : Type u_5} [inst : NormedAddCommGroup V] [inst_1 : Nontrivial V], ‖NormedAddGroupHom.id V‖ = 1
This theorem states that for any non-trivial normed additive commutative group `V`, the norm of the identity function as a continuous normed group homomorphism equals `1`. In other words, when the underlying space is non-empty (i.e., it has at least two distinct elements), the operator norm of the identity operator on this space is equal to `1`.
More concisely: For any non-trivial normed additive commutative group `V`, the operator norm of the identity function is equal to 1.
|
NormedAddGroupHom.opNorm_zero_iff
theorem NormedAddGroupHom.opNorm_zero_iff :
∀ {V₁ : Type u_5} {V₂ : Type u_6} [inst : NormedAddCommGroup V₁] [inst_1 : NormedAddCommGroup V₂]
{f : NormedAddGroupHom V₁ V₂}, ‖f‖ = 0 ↔ f = 0
This theorem states that, for normed additive commutative groups V₁ and V₂, an operator 'f' from V₁ to V₂ is equal to zero if and only if the norm of 'f' is zero. In other words, in the context of normed groups, the norm of an operator vanishing is equivalent to the operator itself being zero.
More concisely: For normed additive commutative groups V₁ and V₂, an operator f from V₁ to V₂ is equal to the zero operator if and only if the norm of f is zero.
|
NormedAddGroupHom.mkNormedAddGroupHom_norm_le'
theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le' :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ max C 0
This theorem states that for any seminormed additive commutative group `V₁` and `V₂`, and a group homomorphism `f` from `V₁` to `V₂`, if a bounded group homomorphism is created using the constructor `AddMonoidHom.mkNormedAddGroupHom` with a certain bound `C`, then the norm of this new homomorphism is less than or equal to the maximum of `C` and `0`. This means that if we provide a negative `C` to the constructor, the norm of the resulting homomorphism will be bounded by `0`. This theorem guarantees that the `mkNormedAddGroupHom` constructor indeed creates a homomorphism whose norm does not exceed the provided bound, or `0` if the bound is negative.
More concisely: For any seminormed additive commutative groups `V₁` and `V₂`, and a group homomorphism `f` from `V₁` to `V₂`, the norm of the bounded homomorphism created using `AddMonoidHom.mkNormedAddGroupHom` from `f` with bound `C` satisfies `||f|| ≤ max{|C|, 0}`.
|
NormedAddGroupHom.ofLipschitz_norm_le
theorem NormedAddGroupHom.ofLipschitz_norm_le :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : V₁ →+ V₂) {K : NNReal} (h : LipschitzWith K ⇑f), ‖NormedAddGroupHom.ofLipschitz f h‖ ≤ ↑K
The theorem `NormedAddGroupHom.ofLipschitz_norm_le` states that for any two seminormed additively commutative groups `V₁` and `V₂`, if we have a Lipschitz continuous group homomorphism `f : V₁ →+ V₂` with a non-negative real number `K` as the Lipschitz constant, then when `f` is equipped as a normed additive group homomorphism using the constructor `NormedAddGroupHom.ofLipschitz`, the norm of this new object is less than or equal to `K`. In other words, the Lipschitz constant `K` provides an upper bound for the norm of the created normed additive group homomorphism from a Lipschitz continuous group homomorphism.
More concisely: For any Lipschitz continuous group homomorphism between seminormed additive groups with a given Lipschitz constant, the resulting normed additive group homomorphism has a norm equal to or less than the Lipschitz constant.
|
NormedAddGroupHom.opNorm_nonneg
theorem NormedAddGroupHom.opNorm_nonneg :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : NormedAddGroupHom V₁ V₂), 0 ≤ ‖f‖
This theorem states that for any normed additive commutative group `V₁` and `V₂`, the operator norm of a normed group homomorphism `f` from `V₁` to `V₂` is non-negative, i.e., `0 ≤ ‖f‖`. The norm of `f` here represents a measure of its "size" or "length", and this theorem asserts that such a measure cannot be negative.
More concisely: The norm of a normed group homomorphism is non-negative.
|
NormedAddGroupHom.opNorm_add_le
theorem NormedAddGroupHom.opNorm_add_le :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f g : NormedAddGroupHom V₁ V₂), ‖f + g‖ ≤ ‖f‖ + ‖g‖
The theorem `NormedAddGroupHom.opNorm_add_le` states that for any two elements `f` and `g` from the type `NormedAddGroupHom V₁ V₂` (which represents normed additive group homomorphisms between two seminormed additive commutative groups `V₁` and `V₂`), the operator norm of their sum is less than or equal to the sum of their respective operator norms. This is the triangle inequality property specific to the operator norm in the context of normed additive group homomorphisms.
More concisely: For any `f : NormedAddGroupHom V₁ V₂` and `g : NormedAddGroupHom V₁ V₂`, their operator norms satisfy `‖f + g‖ ≤ ‖f‖ + ‖g‖`.
|
NormedAddGroupHom.bounds_bddBelow
theorem NormedAddGroupHom.bounds_bddBelow :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
{f : NormedAddGroupHom V₁ V₂}, BddBelow {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
This theorem states that for any normed additive commutative groups `V1` and `V2`, and any normed additive group homomorphism `f` from `V1` to `V2`, the set of all real numbers `c` satisfying two conditions (1: `c` is non-negative, and 2: the norm of `f(x)` is less than or equal to `c` times the norm of `x` for all `x` in `V1`) is bounded from below. In other words, there exists a lower bound for the set of scalars that can bound the norm of the function `f` on every element of `V1`.
More concisely: For any normed additive commutative groups V1 and V2, and normed additive group homomorphism f from V1 to V2, there exists a positive real number c such that for all x in V1, ||fx|| ≤ c * ||x|| holds.
|
NormedAddGroupHom.Equalizer.map.proof_1
theorem NormedAddGroupHom.Equalizer.map.proof_1 :
∀ {V₁ : Type u_2} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
{W₁ : Type u_3} {W₂ : Type u_1} [inst_2 : SeminormedAddCommGroup W₁] [inst_3 : SeminormedAddCommGroup W₂]
{f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} (φ : NormedAddGroupHom V₁ V₂)
(ψ : NormedAddGroupHom W₁ W₂),
ψ.comp f₁ = f₂.comp φ →
ψ.comp g₁ = g₂.comp φ →
f₂.comp (φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)) =
g₂.comp (φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁))
This theorem states that, for any two types `V₁` and `V₂` that form semi-normed commutative additive groups, and any two other such types `W₁` and `W₂`, given two normed additive group homomorphisms `f₁` and `g₁` from `V₁` to `W₁`, two normed additive group homomorphisms `f₂` and `g₂` from `V₂` to `W₂`, and two other normed additive group homomorphisms `φ` from `V₁` to `V₂` and `ψ` from `W₁` to `W₂`, if the composition of `ψ` and `f₁` equals the composition of `f₂` and `φ`, and the composition of `ψ` and `g₁` equals the composition of `g₂` and `φ`, then the composition of `f₂` and the composition of `φ` and the inclusion of the equalizer of `f₁` and `g₁` equals the composition of `g₂` and the composition of `φ` and the inclusion of the equalizer of `f₁` and `g₁`. This theorem can be seen as a property of the equalizer in the category of normed additive group homomorphisms.
More concisely: Given normed additive group homomorphisms `f₁, g₁: V₁ → W₁`, `f₂, g₂: V₂ → W₂`, `φ: V₁ → V₂`, and `ψ: W₁ → W₂`, if `ψ ∘ f₁ = f₂ ∘ φ` and `ψ ∘ g₁ = g₂ ∘ φ`, then `f₂ ∘ φ ∘ i = g₂ ∘ φ ∘ i`, where `i` is the inclusion of the equalizer of `f₁` and `g₁`.
|
NormedAddGroupHom.Equalizer.lift_normNoninc
theorem NormedAddGroupHom.Equalizer.lift_normNoninc :
∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V]
[inst_1 : SeminormedAddCommGroup W] [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W}
(φ : NormedAddGroupHom V₁ V) (h : f.comp φ = g.comp φ),
φ.NormNoninc → (NormedAddGroupHom.Equalizer.lift φ h).NormNoninc
This theorem states that in the context of semi-normed additive commutative groups V, W, and V₁, if we have two normed additive group homomorphisms f and g from V to W, and another normed additive group homomorphism φ from V₁ to V such that the composition of f and φ equals the composition of g and φ, then if φ is norm non-increasing, the lift of φ to the equalizer of f and g is also norm non-increasing. In simpler terms, this theorem is about the preservation of a norm non-increasing property under certain conditions in the context of normed additive group homomorphisms.
More concisely: If two normed additive group homomorphisms from semi-normed additive commutative groups have the same composition with a norm non-increasing homomorphism from another group, then their equalizer lifts preserve the norm non-increasing property.
|
NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one
theorem NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one :
∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
{f : NormedAddGroupHom V W}, f.NormNoninc ↔ ‖f‖ ≤ 1
This theorem states that for any two types `V` and `W`, which are semi-normed additive commutative groups, a normed additive group homomorphism `f` from `V` to `W` is norm-nonincreasing (meaning the norm of `f v` is less than or equal to the norm of `v` for all `v` in `V`) if and only if the norm of `f` is less than or equal to one.
More concisely: A normed additive group homomorphism between two semi-normed additive commutative groups is norm-nonincreasing if and only if its norm is less than or equal to 1.
|
NormedAddGroupHom.comp_apply
theorem NormedAddGroupHom.comp_apply :
∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
[inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃)
(f : NormedAddGroupHom V₁ V₂) (a : V₁), (g.comp f) a = g (f a)
This theorem states that for any three types `V₁`, `V₂`, and `V₃` which have a structure of seminormed additive commutative groups, if `g` is a normed additive group homomorphism from `V₂` to `V₃` and `f` is a normed additive group homomorphism from `V₁` to `V₂`, then for any element `a` of `V₁`, the result of applying the composition of `g` and `f` to `a` is the same as the result of applying `g` to the result of applying `f` to `a`. In other words, the theorem asserts the associativity of the application of composed normed additive group homomorphisms in the context of seminormed additive commutative groups.
More concisely: Given three seminormed additive commutative groups `V₁`, `V₂`, and `V₃`, and normed additive group homomorphisms `f : V₁ → V₂` and `g : V₂ → V₃`, the composition `g ∘ f : V₁ → V₃` is a normed additive group homomorphism, and for all `a ∈ V₁`, `g(f(a)) = (g ∘ f)(a)`.
|
NormedAddGroupHom.norm_id_of_nontrivial_seminorm
theorem NormedAddGroupHom.norm_id_of_nontrivial_seminorm :
∀ (V : Type u_1) [inst : SeminormedAddCommGroup V], (∃ x, ‖x‖ ≠ 0) → ‖NormedAddGroupHom.id V‖ = 1
This theorem states that if there exists an element in a seminormed additive commutative group whose norm is different from zero, then the norm of the identity function in that group equals one. Note that it's not sufficient to assume the group is non-trivial since we are working with seminorms.
More concisely: In a seminormed additive commutative group with an element of non-zero norm, the norm of the identity function equals one.
|
NormedAddGroupHom.continuous
theorem NormedAddGroupHom.continuous :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : NormedAddGroupHom V₁ V₂), Continuous ⇑f
This theorem states that for any two types `V₁` and `V₂` that have the structure of a semi-normed additive commutative group, any normed additive group homomorphism `f` from `V₁` to `V₂` is continuous. In mathematical terms, it says that normed additive group homomorphisms between semi-normed additive commutative groups are always continuous functions.
More concisely: Any normed additive group homomorphism between two semi-normed additive commutative groups is a continuous function.
|
NormedAddGroupHom.opNorm_le_bound
theorem NormedAddGroupHom.opNorm_le_bound :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : NormedAddGroupHom V₁ V₂) {M : ℝ}, 0 ≤ M → (∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M
This theorem states that in the context of seminormed additive commutative groups, if for a normed additive group homomorphism `f` from group `V₁` to `V₂`, there exists a non-negative real number `M` such that the norm of `f(x)` is less than or equal to `M` times the norm of `x` for every `x` in `V₁`, then the norm of the homomorphism `f` itself is less than or equal to `M`.
More concisely: If `f` is a normed additive group homomorphism from seminormed additive group `V₁` to `V₂` with the property that `∀x ∈ V₁, ‖f(x)‖ ≤ M * ‖x‖,` then `‖f‖ ≤ M.`
|
NormedAddGroupHom.NormNoninc.comp
theorem NormedAddGroupHom.NormNoninc.comp :
∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
[inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {g : NormedAddGroupHom V₂ V₃}
{f : NormedAddGroupHom V₁ V₂}, g.NormNoninc → f.NormNoninc → (g.comp f).NormNoninc
This theorem states that if we have two normed add group homomorphisms `g` and `f` between three seminormed add commutative groups `V₁`, `V₂`, and `V₃`, then if both `g` and `f` are norm-nonincreasing (meaning that the norm of each image is less than or equal to the norm of the corresponding input), the composition of `g` and `f` (denoted by `NormedAddGroupHom.comp g f`) is also norm-nonincreasing.
In symbols, if for all `v` in `V₁` and `w` in `V₂`, we have `‖f v‖ ≤ ‖v‖` and `‖g w‖ ≤ ‖w‖`, then for all `v` in `V₁`, we also have `‖(NormedAddGroupHom.comp g f) v‖ ≤ ‖v‖`. This is a property about preserving norms when we have the composition of two norm-nonincreasing normed add group homomorphisms.
More concisely: If `g` and `f` are norm-nonincreasing normed add group homomorphisms between seminormed add commutative groups `V₁`, `V₂`, and `V₃`, then the composition `NormedAddGroupHom.comp g f` is also a norm-nonincreasing homomorphism.
|
NormedAddGroupHom.mkNormedAddGroupHom_norm_le
theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : V₁ →+ V₂) {C : ℝ}, 0 ≤ C → ∀ (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ C
The theorem `NormedAddGroupHom.mkNormedAddGroupHom_norm_le` states that if a bounded group homomorphism is created from a group homomorphism using the constructor `AddMonoidHom.mkNormedAddGroupHom`, the norm of the resulting homomorphism is bounded by the nonnegative constant C, provided to the constructor, i.e., for all `x` in the domain, the norm of the image of `x` under the homomorphism is less than or equal to `C` times the norm of `x`. This condition is valid if `C` is nonnegative.
More concisely: For any non-negative constant C and a group homomorphism, the norm of the resulting bounded additive homomorphism obtained using `AddMonoidHom.mkNormedAddGroupHom` constructor is less than or equal to C times the norm of the input element.
|
NormedAddGroupHom.coe_inj
theorem NormedAddGroupHom.coe_inj :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
{f g : NormedAddGroupHom V₁ V₂}, ⇑f = ⇑g → f = g
This theorem states that for any two normed additive group homomorphisms `f` and `g` from a seminormed additive commutative group `V₁` to another seminormed additive commutative group `V₂`, if the function application of `f` and `g` (denoted by `⇑f` and `⇑g`) are equal, then `f` and `g` themselves are also equal. Essentially, it asserts the injectivity of the coercion function from the type of normed additive group homomorphisms to the type of functions.
More concisely: If two normed additive group homomorphisms between seminormed additive commutative groups have equal function applications, then they are equal.
|
NormedAddGroupHom.comp_assoc
theorem NormedAddGroupHom.comp_assoc :
∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
[inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {V₄ : Type u_5}
[inst_3 : SeminormedAddCommGroup V₄] (h : NormedAddGroupHom V₃ V₄) (g : NormedAddGroupHom V₂ V₃)
(f : NormedAddGroupHom V₁ V₂), (h.comp g).comp f = h.comp (g.comp f)
The theorem `NormedAddGroupHom.comp_assoc` states that for all seminormed additive commutative groups `V₁`, `V₂`, `V₃`, and `V₄`, and for all normed group homomorphisms `h` from `V₃` to `V₄`, `g` from `V₂` to `V₃`, and `f` from `V₁` to `V₂`, the composition of normed group homomorphisms is associative. This means that composing `h` and `g` first, and then composing the result with `f` is equal to first composing `g` and `f`, and then composing `h` with the result.
More concisely: For all seminormed additive commutative groups V₁, V₂, V₃, V₄, and normed group homomorphisms f : V₁ → V₂, g : V₂ → V₃, and h : V₃ → V₄, the associativity of composition holds: h ∘ g ∘ f = g ∘ f ∘ h.
|
AddMonoidHom.mkNormedAddGroupHom_norm_le
theorem AddMonoidHom.mkNormedAddGroupHom_norm_le :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : V₁ →+ V₂) {C : ℝ}, 0 ≤ C → ∀ (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ C
This theorem states that for any bounded group homomorphism function `f` from one seminormed additive commutative group `V₁` to another `V₂`, if a normed group homomorphism is created from `f` using the constructor `AddMonoidHom.mkNormedAddGroupHom` with a nonnegative bound `C`, then the norm of this new function is less than or equal to `C`. This condition holds true for all `x` in `V₁` such that the norm of `f x` is less than or equal to `C` times the norm of `x`.
More concisely: For any bounded group homomorphism `f` from a seminormed additive commutative group `V₁` to another `V₂`, the norm of the resulting normed group homomorphism obtained using `AddMonoidHom.mkNormedAddGroupHom` with a nonnegative bound `C` satisfies `∀x ∈ V₁|∥fx∥ ≤ C * ∥x∥`.
|
NormedAddGroupHom.bound'
theorem NormedAddGroupHom.bound' :
∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
(self : NormedAddGroupHom V W), ∃ C, ∀ (v : V), ‖self.toFun v‖ ≤ C * ‖v‖
This theorem states that for every `NormedAddGroupHom` from a seminormed additive commutative group `V` to another seminormed additive commutative group `W`, there exists a constant `C` such that for all elements `v` of `V`, the norm of `self.toFun v` is less than or equal to `C` times the norm of `v`. Essentially, it asserts that the function defined by `NormedAddGroupHom` is bounded with respect to the norm in these mathematical structures.
More concisely: For every normed additive homomorphism from a seminormed additive commutative group to another, there exists a constant such that the norm of the image under the homomorphism is bounded by the constant times the norm of the argument.
|
NormedAddGroupHom.uniformContinuous
theorem NormedAddGroupHom.uniformContinuous :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : NormedAddGroupHom V₁ V₂), UniformContinuous ⇑f
The theorem `NormedAddGroupHom.uniformContinuous` states that for any two semi-normed additive commutative groups, `V₁` and `V₂`, any homomorphism `f` from `V₁` to `V₂` is uniformly continuous. This means that as any pair of elements `(x, y)` in `V₁` gets arbitrarily close together (i.e., tends towards the diagonal), the images of these elements under `f` (i.e., `(f x, f y)`) also get arbitrarily close together in `V₂`, no matter where `x` and `y` are in `V₁`.
More concisely: Given any two semi-normed additive commutative groups `V₁` and `V₂` and any homomorphism `f` from `V₁` to `V₂`, `f` is uniformly continuous.
|
NormedAddGroupHom.lipschitz
theorem NormedAddGroupHom.lipschitz :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : NormedAddGroupHom V₁ V₂), LipschitzWith ⟨‖f‖, ⋯⟩ ⇑f
The theorem `NormedAddGroupHom.lipschitz` states that for any continuous linear map `f` from one seminormed additive commutative group `V₁` to another `V₂`, `f` is Lipschitz continuous with a Lipschitz constant of `‖f‖`. In other words, for any pair of elements `x, y` in `V₁`, the distance in `V₂` between `f(x)` and `f(y)` is less than or equal to `‖f‖` times the distance between `x` and `y` in `V₁`. The value `‖f‖` represents the operator norm of the linear map `f`.
More concisely: For any continuous linear map between two seminormed additive commutative groups, the operator norm bounds the Lipschitz constant, ensuring that the image difference is less than or equal to the norm times the difference of the arguments.
|
NormedAddGroupHom.le_opNorm
theorem NormedAddGroupHom.le_opNorm :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : NormedAddGroupHom V₁ V₂) (x : V₁), ‖f x‖ ≤ ‖f‖ * ‖x‖
This Lean theorem, `NormedAddGroupHom.le_opNorm`, is stating the fundamental property of the operator norm in the context of normed additive commutative groups. Specifically, for any two types `V₁` and `V₂` that are seminormed additive commutative groups, and for any normed additive group homomorphism `f` from `V₁` to `V₂`, the norm of `f(x)` is always less than or equal to the product of the norm of `f` and the norm of `x`. This is often referred to as the inequality of the operator norm.
More concisely: For any normed additive commutative groups V₁ and V₂ and any normed additive group homomorphism f from V₁ to V₂, the norm of f(x) is less than or equal to the norm of f multiplied by the norm of x for all x in V₁.
|
NormedAddGroupHom.norm_id_le
theorem NormedAddGroupHom.norm_id_le :
∀ (V : Type u_1) [inst : SeminormedAddCommGroup V], ‖NormedAddGroupHom.id V‖ ≤ 1
This theorem states that the norm of the identity function on a seminormed additive commutative group is at most `1`. This norm is actually `1` except in the case where the norm of every element in the group is `0`, in which case the norm of the identity is also `0`. This can occur even when the group is non-trivial due to our consideration of seminorms. The theorem emphasizes that a general inequality is the best possible statement in this context, as the exact value of the norm depends on the specific properties of the group.
More concisely: The identity function on a seminormed additive commutative group has norm at most 1, with equality if and only if the group does not consist entirely of elements with norm 0.
|
NormedAddGroupHom.map_add'
theorem NormedAddGroupHom.map_add' :
∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
(self : NormedAddGroupHom V W) (v₁ v₂ : V), self.toFun (v₁ + v₂) = self.toFun v₁ + self.toFun v₂
The theorem `NormedAddGroupHom.map_add'` states that for any two elements `v₁` and `v₂` from a seminormed additive commutative group `V`, a normed additive group homomorphism `self` from `V` to another seminormed additive commutative group `W` preserves addition. In other words, applying `self` to the sum of `v₁` and `v₂` (i.e., `v₁ + v₂`) yields the same result as the sum of the images of `v₁` and `v₂` under `self` (i.e., `self.toFun v₁ + self.toFun v₂`).
More concisely: For any seminormed additive commutative group homomorphism `self` from a seminormed additive commutative group `V` to another such group `W`, `self (v₁ + v₂) = self v₁ + self v₂` for all `v₁, v₂ ∈ V`.
|
NormedAddGroupHom.ext
theorem NormedAddGroupHom.ext :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
{f g : NormedAddGroupHom V₁ V₂}, (∀ (x : V₁), f x = g x) → f = g
This theorem, `NormedAddGroupHom.ext`, states that for any two normed additive group homomorphisms `f` and `g` from a seminormed additive commutative group `V₁` to another seminormed additive commutative group `V₂`, if `f` and `g` map every element `x` of `V₁` to the same element in `V₂`, then `f` and `g` are the same homomorphism. In other words, two normed additive group homomorphisms are equal if they agree on all elements of the domain.
More concisely: If two normed additive group homomorphisms from a seminormed additive commutative group to another agree on all elements, then they are equal.
|
NormedAddGroupHom.mem_ker
theorem NormedAddGroupHom.mem_ker :
∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
(f : NormedAddGroupHom V₁ V₂) (v : V₁), v ∈ f.ker ↔ f v = 0
This theorem in Lean 4 is stating that, for any two types `V₁` and `V₂` which are instances of the typeclass `SeminormedAddCommGroup`, and given a Bounded Group homomorphism `f` from `V₁` to `V₂` and an element `v` from `V₁`, `v` is in the kernel of `f` if and only if applying `f` to `v` results in the zero element of `V₂`. In other words, the kernel of a Bounded Group homomorphism consists of all elements from the source group that are mapped to the zero element in the target group.
More concisely: A Bounded Group homomorphism maps elements in its source group to the zero element in the target group if and only if those elements are in the kernel of the homomorphism.
|
NormedAddGroupHom.Equalizer.norm_lift_le
theorem NormedAddGroupHom.Equalizer.norm_lift_le :
∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V]
[inst_1 : SeminormedAddCommGroup W] [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W}
(φ : NormedAddGroupHom V₁ V) (h : f.comp φ = g.comp φ) (C : ℝ),
‖φ‖ ≤ C → ‖NormedAddGroupHom.Equalizer.lift φ h‖ ≤ C
This theorem states that for any seminormed additive commutative groups `V`, `W`, and `V₁`, given two morphisms `f` and `g` from `V` to `W`, and another morphism `φ` from `V₁` to `V` such that `f` composed with `φ` is equal to `g` composed with `φ`, if the norm of `φ` is less than or equal to a real number `C`, then the norm of the lifted morphism created from `φ` and this equal composition condition also has a norm less than or equal to `C`.
More concisely: Given seminormed additive commutative groups `V`, `W`, and `V₁`, morphisms `f: V → W`, `g: V → W`, and `φ: V₁ → V` with `||φ|| ≤ C`, if `f ∘ φ = g ∘ φ`, then `||L.lift g φ|| ≤ C`, where `L.lift` denotes the morphism lifting from `φ` and `g`.
|
NormedAddGroupHom.opNorm_zero
theorem NormedAddGroupHom.opNorm_zero :
∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂],
‖0‖ = 0
This theorem states that the operator norm of the zero operator is zero. It applies to any two types V₁ and V₂, given that both V₁ and V₂ are seminormed additive commutative groups. In mathematical terms, if we consider the zero operator from V₁ to V₂, its norm is zero.
More concisely: The norm of the zero operator from a seminormed additive commutative group V₁ to another seminormed additive commutative group V₂ is zero.
|