NormedAddGroupHom.isQuotientQuotient
theorem NormedAddGroupHom.isQuotientQuotient :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), S.normedMk.IsQuotient
The theorem `NormedAddGroupHom.isQuotientQuotient` states that for any type `M` which is a seminormed additive commutative group and any additive subgroup `S` of `M`, the function `AddSubgroup.normedMk S` is a quotient morphism. In other words, `AddSubgroup.normedMk S` maps `M` to the quotient group `M/S` and preserves the group structure under the seminorm. This is a fundamental property in the theory of normed groups and their quotients.
More concisely: The function `AddSubgroup.normedMk` on a seminormed additive commutative group `M` and its additive subgroup `S` is a quotient morphism, preserving the seminorm and group structure on `M/S`.
|
norm_mk_lt'
theorem norm_mk_lt' :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M) {ε : ℝ},
0 < ε → ∃ s ∈ S, ‖m + s‖ < ‖(QuotientAddGroup.mk' S) m‖ + ε
This theorem states that for any seminormed additive commutative group `M`, any subgroup `S` of `M`, any element `m` of `M`, and any real number `ε` greater than zero, there exists an element `s` in `S` such that the norm of `m + s` is less than the norm of the image of `m` under the additive group homomorphism from `M` to `M/S`, plus `ε`. In other words, in a seminormed additive commutative group, you can always find an element in a given subgroup that, when added to any given element, its norm will be closer to the norm of the original element in the quotient group by an arbitrarily small amount.
More concisely: For any seminormed additive commutative group `M`, subgroup `S`, element `m` in `M`, and real `ε > 0`, there exists `s` in `S` such that `∥m + s∥ < ∥m + S∥ + ε`, where `∥.∥` denotes the norm and `S + m` denotes the coset of `m` in `M/S`.
|
Submodule.Quotient.norm_mk_lt
theorem Submodule.Quotient.norm_mk_lt :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {R : Type u_3} [inst_1 : Ring R] [inst_2 : Module R M]
{S : Submodule R M} (x : M ⧸ S) {ε : ℝ}, 0 < ε → ∃ m, Submodule.Quotient.mk m = x ∧ ‖m‖ < ‖x‖ + ε
The theorem `Submodule.Quotient.norm_mk_lt` states that for any element `x` in the quotient space `M ⧸ S` of a module `M` by a submodule `S`, and for any positive real number `ε`, there exists an element `m` in `M` such that the submodule quotient of `m` is `x` and the norm of `m` is less than the sum of the norm of `x` and `ε`. Here, the norm function `‖•‖` is understood in the context of seminormed additive commutative groups. This theorem is a precise way of saying that we can always find an element in the original module `M` that is arbitrarily close (within `ε`) to our chosen element in the quotient space `M ⧸ S`.
More concisely: For any element `x` in the quotient space `M ⧸ S` of a module `M` by a submodule `S`, and for any positive real number `ε`, there exists an element `m` in `M` such that `x = [m]` (the submodule quotient of `m`) and `‖m‖ < ‖x‖ + ε`, where `‖•‖` is the norm function on `M`.
|
QuotientAddGroup.norm_lift_apply_le
theorem QuotientAddGroup.norm_lift_apply_le :
∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
{S : AddSubgroup M} (f : NormedAddGroupHom M N) (hf : ∀ x ∈ S, f x = 0) (x : M ⧸ S),
‖(QuotientAddGroup.lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖
This theorem states that for any seminormed additive commutative groups `M` and `N`, a subgroup `S` of `M`, a normed group homomorphism `f` from `M` to `N`, and a function `hf` that maps any element `x` in `S` to zero via `f`, the norm of the application of the "lifted" group homomorphism `QuotientAddGroup.lift S (NormedAddGroupHom.toAddMonoidHom f) hf` to an element `x` in the quotient group `M ⧸ S` is less than or equal to the product of the norm of `f` and the norm of `x`. Here, "lifted" refers to the process where a homomorphism defined on an original group is extended to a homomorphism defined on the quotient group. The norm ‖.‖ measures the "size" or "length" of an element in a normed group.
More concisely: For any seminormed additive commutative groups M and N, subgroup S of M, normed group homomorphism f from M to N, and function hf mapping any x in S to zero via f, the norm of the lifted homomorphism QuotientAddGroup.lift (S, f, hf) applied to x in the quotient group M / S is less than or equal to the product of the norm of f and the norm of x.
|
NormedAddGroupHom.IsQuotient.norm_le
theorem NormedAddGroupHom.IsQuotient.norm_le :
∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
{f : NormedAddGroupHom M N}, f.IsQuotient → ∀ (m : M), ‖f m‖ ≤ ‖m‖
This theorem states that for any two types `M` and `N`, which are seminormed additive commutative groups, and any normed additive group homomorphism `f` from `M` to `N` that is a quotient map, the norm of `f(m)` is less than or equal to the norm of `m` for any element `m` in `M`. In mathematical terms, this means that the norm (denoted by ‖·‖) is a non-increasing function under the homomorphism `f`.
More concisely: For any seminormed additive commutative groups M and N, and any normed additive group homomorphism f from M to N that is a quotient map, the map f preserves the norm, i.e., ‖f(m)‖ ≤ ‖m‖ for all m in M.
|
AddSubgroup.surjective_normedMk
theorem AddSubgroup.surjective_normedMk :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), Function.Surjective ⇑S.normedMk
The theorem `AddSubgroup.surjective_normedMk` states that for any additive subgroup `S` in a semi-normed additive commutative group `M`, the normed map `S.normedMk` is surjective. In other words, for every element in the codomain of the normed map, there exists an element in `S` such that applying `S.normedMk` to this element yields the given element in the codomain.
More concisely: For any additive subgroup `S` of a semi-normed additive commutative group `M`, the normed map `S.normedMk` is a surjection.
|
norm_mk_zero
theorem norm_mk_zero : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), ‖0‖ = 0
This theorem states that for any given semi-normed additive commutative group `M` and any additive subgroup `S` of `M`, the quotient norm of the zero element is zero. In terms of mathematical language, it is expressed as ‖0‖ = 0, where ‖·‖ is the norm function.
More concisely: For any semi-normed additive commutative group `M` and its subgroup `S`, the norm of the zero element is zero.
|
AddSubgroup.norm_normedMk_le
theorem AddSubgroup.norm_normedMk_le :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), ‖S.normedMk‖ ≤ 1
This theorem states that, for any additive subgroup `S` of a seminormed additive commutative group `M`, the operator norm of the projection (`normedMk`) onto that subgroup is always less than or equal to `1`. In other words, it asserts a bound on how large the operator norm can be when projecting onto an additive subgroup in a seminormed additive commutative group.
More concisely: For any additive subgroup `S` of a seminormed additive commutative group `M`, the operator norm of the projection onto `S` is bounded by 1.
|
norm_mk_lt
theorem norm_mk_lt :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M ⧸ S) {ε : ℝ},
0 < ε → ∃ m, (QuotientAddGroup.mk' S) m = x ∧ ‖m‖ < ‖x‖ + ε
The theorem `norm_mk_lt` states that for any element `x` of the quotient group `M/S` of a given seminormed additve commutative group `M` by an additive subgroup `S`, and for any real number `ε` greater than zero, there exists an element `m` of `M` such that the image of `m` under the additive group homomorphism from `M` to `M/S` is `x` and the norm of `m` is less than the norm of `x` plus `ε`. This theorem essentially states that we can find an approximation of `x` in `M` that is arbitrarily close in norm.
More concisely: For any seminormed additive commutative group `M` with subgroup `S`, and for any element `x` in `M/S` and real `ε > 0`, there exists an element `m` in `M` such that `norm m < norm x + ε` and `x = m % S`, where `%` denotes the quotient group operation.
|
quotient_norm_neg
theorem quotient_norm_neg :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M ⧸ S), ‖-x‖ = ‖x‖
This theorem states that the norm on the quotient of a seminormed additive commutative group satisfies the property that the norm of the additive inverse of an element is equal to the norm of the element itself. In other words, for any seminormed additive commutative group `M` and any additive subgroup `S` of `M`, if `x` is any element of the quotient group `M/S`, then the norm of `-x` (the additive inverse of `x`) is equal to the norm of `x`.
More concisely: In a seminormed additive commutative group, the norm of the additive inverse of any element in the quotient group equals the norm of the element itself.
|
AddSubgroup.norm_normedMk
theorem AddSubgroup.norm_normedMk :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M),
↑S.topologicalClosure ≠ Set.univ → ‖S.normedMk‖ = 1
The theorem `AddSubgroup.norm_normedMk` states that for any seminormed additive commutative group `M` and any additive subgroup `S` of `M`, if the topological closure of `S` does not equal the universal set (meaning that `S` is not dense in `M`), then the operator norm of the canonical map `S.normedMk` (which maps `S` to the quotient space `M/S`) is `1`.
More concisely: If a subgroup of a seminormed additive commutative group is not dense, then the operator norm of the canonical map to the quotient space is equal to 1.
|
quotient_norm_mk_le'
theorem quotient_norm_mk_le' :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M), ‖↑m‖ ≤ ‖m‖
The theorem `quotient_norm_mk_le'` states that for any seminormed additive commutative group `M` and any additive subgroup `S` of `M`, the norm of the projection of any element `m` of `M` onto the quotient group `M/S` is less than or equal to the norm of the original element `m` in `M`. In mathematical notation, this would be expressed as ‖↑m‖ ≤ ‖m‖.
More concisely: The norm of the projection of any element in a seminormed additive commutative group is less than or equal to the norm of the original element.
|
quotient_norm_nonneg
theorem quotient_norm_nonneg :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (x : M ⧸ S), 0 ≤ ‖x‖
This theorem states that the quotient norm is always nonnegative. More specifically, for any type `M` that forms a seminormed additive commutative group and any additive subgroup `S` of `M`, if you take a quotient `x` of `M` by `S`, then the norm of `x` (denoted by ‖x‖) is always greater than or equal to zero.
More concisely: For any seminormed additive commutative group `M` and its additive subgroup `S`, the quotient norm of any element `x` in `M` by `S` is nonnegative, that is, ‖x‖ ≥ 0.
|
AddSubgroup.norm_trivial_quotient_mk
theorem AddSubgroup.norm_trivial_quotient_mk :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M),
↑S.topologicalClosure = Set.univ → ‖S.normedMk‖ = 0
This theorem states that for any type `M` that forms a seminormed additive commutative group, and any additive subgroup `S` of `M`, if the topological closure of `S` equals the universal set (which means `S` is dense), then the operator norm of the canonical quotient map from `M` to `M/S` (represented by `S.normedMk`) is `0`.
More concisely: If `M` is a seminormed additive commutative group and `S` is a dense additive subgroup of `M`, then the operator norm of the quotient map from `M` to `M/S` is 0.
|
quotient_norm_eq_zero_iff
theorem quotient_norm_eq_zero_iff :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M),
‖(QuotientAddGroup.mk' S) m‖ = 0 ↔ m ∈ closure ↑S
Here is the translation in natural language:
The theorem `quotient_norm_eq_zero_iff` states that for any type `M` that is a seminormed additive commutative group, any additive subgroup `S` of `M`, and any element `m` from `M`, the norm of the image of `m` under the additive group homomorphism from `M` to the quotient group `M/S` is zero if and only if `m` belongs to the closure of `S`. In other words, the norm of the equivalence class of `m` in the quotient group `M/S` is zero precisely when `m` is in the smallest closed set containing `S`.
More concisely: For any seminormed additive commutative group (M, ||.||), subgroup S of M, and element m in M, the norm ||m|| = 0 in M/S if and only if m is in the closure of S.
|
AddSubgroup.ker_normedMk
theorem AddSubgroup.ker_normedMk :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), S.normedMk.ker = S
This theorem states that for any given seminormed additive commutative group `M` and any additive subgroup `S` of `M`, the kernel of the morphism from `M` to the quotient group `M / S` (generated by the `normedMk` function applied to `S`) is exactly `S` itself. Here, the kernel of a group homomorphism is the set of all elements in the domain that map to the identity in the codomain.
More concisely: The kernel of the quotient homomorphism from a seminormed additive commutative group to its quotient by an additive subgroup equals the subgroup itself.
|
quotient_norm_add_le
theorem quotient_norm_add_le :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (x y : M ⧸ S), ‖x + y‖ ≤ ‖x‖ + ‖y‖ := by
sorry
This theorem states that for any seminormed add commutative group `M` and any additive subgroup `S` of `M`, the norm of the sum of any two elements in the quotient group `M ⧸ S` is less than or equal to the sum of their norms. This is a formalization of the triangle inequality in the context of quotient norms.
More concisely: For any seminormed add commutative group `M`, and additive subgroup `S` of `M`, the quotient norm of the sum of any two elements in `M ⧸ S` is less than or equal to the sum of their quotient norms.
|
norm_mk_nonneg
theorem norm_mk_nonneg :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M), 0 ≤ ‖(QuotientAddGroup.mk' S) m‖
This theorem states that the quotient norm is nonnegative. Specifically, for any seminormed add commutative group `M`, any additive subgroup `S` of `M`, and any element `m` of `M`, the norm of the image of `m` under the additive group homomorphism from `M` to `M/S` (denoted by `QuotientAddGroup.mk' S`) is greater than or equal to zero. In mathematical terms, $0 \leq \| (QuotientAddGroup.mk' S) m \|$.
More concisely: For any seminormed add commutative group `M`, any additive subgroup `S` of `M`, and any element `m` in `M`, the norm of the quotient `QuotientAddGroup.mk' S m` is nonnegative. That is, $\| QuotientAddGroup.mk' S(m) \| \geq 0$.
|
quotient_norm_mk_le
theorem quotient_norm_mk_le :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M),
‖(QuotientAddGroup.mk' S) m‖ ≤ ‖m‖
The theorem `quotient_norm_mk_le` states that, for any semi-normed additive commutative group `M` and any additive subgroup `S` of `M`, and for any element `m` of `M`, the norm of the projection of `m` onto the quotient group `M/S` (obtained using the additive group homomorphism `QuotientAddGroup.mk'` from `M` to `M/S`) is less than or equal to the norm of `m`. This means the norm does not increase when an element is projected from the group to a quotient group.
More concisely: For any semi-normed additive commutative group M, additive subgroup S, and element m in M, the norm of the projection of m to the quotient group M/S using QuotientAddGroup.mk' is less than or equal to the norm of m.
|
QuotientAddGroup.norm_mk
theorem QuotientAddGroup.norm_mk :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M), ‖↑x‖ = Metric.infDist x ↑S := by
sorry
This theorem establishes an alternative definition of the norm on a quotient group. Specifically, within the context of a semi-normed additive commutative group `M` and a defined additive subgroup `S` of `M`, the norm of an element `x` from `M` when considered as part of the quotient group `M ⧸ S` is equal to the minimum distance from `x` to the set `S`. The minimum distance is measured using the `Metric.infDist` function. In other words, for every `x` in `M`, the norm of `x` in the quotient group `M ⧸ S` is equal to the minimum distance of `x` to `S`.
More concisely: For any semi-normed additive commutative group `M`, additive subgroup `S` of `M`, and `x` in `M`, the norm of `x` in the quotient group `M / S` is equal to the minimum distance from `x` to `S` using the `Metric.infDist` function.
|
AddSubgroup.normedMk.apply
theorem AddSubgroup.normedMk.apply :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M),
S.normedMk m = (QuotientAddGroup.mk' S) m
The theorem `AddSubgroup.normedMk.apply` states that for all seminormed additive commutative groups `M` and any additive subgroup `S` of `M`, and for any element `m` in `M`, the application of `S.normedMk` on `m` is equal to the application of `QuotientAddGroup.mk' S` on `m`. In other words, the mapping of any element of the group `M` to the quotient group `M/S` using the normed map `S.normedMk` is exactly the same as the mapping using the additive group homomorphism `QuotientAddGroup.mk' S`.
More concisely: The normed map `S.normedMk` on a seminormed additive commutative group `M` and its subgroup `S` is equal to the additive group homomorphism `QuotientAddGroup.mk' S`.
|
quotient_norm_mk_eq
theorem quotient_norm_mk_eq :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M),
‖(QuotientAddGroup.mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)
This theorem states that for any seminormed additive commutative group `M`, any additive subgroup `S` of `M`, and any element `m` of `M`, the norm of the image of `m` under the natural morphism to the quotient group `M/S` (represented by `QuotientAddGroup.mk' S m`) is equal to the infimum of the set of norms of `m + x` for all `x` in `S`. In other words, it describes the norm of an element in the quotient group in terms of the norms of elements in the original group.
More concisely: For any seminormed additive commutative group `M`, any additive subgroup `S` of `M`, and any element `m` in `M`, the norm of `m` in the quotient group `M/S` is equal to the infimum of the norms of `m + x` for all `x` in `S`.
|
norm_mk_eq_zero
theorem norm_mk_eq_zero :
∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M),
IsClosed ↑S → ∀ (m : M), ‖(QuotientAddGroup.mk' S) m‖ = 0 → m ∈ S
This theorem states that for any type `M` that is a seminormed additive commutative group, and any additive subgroup `S` of `M` which is closed, if an element `m` from `M` is mapped to `0` under the quotient norm (i.e., its norm in the quotient group `M ⧸ S` is `0`), then the element `m` must be a member of the subgroup `S`. In mathematical notation, if `M` is a seminormed additive commutative group, `S` is a closed additive subgroup of `M`, and for some `m` in `M` we have ‖(QuotientAddGroup.mk' S) m‖ = 0, then `m` belongs to `S`.
More concisely: If `M` is a seminormed additive commutative group, `S` is a closed additive subgroup of `M`, and the quotient norm of `m` in `M ⧸ S` is 0, then `m` is in `S`.
|