isBounded_iff_forall_norm_le
theorem isBounded_iff_forall_norm_le :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C := by
sorry
This theorem, `isBounded_iff_forall_norm_le`, states that for any set `s` in a seminormed add group `E`, the set `s` is bounded relative to the ambient bornology on `E` if and only if there exists a real number `C` such that for all elements `x` in the set `s`, the seminorm (or "length") of `x` is less than or equal to `C`. This essentially means that every element in set `s` has a "length" that does not exceed a certain upper bound `C`.
More concisely: A set `s` in a seminormed add group `E` is bounded relative to the ambient bornology if and only if there exists a real number `C` such that the seminorm of every element `x` in `s` is less than or equal to `C`.
|
Real.nnnorm_of_nonneg
theorem Real.nnnorm_of_nonneg : ∀ {r : ℝ} (hr : 0 ≤ r), ‖r‖₊ = ⟨r, hr⟩
This theorem states that for every real number `r` that is non-negative (i.e., greater than or equal to zero), the non-negative norm of `r` (denoted as ‖r‖₊) is equal to the non-negative real number that has `r` as its value and the property that `r` is non-negative. This means that the non-negative norm of a non-negative real number is simply the number itself, wrapped in a structure that explicitly confirms its non-negativity.
More concisely: For every non-negative real number `r`, the non-negative norm `‖r‖₊` equals `r`.
|
MonoidHomClass.isometry_of_norm
theorem MonoidHomClass.isometry_of_norm :
∀ {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
[inst_2 : FunLike 𝓕 E F] [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕), (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f
The theorem `MonoidHomClass.isometry_of_norm` states that for any types `𝓕`, `E` and `F`, where `E` and `F` are seminormed groups, `𝓕` is a type that behaves like a function from `E` to `F`, and there is a monoid homomorphism from `𝓕` to the function type `E → F`, then a term `f` of type `𝓕` is an isometry (i.e., a map that preserves the distance between two points in a pseudometric space) if and only if the norm of `f(x)` is equal to the norm of `x` for all `x` in `E`. This is a reverse alias of the theorem `MonoidHomClass.isometry_iff_norm`.
More concisely: A function `f` from a seminormed group `E` to another seminormed group `F`, which is a monoid homomorphism and behaves like a function, is an isometry if and only if the norm of `f(x)` equals the norm of `x` for all `x` in `E`.
|
HasCompactSupport.norm
theorem HasCompactSupport.norm :
∀ {α : Type u_3} {E : Type u_6} [inst : NormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
HasCompactSupport f → HasCompactSupport fun x => ‖f x‖
The theorem `HasCompactSupport.norm` states that for any types `α` and `E`, where `E` is a normed add group and `α` is a topological space, and for any function `f` from `α` to `E`, if `f` has compact support, then the function that maps each `x` in `α` to the norm of `f(x)` also has compact support. In other words, if the closure of the support of function `f` is compact, then the closure of the support of the function that computes the norm of `f(x)` is also compact.
More concisely: If `f` is a continuous function from a compact topological space `α` to a normed additive group `E` with compact support, then the function `x => ||f(x)||` also has compact support.
|
Filter.Tendsto.norm
theorem Filter.Tendsto.norm :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E},
Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => ‖f x‖) l (nhds ‖a‖)
This theorem, `Filter.Tendsto.norm`, states that for any seminormed add group `E` and any filter `l` in an arbitrary type `α`, if a function `f : α → E` tends to a value `a` in `E` as `l` tends to infinity, then the norm of `f`, i.e. `‖f x‖`, tends to the norm of `a`, `‖a‖`, as `l` also tends to infinity. This is a formalization of the common mathematical fact that in normed vector spaces, the limit of the norm of a sequence of vectors is equal to the norm of the limit of the sequence, assuming the limit exists.
More concisely: If a function from a filter in a seminormed add group to the same group tends to a limit in the group, then the sequence of norms of the function's values tends to the norm of the limit.
|
NormedAddGroup.dist_eq
theorem NormedAddGroup.dist_eq : ∀ {E : Type u_9} [self : NormedAddGroup E] (x y : E), dist x y = ‖x - y‖
This theorem states that for any type `E` that forms a Normed Additive Group, the distance function between any two elements `x` and `y` of `E` is equal to the norm of the difference between `x` and `y`. In other words, in any normed additive group, the distance between two elements is simply the norm of their difference.
More concisely: In a normed additive group, the distance between two elements is equal to the norm of their difference.
|
pi_norm_lt_iff'
theorem pi_norm_lt_iff' :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (π i)]
{x : (i : ι) → π i} {r : ℝ}, 0 < r → (‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r)
This theorem states that for a given product space (indexed by some type `ι` where each component is a seminormed group), the norm of an element in this space is less than a positive real number `r` if and only if the norm of each of the element's components is less than `r`. This links the seminorm of the whole space's element to the seminorms of its components.
More concisely: For a product space of seminormed groups indexed by type `ι`, an element's norm is less than a positive real number `r` if and only if the norm of each of its components is less than `r`.
|
norm_nonneg
theorem norm_nonneg : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), 0 ≤ ‖a‖
This theorem states that for any type `E` which forms a seminormed add group, the norm of any element `a` of `E` is always non-negative. In mathematical terms, this means that for every element `a` in a seminormed add group `E`, the inequality 0 ≤ ‖a‖ always holds.
More concisely: In a seminormed add group, the norm of any element is non-negative.
|
dist_add_add_le
theorem dist_add_add_le :
∀ {E : Type u_6} [inst : SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E),
dist (a₁ + a₂) (b₁ + b₂) ≤ dist a₁ b₁ + dist a₂ b₂
This theorem states that for any type `E`, which forms a seminormed add commutative group, the distance between the sum of two elements `a₁` and `a₂` and the sum of two elements `b₁` and `b₂` is less than or equal to the sum of the distances between `a₁` and `b₁` and `a₂` and `b₂`. This is a generalization of the triangle inequality to seminormed add commutative groups.
More concisely: For any seminormed add commutative group `E` and elements `a₁, a₂, b₁, b₂` in `E`, the inequality `dist (a₁ + a₂, b₁ + b₂) ≤ dist (a₁, b₁) + dist (a₂, b₂)` holds.
|
norm_le_zero_iff
theorem norm_le_zero_iff : ∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, ‖a‖ ≤ 0 ↔ a = 0
This theorem states that for any entity `a` of a certain type `E`, where `E` is a normed group, the norm of `a` is less than or equal to zero if and only if `a` is zero. A normed group is a group in which distance and subtraction operations are defined in a way that satisfies certain conditions. Essentially, this theorem is saying that in these mathematical structures, the only entity with a norm (or length) of zero or less is the zero entity itself.
More concisely: In a normed group, an entity has zero norm if and only if it is the additive identity.
|
tendsto_zero_iff_norm_tendsto_zero
theorem tendsto_zero_iff_norm_tendsto_zero :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] {f : α → E} {a : Filter α},
Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun x => ‖f x‖) a (nhds 0)
The theorem `tendsto_zero_iff_norm_tendsto_zero` states that for any seminormed additive group `E`, any type `α`, any function `f` from `α` to `E`, and any filter `a` on `α`, the function `f` tends towards zero at the filter `a` if and only if the norm of the function `f` also tends towards zero at the same filter `a`. In other words, a function's values get arbitrarily close to zero under the filter if and only if their norms also get arbitrarily close to zero.
More concisely: For any seminormed additive group `E`, function `f` from type `α` to `E`, and filter `a` on `α`, the function `f` tends towards zero at `a` if and only if the norm of `f` tends towards zero at `a`.
|
norm_div_rev
theorem norm_div_rev : ∀ {E : Type u_6} [inst : SeminormedGroup E] (a b : E), ‖a / b‖ = ‖b / a‖
This theorem, `norm_div_rev`, states that for any type `E` that forms a Semi-normed group, the norm of the result of dividing `a` by `b` is equal to the norm of the result of dividing `b` by `a`. In more mathematical terms, this is equivalent to stating that for any elements `a` and `b` in `E`, the norm of `a / b` (denoted as ‖a / b‖) is equal to the norm of `b / a` (denoted as ‖b / a‖).
More concisely: For any type `E` forming a Semi-normed group and elements `a`, `b` in `E` with `b ≠ 0`, the norms of `a / b` and `b / a` are equal: ‖`a / b`‖ = ‖`b / a`‖.
|
MonoidHomClass.continuous_of_bound
theorem MonoidHomClass.continuous_of_bound :
∀ {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
[inst_2 : FunLike 𝓕 E F] [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ),
(∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → Continuous ⇑f
The theorem `MonoidHomClass.continuous_of_bound` states that for any seminormed groups `E` and `F`, if there is a homomorphism `f` from `E` to `F` and a real number `C` such that the norm of `f(x)` is less than or equal to `C` times the norm of `x` for all `x` in `E`, then `f` is continuous. Here, the homomorphism `f` is defined as a function-like element of type `𝓕` that adheres to the `MonoidHomClass`, which specifies that it preserves the monoid structure under the operation.
More concisely: If `f` is a homomorphism from a seminormed group `E` to a seminormed group `F` such that `∀x ∈ E, ||f x|| ≤ C ||x||`, then `f` is continuous.
|
norm_le_zero_iff'
theorem norm_le_zero_iff' :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : T0Space E] {a : E}, ‖a‖ ≤ 0 ↔ a = 0
This theorem states that for any type `E` that is a seminormed add group and a `T0` topological space, the norm of an element `a` of `E` is less than or equal to zero if and only if `a` is equal to zero. In mathematical terms, this theorem says that for all seminormed add groups (which are also `T0` spaces) `E` and all elements `a` of `E`, the condition `‖a‖ ≤ 0` is equivalent to `a = 0`.
More concisely: In a seminormed add group and a T0 topological space, an element has zero norm if and only if it is the zero element.
|
LipschitzWith.add
theorem LipschitzWith.add :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
{f g : α → E}, LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) fun x => f x + g x
The theorem `LipschitzWith.add` states that for any type `α` and a semi-normed add commutative group `E`, given two nonnegative real numbers `Kf` and `Kg`, and two functions `f` and `g` that are Lipschitz continuous with constants `Kf` and `Kg` respectively, the function that maps any element `x` of type `α` to the sum of `f x` and `g x` is also Lipschitz continuous with the constant being the sum of `Kf` and `Kg`. In other words, the addition of two Lipschitz continuous functions is also Lipschitz continuous, with the Lipschitz constant being the sum of the Lipschitz constants of the two functions.
More concisely: If `f` and `g` are Lipschitz continuous functions with constants `Kf` and `Kg` respectively on a semi-normed additive commutative group `E`, then their sum `h(x) = f(x) + g(x)` is a Lipschitz continuous function with constant `Kf + Kg`.
|
Filter.Tendsto.op_zero_isBoundedUnder_le
theorem Filter.Tendsto.op_zero_isBoundedUnder_le :
∀ {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [inst : SeminormedAddGroup E]
[inst_1 : SeminormedAddGroup F] [inst_2 : SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α},
Filter.Tendsto f l (nhds 0) →
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g) →
∀ (op : E → F → G),
(∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 0)
This theorem states that for any types `α`, `E`, `F`, and `G`, where `E`, `F`, and `G` are seminormed additive groups, given a filter `l` over `α` and functions `f : α → E` and `g : α → F`, if `f` tends to zero with respect to the filter `l` and the norm of `g` is bounded under the filter `l`, then for any binary operation `op : E → F → G` that satisfies a specific inequality related to norms (namely, the norm of the operation applied to any `x : E` and `y : F` is less than or equal to the product of the norms of `x` and `y`), the function that maps `x` in the domain of the filter to the operation applied to `f(x)` and `g(x)` also tends to zero with respect to `l`. In layman's terms, it states that the product of a function tending to zero and a bounded function also tends to zero under specific conditions.
More concisely: If `f : α → E` tends to zero under filter `l` and the norm of `g : α → F` is bounded under `l`, then the function `x ↦ op(f(x), g(x))` tends to zero under `l`, given `op : E → F → G` satisfying the norm inequality: ||op(x, y)|| ≤ ||x|| * ||y|| for all `x : E` and `y : F`.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.22
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.22 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
This theorem states that for any types `α` and `β`, a function `f` from `α` to `β`, a set `s` of type `β`, and an element `a` of type `α`, the statement "element `a` is in the preimage of set `s` under function `f`" is equivalent to the statement "the result of applying function `f` to element `a` is in set `s`". In mathematical terms, we can express this as $a \in f^{-1}(s) \Leftrightarrow f(a) \in s$.
More concisely: For any functions $f: \alpha \to \beta$ and sets $s \subseteq \beta$, the elements $a \in \alpha$ satisfy $a \in f^{-1}(s) \Leftrightarrow f(a) \in s$.
|
ne_zero_of_mem_unit_sphere
theorem ne_zero_of_mem_unit_sphere :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] (x : ↑(Metric.sphere 0 1)), ↑x ≠ 0
This theorem states that for any seminormed additive group `E`, any point `x` on the unit sphere centered at zero (i.e., the set of all points at a distance 1 from the origin) is not equal to the zero vector. In other words, there are no points on the unit sphere that are also at the origin.
More concisely: The theorem asserts that that the unit sphere of a seminormed additive group `E` contains no point equal to the zero vector.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.30
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.30 :
∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, (‖a‖ = 0) = (a = 0)
This theorem, named `Mathlib.Analysis.Normed.Group.Basic._auxLemma.30`, states that for any type `E` that is a normed additive group, the norm of an element `a` from `E` is zero if and only if `a` itself is the zero element of the group. In mathematical notation, this could be written as ‖a‖ = 0 if and only if a = 0.
More concisely: For any normed additive group E and its element a, the norm of a is zero if and only if a is the additive identity of E.
|
dist_eq_norm_div
theorem dist_eq_norm_div : ∀ {E : Type u_6} [inst : SeminormedGroup E] (a b : E), dist a b = ‖a / b‖
This theorem states that in any semi-normed group `E`, the distance between two elements `a` and `b` of `E` is equal to the norm of their division (`a / b`). Here, `dist` represents the metric or distance function, and `‖a / b‖` represents the norm (or length) of the element resulting from the division of `a` and `b`.
More concisely: In a semi-normed group, the distance between two elements is equal to the norm of their quotient.
|
norm_nonneg'
theorem norm_nonneg' : ∀ {E : Type u_6} [inst : SeminormedGroup E] (a : E), 0 ≤ ‖a‖
This theorem states that for any type `E` that is a seminormed group, the norm of any element `a` of `E` is nonnegative. In other words, for every element in a seminormed group, its norm is always greater than or equal to zero. This is symbolically represented in LaTeX as, ∀a ∈ E, 0 ≤ ‖a‖.
More concisely: In a seminormed group, the norm of every element is nonnegative. (∀a ∈ E, 0 ≤ ‖a‖)
|
norm_le_zero_iff'''
theorem norm_le_zero_iff''' :
∀ {E : Type u_6} [inst : SeminormedGroup E] [inst_1 : T0Space E] {a : E}, ‖a‖ ≤ 0 ↔ a = 1
This theorem states that for any type `E` that forms a semi-normed group with a `T0` topological space, the norm of an element `a` of `E` is less than or equal to zero if and only if `a` is equal to 1. In mathematical terms, this means that for all elements of a semi-normed group in a particular topological space, the norm of an element being less than or equal to zero is equivalent to that element being unity.
More concisely: In a semi-normed group endowed with a T0 topology, an element has zero norm if and only if it is the identity.
|
Subgroup.norm_coe
theorem Subgroup.norm_coe : ∀ {E : Type u_6} [inst : SeminormedGroup E] {s : Subgroup E} (x : ↥s), ‖↑x‖ = ‖x‖ := by
sorry
This theorem states that if 'x' is an element of a subgroup 's' of a seminormed group 'E', then its norm in the subgroup 's' is the same as its norm in the entire group 'E'. This is essentially a reversed version of the `simp` lemma `Subgroup.coe_norm` that is used by `norm_cast`. The theorem serves to ensure the consistency of the definition of a norm across a group and its subgroups.
More concisely: If x is an element of a subgroup s of a seminormed group E, then the norm of x in s equals its norm in E.
|
lipschitzWith_one_norm
theorem lipschitzWith_one_norm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E], LipschitzWith 1 norm
The theorem `lipschitzWith_one_norm` states that for any type `E` that is a `SeminormedAddGroup`, the norm function is Lipschitz continuous with a Lipschitz constant of 1. In the context of mathematics, this means that for all elements `x` and `y` in `E`, the distance between the norms of `x` and `y` (i.e., `||x||` and `||y||`) is less than or equal to the distance between `x` and `y` itself. This property is a key feature of norms in seminormed groups.
More concisely: For any `SeminormedAddGroup` `E`, the norm function `||.||` is 1-Lipschitz continuous, i.e., `||x - y|| ≤ ||x - y||_1 + ||y - x||`, where `||.||_1` denotes the 1-norm on `E`.
|
norm_add_le_of_le
theorem norm_add_le_of_le :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ},
‖a₁‖ ≤ r₁ → ‖a₂‖ ≤ r₂ → ‖a₁ + a₂‖ ≤ r₁ + r₂
The theorem `norm_add_le_of_le` states that for any type `E` that has a structure of a seminormed addition group, given two elements `a₁` and `a₂` of `E`, and two real numbers `r₁` and `r₂`, if the norm of `a₁` is less than or equal to `r₁` and the norm of `a₂` is less than or equal to `r₂`, then the norm of the sum `a₁ + a₂` is less than or equal to the sum `r₁ + r₂`. This is essentially a statement about the triangle inequality in the context of seminormed addition groups.
More concisely: For any seminormed addition group (E, +, ||.||) and elements a₁, a₂ in E, and real numbers r₁, r₂ such that ||a₁|| ≤ r₁ and ||a₂|| ≤ r₂, it holds that ||a₁ + a₂|| ≤ r₁ + r₂.
|
tendsto_norm_cobounded_atTop
theorem tendsto_norm_cobounded_atTop :
∀ {E : Type u_6} [inst : SeminormedAddGroup E], Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop
The theorem `tendsto_norm_cobounded_atTop` states that for any type `E` that has a seminormed add group structure, the norm function, when applied to the cobounded sets in the bornology of `E`, tends to infinity. In simpler terms, this means that as we take larger and larger sets in the bornology (sets which are cobounded), the norm of the elements in those sets tends to infinity. This is a formal way of expressing that the norm grows without bound when considering larger sets in the bornology structure.
More concisely: For any seminormed add group `E`, the norm function tends to infinity as the sets in `E`'s bornology become cobounded.
|
Filter.Tendsto.op_zero_isBoundedUnder_le'
theorem Filter.Tendsto.op_zero_isBoundedUnder_le' :
∀ {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [inst : SeminormedAddGroup E]
[inst_1 : SeminormedAddGroup F] [inst_2 : SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α},
Filter.Tendsto f l (nhds 0) →
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g) →
∀ (op : E → F → G),
(∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 0)
This theorem refers to the situation where you have two functions (`f` and `g`), and a binary operation (`op`). The function `f` has the property that it tends to zero. The function `g` is bounded under a relation that defines an order (one value is less than or equal to another). Also, the binary operation `op` has an upper bound estimated by `A * ‖x‖ * ‖y‖` for some constant `A`.
The theorem states that, under these conditions, the function resulting from applying the binary operation `op` to the outputs of `f` and `g` (namely `(f x) (g x)`), also tends to zero. This theorem is generalizable to any binary operation that satisfies the condition, including multiplication, scalar multiplication and their flipped versions.
More concisely: If `f` and `g` are functions with `f` tending to zero, `g` is bounded, and `op` is a binary operation with an upper bound `A * ‖x‖ * ‖y‖, then the composition `(f x) (g x)` tends to zero for all `x`.
|
comap_norm_atTop
theorem comap_norm_atTop :
∀ {E : Type u_6} [inst : SeminormedAddGroup E], Filter.comap norm Filter.atTop = Bornology.cobounded E
The theorem `comap_norm_atTop` states that for any type `E` which forms a seminormed add group, the filter of the preimage of the filter at infinity (`Filter.atTop`) under the norm function is equal to the filter of cobounded sets in the bornology of `E`. In other words, the norm function maps cobounded sets in `E` to sets that are unbounded above. This reveals a relationship between the norm of a seminormed group and its associated bornology.
More concisely: For any seminormed add group `E`, the preimage of the filter at infinity under the norm function equals the filter of cobounded sets in `E`'s bornology.
|
norm_le_pi_norm
theorem norm_le_pi_norm :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (π i)]
(f : (i : ι) → π i) (i : ι), ‖f i‖ ≤ ‖f‖
This theorem states that for any finite type `ι`, and any map `f` from `ι` to a seminormed add group `π i`, the norm of `f i` is always less than or equal to the norm of `f`. In other words, the norm of any individual element in the range of `f` is bounded above by the overall norm of the function `f`. This theorem holds true for every element `i` in the finite type `ι`.
More concisely: For any finite type `ι` and map `f` from `ι` to a seminormed add group `π i`, the maximum norm of `f i` over all `i` in `ι` is less than or equal to the norm of `f`.
|
mem_sphere_zero_iff_norm
theorem mem_sphere_zero_iff_norm :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, a ∈ Metric.sphere 0 r ↔ ‖a‖ = r
The theorem `mem_sphere_zero_iff_norm` states that for any seminormed add group `E` and any elements `a` of `E` and real number `r`, `a` is in the sphere centered at zero with radius `r` in the metric space if and only if the norm of `a` is equal to `r`. In other words, an element belongs to this particular sphere if its norm equals the radius of the sphere.
More concisely: An element `a` in a seminormed add group `E` belongs to the sphere centered at zero with radius `r` if and only if the norm of `a` is equal to `r`.
|
pi_norm_le_iff_of_nonneg
theorem pi_norm_le_iff_of_nonneg :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (π i)]
{x : (i : ι) → π i} {r : ℝ}, 0 ≤ r → (‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r)
This theorem, `pi_norm_le_iff_of_nonneg`, states that for a given non-negative real number `r`, and a given element `x` of a product space (where the product space is defined over a finite type `ι`, with each component being an element of a seminormed add group), the seminorm of `x` is less than or equal to `r` if and only if the norm of each component of `x` is less than or equal to `r`. In mathematical terms, if `0 ≤ r`, then `‖x‖ ≤ r` is equivalent to the condition that for all `i` in `ι`, `‖x i‖ ≤ r`.
More concisely: For a non-negative real number `r` and an element `x` of a product space over a finite type `ι`, where each component is an element of a seminormed add group, `‖x‖ ≤ r` if and only if for all `i` in `ι`, `‖x i‖ ≤ r`.
|
nnnorm_ne_zero_iff
theorem nnnorm_ne_zero_iff : ∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, ‖a‖₊ ≠ 0 ↔ a ≠ 0
This theorem states that for any Type `E` which is a `NormedAddGroup`, the nonnegative norm, denoted as `‖a‖₊`, of an element `a` from `E` is not equal to zero if and only if `a` is not equal to zero. In other words, an element of the `NormedAddGroup` is zero if and only if its nonnegative norm is also zero.
More concisely: For any `NormedAddGroup` `E`, the nonnegative norm of an element `a` is zero if and only if `a` is the additive identity of `E`.
|
AddMonoidHomClass.lipschitz_of_bound
theorem AddMonoidHomClass.lipschitz_of_bound :
∀ {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
[inst_2 : FunLike 𝓕 E F] [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ),
(∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → LipschitzWith C.toNNReal ⇑f
This theorem states that a homomorphism `f` of seminormed groups is Lipschitz continuous if there exists a constant `C` such that for all elements `x`, the norm of `f x` is less than or equal to `C` times the norm of `x`. Here, Lipschitz continuity is defined as a function `f` being Lipschitz continuous with constant `K ≥ 0` if for all `x, y` we have `dist (f x) (f y) ≤ K * dist x y`. The constant `C` is interpreted as a non-negative real number using the `Real.toNNReal` function, which returns `0` if `C < 0`. This concept is analogous to a condition for linear maps of (semi)normed spaces, which can be found in `Mathlib/Analysis/NormedSpace/OperatorNorm.lean`.
More concisely: A homomorphism between seminormed groups is Lipschitz continuous if there exists a constant `C` such that the norm of the image under the homomorphism is bounded by `C` times the norm of the argument.
|
Real.norm_coe_nat
theorem Real.norm_coe_nat : ∀ (n : ℕ), ‖↑n‖ = ↑n
This theorem states that for any natural number 'n', the norm (or absolute value) of 'n' when it is coerced (or converted) into a real number is equal to 'n' itself as a real number. Essentially, this means that the absolute value of any natural number is just the number itself when both are considered as real numbers.
More concisely: For any natural number n, |n| = n, where |.| denotes the absolute value function.
|
Pi.sum_nnnorm_apply_le_nnnorm
theorem Pi.sum_nnnorm_apply_le_nnnorm :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (π i)]
(f : (i : ι) → π i), (Finset.univ.sum fun i => ‖f i‖₊) ≤ Fintype.card ι • ‖f‖₊
This theorem states that for every function `f` from an index set `ι` to a type `π i` (where `i` is an element from `ι`), the $L^1$ norm of `f` is less than or equal to the $L^\infty$ norm of `f` scaled by the cardinality of the index set `ι`. The $L^1$ norm is represented by the summation of the norms of `f i` for all `i` in `ι`, and the $L^\infty$ norm is represented by the norm of `f`. Here, `ι` is a finite type, and `π i` is a seminormed add group for each `i` in `ι`.
More concisely: For every function `f` from a finite index set `ι` to a seminormed add group `π i`, the sum of the $L^1$ norms of `f i` over `ι` is less than or equal to the $L^\infty$ norm of `f` multiplied by the cardinality of `ι`.
|
norm_add_le
theorem norm_add_le : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), ‖a + b‖ ≤ ‖a‖ + ‖b‖
This is the Triangle Inequality for the norm in the context of semi-normed add groups. For any type `E` that forms a semi-normed add group, and any two elements `a` and `b` of type `E`, the norm of the sum of `a` and `b` is always less than or equal to the sum of the norms of `a` and `b`. Mathematically, this is expressed as ‖a + b‖ ≤ ‖a‖ + ‖b‖.
More concisely: For any semi-normed add group `E` and elements `a, b` in `E`, the triangle inequality holds: ‖a + b‖ ≤ ‖a‖ + ‖b‖.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.17
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.17 :
∀ {E : Type u_6} [inst : SeminormedGroup E] (a b : E), ‖a / b‖ = dist a b
This theorem, `Mathlib.Analysis.Normed.Group.Basic._auxLemma.17`, states that for any type `E` that is a semi-normed group, the norm of the ratio of any two elements `a` and `b` of `E` is equal to the distance between `a` and `b`. In mathematical notation, this is represented as ‖a / b‖ = dist(a, b).
More concisely: For any semi-normed group `E`, the norm of the quotient of two of its elements `a` and `b` is equal to the distance between `a` and `b`. That is, ‖a / b‖ = dist(a, b).
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.36
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.36 :
∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, (‖a‖₊ = 0) = (a = 0)
This theorem, from the Mathlib library in Analysis and Normed Group Basics, states that for any type `E` which forms a normed add group, the nonnegative real number norm (`‖a‖₊`) of an element `a` from `E` is equal to zero if and only if the element `a` itself is zero. It essentially connects the concepts of zero norm and the zero element in the context of normed add groups.
More concisely: For any normed add group `E`, the element `a` in `E` has norm 0 if and only if `a` is the additive identity of `E`.
|
NormedCommGroup.dist_eq
theorem NormedCommGroup.dist_eq : ∀ {E : Type u_9} [self : NormedCommGroup E] (x y : E), dist x y = ‖x / y‖
This theorem states that for any normed commutative group, the distance between two elements `x` and `y` is equal to the norm of the quotient `x / y`. Here, `E` is any type forming a normed commutative group, `x` and `y` are elements of `E`, and `‖x / y‖` denotes the norm of `x / y`. The distance function `dist` and the norm function (represented by ‖.‖) are both general concepts in mathematics, often used in spaces where one can measure "sizes" or "distances". In this context, the theorem relates these two concepts, showing they give the same result for any two elements of the group.
More concisely: For any normed commutative group (E, ‖.‖), and for all x, y in E with y ≠ 0, the distance between x and y is equal to the norm of x/y. That is, dist(x, y) = ‖x/y‖.
|
norm_eq_zero''
theorem norm_eq_zero'' : ∀ {E : Type u_6} [inst : NormedGroup E] {a : E}, ‖a‖ = 0 ↔ a = 1
This theorem states that for any type `E` that forms a Normed Group, the norm of an element `a` of `E` is equal to zero if and only if `a` is equal to one. In mathematical terms, given a Normed Group `(E, ‖·‖)`, it states that `‖a‖ = 0` if and only if `a = 1`. This theorem provides a characterization of the zero element in the Normed Group in terms of its norm.
More concisely: In a Normed Group `(E, ‖·‖)`, the element `a` has norm 0 if and only if `a` is the additive identity (i.e., `a = 1`).
|
pi_norm_le_iff_of_nonneg'
theorem pi_norm_le_iff_of_nonneg' :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (π i)]
{x : (i : ι) → π i} {r : ℝ}, 0 ≤ r → (‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r)
This theorem states that for a given element 'x' in a product space, generated over a finite type 'ι' with each component being a seminormed group, the seminorm of 'x' is less than or equal to a non-negative real number 'r' if and only if the norm of each individual component of 'x' is less than or equal to 'r'. In other words, it provides a condition on the seminorm of an element in a product space based on the norms of its individual components.
More concisely: For an element x in the product of seminormed groups indexed by a finite type ι, the seminorm of x is less than or equal to r if and only if the norm of each component of x is less than or equal to r.
|
Pi.sum_nnnorm_apply_le_nnnorm'
theorem Pi.sum_nnnorm_apply_le_nnnorm' :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (π i)]
(f : (i : ι) → π i), (Finset.univ.sum fun i => ‖f i‖₊) ≤ Fintype.card ι • ‖f‖₊
The theorem `Pi.sum_nnnorm_apply_le_nnnorm'` states that for any finite type `ι`, any function `f` from `ι` to a semi-normed group `π i`, the sum of the nonnegative norms of `f i` over all `i` in the finite set is less than or equal to the nonnegative norm of `f` scaled by the cardinality of `ι`. In simpler terms, the sum of norms of the function values is always less than or equal to the norm of the function itself times the size of the set over which the function is defined.
More concisely: For any finite type ι and any function f from ι to a semi-normed group π, the sum of the nonnegative norms of f i over i in ι is less than or equal to the nonnegative norm of f scaled by the cardinality of ι. In symbols: ∫i∈ι‖fi‖0 dι ≤ ‖f‖0 * |ι|.
|
SeminormedCommGroup.dist_eq
theorem SeminormedCommGroup.dist_eq : ∀ {E : Type u_9} [self : SeminormedCommGroup E] (x y : E), dist x y = ‖x / y‖
The theorem states that in a Seminormed Commutative Group (a commutative group that has a seminorm), the distance between two elements, `x` and `y`, is equal to the norm of the quotient of `x` and `y`. Here, the distance function and the norm function are related, where the distance is found by taking the norm of the quotient of two elements.
More concisely: In a Seminormed Commutative Group, the distance between two elements is equal to the norm of their quotient.
|
eq_of_norm_div_eq_zero
theorem eq_of_norm_div_eq_zero : ∀ {E : Type u_6} [inst : NormedGroup E] {a b : E}, ‖a / b‖ = 0 → a = b
This theorem, `eq_of_norm_div_eq_zero`, states that for any normed group `E` and any two elements `a` and `b` of `E`, if the norm of the ratio `a / b` is equal to zero, then `a` must be equal to `b`. Essentially, it's a theorem about the properties of division and norms in normed groups, and it asserts that the only way for the norm of a ratio to be zero is if the numerator and denominator are the same.
More concisely: In a normed group, if the norm of the quotient of two elements is zero, then the elements are equal.
|
mem_closedBall_zero_iff
theorem mem_closedBall_zero_iff :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, a ∈ Metric.closedBall 0 r ↔ ‖a‖ ≤ r
This theorem states that for any Seminormed Additive Group `E` and any element `a` in it, and any real number `r`, `a` is in the closed ball of radius `r` centered at `0` if and only if the norm of `a` is less than or equal to `r`. In other words, a point is within a certain distance from the origin in this metric space if and only if its norm is less than or equal to that distance.
More concisely: For any seminormed additive group `E` and real number `r`, an element `a` in `E` belongs to the closed ball centered at `0` with radius `r` if and only if the norm of `a` is less than or equal to `r`.
|
norm_le_insert
theorem norm_le_insert : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (u v : E), ‖v‖ ≤ ‖u‖ + ‖u - v‖
This theorem, `norm_le_insert`, which is an alias for `norm_le_norm_add_norm_sub`, establishes that for any seminormed add group `E` and any two elements `u` and `v` from `E`, the norm of `v` is less than or equal to the sum of the norm of `u` and the norm of the difference between `u` and `v`, i.e., ‖v‖ ≤ ‖u‖ + ‖u - v‖. In simpler terms, it states that the "length" (norm) of a vector `v` in a space with a certain kind of structure (a seminormed add group) is always less than or equal to the "length" of another vector `u` plus the "length" of the vector that takes us from `u` to `v`.
More concisely: For any seminormed add group E and elements u, v ∈ E, the norm of v is less than or equal to the sum of the norms of u and the difference between u and v: ||v|| ≤ ||u|| + ||u - v||.
|
Pi.sum_norm_apply_le_norm
theorem Pi.sum_norm_apply_le_norm :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (π i)]
(f : (i : ι) → π i), (Finset.univ.sum fun i => ‖f i‖) ≤ Fintype.card ι • ‖f‖
This theorem states that for any finite type `ι` and any function `f` that maps every element of `ι` to a seminormed add group, the sum of the norms of `f` at each element of `ι` (i.e., the $L^1$ norm of `f`) is less than or equal to the cardinality of `ι` (i.e., the number of elements in `ι`) times the supremum norm of `f` (i.e., the $L^\infty$ norm of `f`). This is essentially a statement about the relationship between the $L^1$ and $L^\infty$ norms in finite dimensions.
More concisely: For any finite type `ι` and function `f` from `ι` to seminormed add groups, the $L^1$ norm of `f` is less than or equal to the cardinality of `ι` times the $L^\infty$ norm of `f`.
|
dist_zero_right
theorem dist_zero_right : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), dist a 0 = ‖a‖
This theorem states that for any type `E` that forms a seminormed add group, the distance of any element `a` from zero is equal to the norm of `a`. In mathematical terms, we can say that for any element `a` in a seminormed add group `E`, the distance from `a` to the zero element (`0`) is identical to the seminorm of `a` (denoted as `‖a‖`).
More concisely: In a seminormed add group, the seminorm of an element equals its distance to the zero element.
|
mem_ball_zero_iff
theorem mem_ball_zero_iff :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, a ∈ Metric.ball 0 r ↔ ‖a‖ < r
This theorem, `mem_ball_zero_iff`, states that for any type `E` that forms a semi-normed add group, any element `a` of type `E`, and any real number `r`, `a` is an element of the metric ball centered at 0 with radius `r` if and only if the semi-norm of `a` is less than `r`. In other words, the point `a` is within the open ball of radius `r` centered at the origin in the metric space defined by the semi-norm if its distance from the origin, measured by the semi-norm, is less than `r`.
More concisely: For any semi-normed add group type `E`, element `a` of `E`, and real number `r`, `a` belongs to the open metric ball of radius `r` centered at 0 if and only if the semi-norm of `a` is less than `r`.
|
Bornology.IsBounded.exists_norm_le'
theorem Bornology.IsBounded.exists_norm_le' :
∀ {E : Type u_6} [inst : SeminormedGroup E] {s : Set E}, Bornology.IsBounded s → ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
This theorem, referred to as an alias of the forward direction of `isBounded_iff_forall_norm_le'`, states that for any set `s` of elements of type `E`, where `E` is a seminormed group, if `s` is bounded relative to the ambient bornology on `E`, then there exists a real number `C` such that the norm of each element `x` in `s` is less than or equal to `C`. Here, the norm ‖x‖ is a function that gives the length or size of the vector `x`.
More concisely: If a set `s` of elements in a seminormed group `E` is bounded, then there exists a real number `C` such that the norm of every element `x` in `s` satisfies `‖x‖ ≤ C`.
|
dist_one_right
theorem dist_one_right : ∀ {E : Type u_6} [inst : SeminormedGroup E] (a : E), dist a 1 = ‖a‖
This theorem, `dist_one_right`, states that for any type `E` that is a seminormed group, the distance from any element `a` of type `E` to the number 1 is equal to the norm of `a`. The `dist` function in this context defines the distance between two elements in a seminormed group, while `‖a‖` denotes the norm of `a`. In general, the norm of a vector in a normed group is a non-negative value that represents the "length" or "size" of the vector.
More concisely: For any seminormed group `E` and element `a` in `E`, the distance from `a` to 1 is equal to the norm of `a`. (i.e. `dist a 1 = ‖a‖`)
|
abs_norm
theorem abs_norm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (z : E), |‖z‖| = ‖z‖
This theorem states that for any type `E` that is a seminormed add group, the absolute value of the norm of an element `z` of `E` is equal to the norm of `z`. In other words, the norm of any element in a seminormed add group is always nonnegative, hence its absolute value remains the same.
More concisely: For any seminormed add group `E` and its element `z`, the norm of `z` equals its absolute value.
|
SeminormedAddGroup.dist_eq
theorem SeminormedAddGroup.dist_eq : ∀ {E : Type u_9} [self : SeminormedAddGroup E] (x y : E), dist x y = ‖x - y‖ := by
sorry
This theorem is stating that for any type `E` that is a Seminormed Additive Group, the distance between two elements `x` and `y` of `E` is equal to the norm of the difference between `x` and `y`. In other words, the distance function in this context is induced by the norm function. Here, the distance and norm functions are mathematical concepts which, informally speaking, measure 'how far apart' elements are and 'how large' elements are, respectively. In formal mathematical terms, they are functions that satisfy certain properties that make them useful in various areas of mathematics.
More concisely: For any seminormed additive group `E` and elements `x` and `y` in `E`, the distance `d(x, y)` between `x` and `y` equals the norm `‖x - y‖` of their difference.
|
Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.17
theorem Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.17 :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), ‖a - b‖ = dist a b
This theorem from the Mathlib library in Analysis/Normed Group/Basic states that for any type 'E' that has an instance of a 'SemimornedAddGroup', the norm of the difference between any two elements 'a' and 'b' of this type is equal to the distance between 'a' and 'b'. In mathematical terms, it asserts that ‖a - b‖ = dist(a, b) for any 'a' and 'b' in 'E'.
More concisely: For any type 'E' with a SeminormedAddGroup structure, the norm of the difference between any two elements equals their distance: ‖a - b‖ = dist(a, b).
|
Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.40
theorem Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.40 :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), ‖a‖ = dist a 0
This theorem, from the Mathlib library in the Analysis of Normed Groups section, states that for any type `E` which forms a semi-normed add group, the norm of an element `a` of type `E` is equal to the distance of `a` from 0. In mathematical terms, it says that for all `a` in `E`, the norm of `a` (`‖a‖`) is equal to the distance of `a` from the origin (`dist a 0`).
More concisely: For any semi-normed add group `E`, the norm of an element `a` in `E` is equal to the distance from `a` to the origin.
|
tendsto_norm_zero
theorem tendsto_norm_zero :
∀ {E : Type u_6} [inst : SeminormedAddGroup E], Filter.Tendsto (fun a => ‖a‖) (nhds 0) (nhds 0)
This theorem, `tendsto_norm_zero`, states that for every semi-normed add group `E`, the norm function tends to zero as its argument tends to zero. More formally, given any neighborhood of zero in the reals (in the space of norms), there exists a neighborhood of zero in the semi-normed add group such that the norm of all elements in this neighborhood is contained within the specified neighborhood of zero in the reals. Essentially, it's stating that the norm of elements close to zero in the semi-normed add group will also be close to zero, which is a fundamental property of norms in a topological space.
More concisely: Given any semi-normed add group `E` and any neighborhood of zero in the real numbers, there exists a neighborhood of zero in `E` such that the norm of every element in this neighborhood is contained within the given neighborhood of zero in the real numbers.
|
Filter.Tendsto.op_one_isBoundedUnder_le'
theorem Filter.Tendsto.op_one_isBoundedUnder_le' :
∀ {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [inst : SeminormedGroup E]
[inst_1 : SeminormedGroup F] [inst_2 : SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α},
Filter.Tendsto f l (nhds 1) →
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g) →
∀ (op : E → F → G),
(∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 1)
Here's a description of the theorem:
This theorem provides a helper lemma, which is essential to prove that the output of an operation (which can be a scalar or usual multiplication) involving a function tending towards one and a bounded function, also tends to one. The operation is defined as a binary function `op : E → F → G`, which satisfies a norm condition: `‖op x y‖ ≤ A * ‖x‖ * ‖y‖` for some constant `A`. The theorem states that, given a function `f` which tends towards one and another function `g` which is bounded under the filter `l`, for any operation `op` that satisfies the norm condition, the function `x => op (f x) (g x)` also tends towards one under the same filter `l`. This theorem is general enough to apply to various kinds of multiplication operations such as `(*)`, `flip (*)`, `(•)`, and `flip (•)`.
More concisely: Given functions `f` tending to 1 and `g` bounded under filter `l`, for any binary function `op` satisfying the norm condition `‖op x y‖ ≤ A * ‖x‖ * ‖y‖, the function `x => op (f x) (g x)` also tends to 1 under filter `l`.
|
norm_le_norm_add_norm_sub'
theorem norm_le_norm_add_norm_sub' : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖u - v‖ := by
sorry
This theorem states that for any seminormed add group `E`, and for any two elements `u` and `v` in `E`, the norm of `u` is less than or equal to the sum of the norm of `v` and the norm of the difference between `u` and `v`. This is a generalization of the triangle inequality in the context of seminormed add groups.
More concisely: For any seminormed add group `E` and elements `u`, `v` in `E`, |u| ≤ |v| + |u - v|.
|
nnnorm_le_insert
theorem nnnorm_le_insert : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊
This theorem, `nnnorm_le_insert`, is an alias of `nnnorm_le_nnnorm_add_nnnorm_sub` and it states that for any seminormed add group `E` and its elements `a` and `b`, the nonnegative norm of `b` is less than or equal to the sum of the nonnegative norm of `a` and the nonnegative norm of the difference between `a` and `b`. In mathematical terms, it's the inequality ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊.
More concisely: For any seminormed add group `E` and its elements `a` and `b`, the nonnegative norm of `b` is less than or equal to the sum of the nonnegative norm of `a` and the nonnegative norm of `a - b`.
|
Subgroup.coe_norm
theorem Subgroup.coe_norm : ∀ {E : Type u_6} [inst : SeminormedGroup E] {s : Subgroup E} (x : ↥s), ‖x‖ = ‖↑x‖ := by
sorry
This theorem states that for a given seminormed group `E` and any of its subgroups `s`, the norm of an element `x` in the subgroup `s` is equal to its norm when considered as an element of the group `E`. In other words, the norm of `x` doesn't change whether it is being considered in the context of the whole group or just one of its subgroups.
More concisely: For any seminormed group `E` and its subgroup `s`, the norm of an element `x` in `s` equals its norm as an element of `E`.
|
dist_eq_norm
theorem dist_eq_norm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), dist a b = ‖a - b‖
This theorem, named `dist_eq_norm`, applies to any seminormed add group `E` of an arbitrary type `u_6`. It states that for any two elements `a` and `b` of `E`, the distance between `a` and `b` is equal to the norm of the difference between `a` and `b`. In mathematical notation, this means `dist(a, b) = ‖a - b‖`.
More concisely: For any seminormed add group `E` and elements `a` and `b` in `E`, the distance between `a` and `b` equals the norm of their difference: `dist(a, b) = ‖a - b‖`.
|
norm_zero
theorem norm_zero : ∀ {E : Type u_6} [inst : SeminormedAddGroup E], ‖0‖ = 0
This theorem states that for any type `E` that forms a semi-normed group, the semi-norm of the zero element is zero. In mathematical terms, for any semi-normed add group `E`, the norm of zero (`‖0‖`) equals zero.
More concisely: In a semi-normed additive group, the norm of the additive identity is zero.
|
norm_pos_iff
theorem norm_pos_iff : ∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, 0 < ‖a‖ ↔ a ≠ 0
This theorem states that for any type `E` that is a normed additive group and any element `a` of `E`, the norm of `a` is positive if and only if `a` is not the zero element. In other words, in the context of normed additive groups, a nonzero element always has a positive norm, and an element has a positive norm if and only if it's not the zero element.
More concisely: In a normed additive group, an element has a positive norm if and only if it is nonzero.
|
tendsto_norm_cocompact_atTop
theorem tendsto_norm_cocompact_atTop :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : ProperSpace E],
Filter.Tendsto norm (Filter.cocompact E) Filter.atTop
The theorem `tendsto_norm_cocompact_atTop` states that for any type `E` that is equipped with a semi-normed additive group structure and is also a proper space (i.e., every closed ball is compact), the norm function tends to infinity (`Filter.atTop`) when the filter tends towards the complement of compact sets (`Filter.cocompact E`). In other words, as we move away from compact sets in this space, the norm of the elements tends to increase without bound.
More concisely: For any proper, semi-normed additive group `E`, the norm function `norm : E → ℝ` tends to infinity as the filter approaches the complement of compact sets.
|
SeminormedAddCommGroup.dist_eq
theorem SeminormedAddCommGroup.dist_eq :
∀ {E : Type u_9} [self : SeminormedAddCommGroup E] (x y : E), dist x y = ‖x - y‖
This theorem states that for any seminormed additive commutative group `E` and any two elements `x` and `y` within this group, the distance between `x` and `y` is equal to the norm of the difference between `x` and `y`. In mathematical notation, this is saying that for all `x, y` in `E`, the distance `d(x, y)` is equal to the norm `‖x - y‖`.
More concisely: For any seminormed additive commutative group `E`, the distance between any two elements `x` and `y` is equal to the norm of their difference: `d(x, y) = ‖x - y‖`.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.6
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.6 :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), (0 ≤ ‖a‖) = True
This theorem, named `Mathlib.Analysis.Normed.Group.Basic._auxLemma.6`, states that for any type `E` that forms a seminormed add group, the norm of any element `a` of type `E` is always non-negative. In mathematical terms, it says that for every `a` in `E`, `0 ≤ ‖a‖` is always true.
More concisely: For any seminormed add group `E`, the norm of every element `a` in `E` is non-negative (i.e., `0 ≤ ‖a‖`).
|
norm_sum_le_of_le
theorem norm_sum_le_of_le :
∀ {ι : Type u_4} {E : Type u_6} [inst : SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ},
(∀ b ∈ s, ‖f b‖ ≤ n b) → ‖s.sum fun b => f b‖ ≤ s.sum fun b => n b
The theorem `norm_sum_le_of_le` states that for any finite set `s` of elements of type `ι`, if each element `b` in `s` is such that the norm of `f(b)` is less than or equal to `n(b)`, then the norm of the sum of `f(b)` over all `b` in `s` is less than or equal to the sum of `n(b)` over all `b` in `s`. Here, `f` is a function mapping `ι` to a seminormed add commutative group `E`, and `n` is a function mapping `ι` to real numbers.
More concisely: For any finite set `s` and function `f` from a type `ι` to a seminormed add commutative group `E`, and function `n` from `ι` to the real numbers, if `||f(b)|| ≤ n(b)` for all `b` in `s`, then `||∑(b ∈ s) f(b)|| ≤ ∑(b ∈ s) n(b)`.
|
Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.22
theorem Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.22 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
This theorem states that for all types `α` and `β`, for any function `f` from `α` to `β`, for any set `s` of type `β`, and any element `a` of type `α`, the statement "`a` belongs to the preimage of `s` under `f`" is equivalent to the statement "`f(a)` belongs to `s`". In mathematical terms, for any element `a` in the domain of a function, `a` is in the preimage of a set `s` under function `f` if and only if the image of `a` under `f` is in the set `s`.
More concisely: For any function between types `α` and `β`, and any set `s` of type `β`, the element `a` of type `α` is in the preimage of `s` under `f` if and only if `f(a)` is in `s`.
|
nnnorm_zero
theorem nnnorm_zero : ∀ {E : Type u_6} [inst : SeminormedAddGroup E], ‖0‖₊ = 0
This theorem states that for any type `E` which has the structure of a seminormed add group, the non-negative seminorm of zero is equal to zero. In mathematical terms, if we denote the seminorm of an element `x` in `E` by `‖x‖₊`, then `‖0‖₊ = 0`. This is a standard property of seminorms in functional analysis.
More concisely: For any seminormed add group `E`, the seminorm of the additive identity (zero) is equal to zero.
|
mem_closure_zero_iff_norm
theorem mem_closure_zero_iff_norm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] {x : E}, x ∈ closure {0} ↔ ‖x‖ = 0
The theorem `mem_closure_zero_iff_norm` states that for any seminormed additive group `E` and any element `x` of `E`, the element `x` is in the closure of the set containing only the zero element if and only if the norm of `x` is zero. In other words, any element `x` in the closure of a set that only contains the zero element in a seminormed additive group will have a norm of zero.
More concisely: For any seminormed additive group E and element x of E, x is in the closure of {0} if and only if the norm of x is zero.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.32
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.32 :
∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, (0 < ‖a‖) = (a ≠ 0)
This theorem is a statement about normed add groups in the field of analysis. It says that for any element `a` in a normed add group `E`, the norm of `a` is greater than zero if and only if `a` is not equal to zero. This basically means that the only element in `E` with a norm of zero is the zero element itself, which is a fundamental property of normed spaces.
More concisely: In a normed add group, the only element with norm equal to zero is the additive identity.
|
LipschitzOnWith.norm_sub_le
theorem LipschitzOnWith.norm_sub_le :
∀ {E : Type u_6} {F : Type u_7} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {s : Set E}
{f : E → F} {C : NNReal},
LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
The theorem `LipschitzOnWith.norm_sub_le` states that for any types `E` and `F` that are seminormed add groups, any set `s` of type `E`, any function `f` from `E` to `F`, and any nonnegative real number `C`, if the function `f` is Lipschitz continuous with constant `C` on the set `s`, then for all `x` and `y` in `s`, the norm of the difference between `f(x)` and `f(y)` is less than or equal to `C` times the norm of the difference between `x` and `y`. In mathematical terms, we have $\|f(x) - f(y)\| \leq C \|x - y\|$ for all $x, y \in s$.
More concisely: For any Lipschitz continuous function $f$ from a seminormed add group $E$ to another seminormed add group $F$, and any set $s$ in $E$, the norm of $f(x) - f(y)$ is less than or equal to the Lipschitz constant $C$ times the norm of $x - y$ for all $x, y \in s$.
|
norm_div_le
theorem norm_div_le : ∀ {E : Type u_6} [inst : SeminormedGroup E] (a b : E), ‖a / b‖ ≤ ‖a‖ + ‖b‖
This theorem states that for any two elements `a` and `b` in a seminormed group `E`, the norm of their division `a / b` is less than or equal to the sum of their individual norms. In other words, it states that in a seminormed group, the norm of the quotient of two elements is always less than or equal to the sum of the norms of the two elements. This can be written in mathematical notation as ‖a / b‖ ≤ ‖a‖ + ‖b‖.
More concisely: In a seminormed group, the norm of the quotient of two elements is less than or equal to the sum of their individual norms: ‖a / b‖ ≤ ‖a‖ + ‖b‖.
|
pi_norm_lt_iff
theorem pi_norm_lt_iff :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (π i)]
{x : (i : ι) → π i} {r : ℝ}, 0 < r → (‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r)
This theorem, named `pi_norm_lt_iff`, states that for any given index type `ι`, any function `π` that maps indices to types, any `x` which is a function from indices to instances of these types, and any real number `r` that is greater than zero, the statement "the seminorm of `x` is less than `r`" is equivalent to the statement "the seminorm of each component of `x` is less than `r`". This is essentially a property of seminorms in a product space, which defines how the seminorm of an element can be related to the seminorms of its individual components.
More concisely: For any index type `ι`, function `π` mapping indices to types, function `x` from indices to their types, and real number `r > 0`, the seminorm of `x` is less than `r` if and only if the seminorm of each component function `π i -> x i` is less than `r`.
|
Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.24
theorem Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.24 :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, (y ∈ Metric.closedBall x ε) = (dist y x ≤ ε) := by
sorry
This theorem, "Mathlib.Analysis.Normed.Group.Basic._auxAddLemma.24", states that for any pseudometric space `α`, and any elements `x` and `y` of that space, and any real number `ε`, the fact that `y` is in the closed ball of radius `ε` centered at `x` is equivalent to the statement that the distance from `y` to `x` is less than or equal to `ε`. This is an equivalence claim, which means that the two conditions described (being in the closed ball and having a distance less than or equal to `ε`) always hold true together or always false together.
More concisely: For any pseudometric space and elements, the closed ball condition and the distance condition are equivalent: an element belongs to the closed ball of center and radius if and only if its distance to the center is less than or equal to the radius.
|
NormedGroup.dist_eq
theorem NormedGroup.dist_eq : ∀ {E : Type u_9} [self : NormedGroup E] (x y : E), dist x y = ‖x / y‖
This theorem states that in any normed group `E`, the distance function between two elements `x` and `y` of the group is equal to the norm of `x` divided by `y`. Here, a normed group is a group that also has a vector space structure and a norm function, which assigns a non-negative length or size to each vector in the vector space. The distance function measures the distance between two points in the group, while the norm function measures the length or size of a single vector. In essence, this theorem connects these two concepts, showing that the distance between two points is simply the norm of their difference.
More concisely: In a normed group, the distance between two elements is equal to the norm of their difference.
|
Filter.Tendsto.op_one_isBoundedUnder_le
theorem Filter.Tendsto.op_one_isBoundedUnder_le :
∀ {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [inst : SeminormedGroup E]
[inst_1 : SeminormedGroup F] [inst_2 : SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α},
Filter.Tendsto f l (nhds 1) →
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g) →
∀ (op : E → F → G),
(∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 1)
This theorem, `Filter.Tendsto.op_one_isBoundedUnder_le`, states that for any types `α`, `E`, `F`, and `G`, where `E`, `F`, and `G` are seminormed groups, and given two functions `f : α → E` and `g : α → F` with a filter `l` on `α`, if the function `f` tends to 1 with respect to the filter `l` and the composition of the norm-function with `g` is eventually bounded under the order relation `(fun x x_1 => x ≤ x_1)` with respect to the filter `l`, then, for any binary operation `op : E → F → G` which satisfies the inequality `‖op x y‖ ≤ ‖x‖ * ‖y‖` for all `x` in `E` and `y` in `F`, the function `(fun x => op (f x) (g x))` tends to 1 with respect to the filter `l`. In other words, the product of a function that tends to one and a bounded function also tends to one, and this is proven in a generalized way for any binary operation that satisfies a certain norm bound.
More concisely: If a function that tends to 1 with respect to a filter and is composed with a function that is eventually bounded under the filter with respect to the order relation, then the composition of their norms with any binary operation satisfying the triangle inequality tends to 1 with respect to the filter.
|
squeeze_one_norm
theorem squeeze_one_norm :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
(∀ (n : α), ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 1)
This theorem is a special case of the squeeze theorem for functions with norms. It states that for any types `α` and `E`, where `E` is a semi-normed group, and for any functions `f : α → E` and `a : α → ℝ`, along with a filter `t₀` on `α`, if the norm of `f` at any point `n` (i.e., `‖f n‖`) is less than or equal to `a n`, and if the function `a` tends to `0` with respect to the filter `t₀` (i.e., as `n` tends to whatever values are "central" according to `t₀`, `a n` tends to `0`), then `f` also tends to `1` with respect to the same filter `t₀`. In other words, if the norm of `f` is bounded by some real function `a` that approaches `0` for values in `t₀`, then `f` approaches `1` for those same values.
More concisely: If `f : α → E` is a function from type `α` to a semi-normed group `E` and `a : α → ℝ` is a function such that `‖f n‖ ≤ a n` for all `n ∈ α` and `a` tends to `0` with respect to filter `t₀` on `α`, then `f` tends to `1` with respect to `t₀`.
|
AddSubgroup.coe_norm
theorem AddSubgroup.coe_norm :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s), ‖x‖ = ‖↑x‖
The theorem, `AddSubgroup.coe_norm`, states that for any seminormed additive group `E` and any of its subgroups `s`, the norm of an element `x` within the subgroup `s` is equal to the norm of the same element when considered as part of the larger group `E`. This means that the norm operation is invariant under the inclusion of `x` in the subgroup `s` or the group `E`.
More concisely: For any seminormed additive group `E`, subgroup `s` of `E`, and `x` in `s`, the norm of `x` in `E` equals the norm of `x` in `s`.
|
ball_zero_eq
theorem ball_zero_eq : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (r : ℝ), Metric.ball 0 r = {x | ‖x‖ < r} := by
sorry
The theorem `ball_zero_eq` states that for any real number `r` and for any semi-normed additive group `E`, the metric ball of radius `r` centered at zero is exactly the set of all elements `x` in `E` such that the norm of `x` is less than `r`. In other words, it equates the concept of a metric ball at the origin in a semi-normed additive group with the set of points whose norm is less than a given radius.
More concisely: In a semi-normed additive group, the metric ball centered at the origin with radius `r` is equal to the set of elements with norm less than `r`.
|
Real.ennnorm_eq_ofReal
theorem Real.ennnorm_eq_ofReal : ∀ {r : ℝ}, 0 ≤ r → ↑‖r‖₊ = ENNReal.ofReal r
This theorem states that for every real number `r` that is nonnegative (i.e., `r` is greater than or equal to 0), the nonnegative extended real number norm of `r`, denoted as `↑‖r‖₊`, is equal to the nonnegative extended real number obtained by applying the `ENNReal.ofReal` function to `r`. In other words, if you have a nonnegative real number `r`, its norm in the extended nonnegative real number domain is the same as if you just convert `r` to an extended nonnegative real number using the `ENNReal.ofReal` function.
More concisely: For all non-negative real numbers `r`, `↑‖r‖₊ = ENNReal.ofReal r`.
|
edist_eq_coe_nnnorm_sub
theorem edist_eq_coe_nnnorm_sub : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), edist a b = ↑‖a - b‖₊ := by
sorry
This theorem states that for any seminormed add group `E` and any elements `a` and `b` of `E`, the extended distance between `a` and `b` is equal to the non-negative real number obtained by casting the non-negative norm of the difference between `a` and `b`. In the context of mathematics, this is stating that in any seminormed add group, the "distance" between two elements is precisely the norm of their difference.
More concisely: In a seminormed add group, the distance between two elements is equal to the norm of their difference.
|
norm_ne_zero_iff
theorem norm_ne_zero_iff : ∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, ‖a‖ ≠ 0 ↔ a ≠ 0
This theorem, `norm_ne_zero_iff`, states that for any type `E`, that is a normed add group, and any element `a` of this type, the norm of `a` is not equal to zero if and only if `a` is not equal to zero. In other words, in a normed add group, an element has a nonzero norm if and only if the element itself is not zero.
More concisely: In a normed add group, the norm of an element is nonzero if and only if the element is nonzero.
|
norm_sub_norm_le
theorem norm_sub_norm_le : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), ‖a‖ - ‖b‖ ≤ ‖a - b‖
This theorem states that for any type `E` that is a seminormed add group, for any elements `a` and `b` of `E`, the absolute value of the difference of their norms (‖a‖ - ‖b‖) is less than or equal to the norm of their difference (‖a - b‖). This is a property related to the triangle inequality in the context of normed spaces.
More concisely: For any seminormed add group `E` and elements `a` and `b` in `E`, |‖a‖ - ‖b‖| ≤ ‖a - b‖.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.25
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.25 : ∀ {r₁ r₂ : NNReal}, (r₁ ≤ r₂) = (↑r₁ ≤ ↑r₂)
This theorem states that for any two nonnegative real numbers `r₁` and `r₂`, the condition that `r₁` is less than or equal to `r₂` is equivalent to the condition that the real number associated with `r₁` is less than or equal to the real number associated with `r₂`. Here, the `↑` symbol indicates the coercion of a nonnegative real number to a real number.
More concisely: For any nonnegative real numbers `r₁` and `r₂`, `r₁ ≤ r₂` if and only if `↑r₁ ≤ ↑r₂`.
|
norm_sub_rev
theorem norm_sub_rev : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), ‖a - b‖ = ‖b - a‖
This theorem states that for any type `E` that forms a semi-normed add group (which is a mathematical structure that combines the properties of a group and a semi-norm), the norm of the difference between any two elements `a` and `b` (`‖a - b‖`) is equal to the norm of the difference between `b` and `a` (`‖b - a‖`). This is essentially saying that the order in which you subtract the two elements does not affect the result of the norm, aligning with the idea that distance is direction-independent.
More concisely: For any type `E` forming a semi-normed add group, the norm of the difference between two elements `a` and `b` is equal to the norm of `b` minus `a`, i.e., `‖a - b‖ = ‖b - a‖`.
|
nnnorm_eq_zero
theorem nnnorm_eq_zero : ∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, ‖a‖₊ = 0 ↔ a = 0
This theorem states that for any type `E` that is a normed add group, the non-negative norm (`‖a‖₊`) of an element `a` from `E` is equal to zero if and only if the element `a` itself is zero. In other words, in a normed add group, an element has zero norm if and only if it is the zero element.
More concisely: In a normed add group, the element of zero norm is equivalent to the zero element.
|
norm_le_norm_add_norm_div'
theorem norm_le_norm_add_norm_div' : ∀ {E : Type u_6} [inst : SeminormedGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖u / v‖ := by
sorry
This theorem, `norm_le_norm_add_norm_div'`, states that for any given type `E` which is a seminormed group, and for any two elements `u` and `v` of that group, the norm of `u` is less than or equal to the sum of the norm of `v` and the norm of the quotient `u / v`. In mathematical notation, this is $\|u\| \leq \|v\| + \|u / v\|$.
More concisely: For any seminormed group `E` and elements `u` and `v` in `E` with `v ≠ 0`, the norm of `u` is less than or equal to the sum of the norms of `v` and `u / v`. (Mathematically: $\|u\| \leq \|v\| + \|u / v\|$)
|
Real.norm_eq_abs
theorem Real.norm_eq_abs : ∀ (r : ℝ), ‖r‖ = |r|
This theorem states that for any real number `r`, the norm of `r` is equal to the absolute value of `r`. In other words, the magnitude of any real number, when considered in the context of a normed field, is the same as its absolute value. The norm and absolute value both measure "size" in their respective contexts.
More concisely: For any real number `r`, the norm of `r` equals its absolute value. (i.e., `‖r‖ = |r|`)
|
AddMonoidHomClass.antilipschitz_of_bound
theorem AddMonoidHomClass.antilipschitz_of_bound :
∀ {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
[inst_2 : FunLike 𝓕 E F] [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal},
(∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) → AntilipschitzWith K ⇑f
The theorem `AddMonoidHomClass.antilipschitz_of_bound` states that for all types `𝓕`, `E`, and `F`, where `E` and `F` are seminormed add groups, and `𝓕` is a type that behaves like a function from `E` to `F` and is also an additive monoid homomorphism, given a certain function `f` of type `𝓕` and a nonnegative real number `K`, if for every element `x` of type `E`, the seminorm of `x` is less than or equal to `K` times the seminorm of `f x`, then the function `f` is `K`-Antilipschitz.
In mathematical terms, a function `f` is `K`-Antilipschitz if the extended distance between any two points `x` and `y` is always less than or equal to `K` times the extended distance between `f(x)` and `f(y)`.
More concisely: Given a type `𝓕` that is a function from a seminormed add group `E` to another seminormed add group `F`, is an additive monoid homomorphism, and satisfies the condition that for all `x` in `E`, the seminorm of `x` is less than or equal to `K` times the seminorm of `𝓕(x)`, then `𝓕` is `K`-Antilipschitz.
|
tendsto_iff_norm_sub_tendsto_zero
theorem tendsto_iff_norm_sub_tendsto_zero :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] {f : α → E} {a : Filter α} {b : E},
Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖f e - b‖) a (nhds 0)
This theorem, `tendsto_iff_norm_sub_tendsto_zero`, establishes an equivalence between two conditions for a function `f` from an arbitrary type `α` into a seminormed add group `E`. The function `f` is said to tend towards a value `b` with respect to a filter `a` if and only if the norm of the difference between `f(e)` and `b` tends towards zero with respect to the same filter `a`. Here, tending towards a value is defined in terms of the `Filter.Tendsto` function, which says that for every neighborhood of the targeted value, the preimage under `f` of that neighborhood is a neighborhood with respect to the filter.
More concisely: A function `f : α → E` from type `α` to a seminormed add group `E` tends towards `b` with respect to a filter `a` if and only if the norm of `f(e) - b` tends towards 0 with respect to `a`.
|
nndist_eq_nnnorm
theorem nndist_eq_nnnorm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), nndist a b = ‖a - b‖₊
This theorem, called `nndist_eq_nnnorm`, states that for any type `E` which is a seminormed add group (a group with an additional structure called a seminorm), the non-negative distance (`nndist`) between any two elements `a` and `b` of `E` is equal to the non-negative norm (`nnnorm`) of the difference between `a` and `b`. In mathematical terms, for all `a` and `b` in `E`, `nndist a b = ‖a - b‖₊`.
More concisely: For any seminormed add group `E`, the non-negative distance between two elements `a` and `b` is equal to the non-negative norm of their difference: `nndist a b = ‖a - b‖₊`.
|
squeeze_zero_norm'
theorem squeeze_zero_norm' :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
(∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)
This theorem, often referred to as a special case of the sandwich theorem, states that for any seminormed add group `E` and any types `α`, given a function `f` from `α` to `E`, a real-valued function `a` on `α`, and a filter `t₀` on `α`, if the norm of `f` at any `α` value `n` is eventually (according to the filter `t₀`) bounded by the value of `a` at `n`, and if `a` tends to zero according to the filter `t₀`, then `f` also tends to zero according to the filter `t₀`. The theorem has two versions: the version with the prime (`'`) uses the "eventually" terminology, while the version without the prime states the fact absolutely.
More concisely: If in a seminormed add group `E`, a function `f` from a type `α` to `E`, a real-valued function `a` on `α`, and a filter `t₀` on `α` exist such that for all `n` in `α`, the filter `t₀` eventually has `n` in its neighborhood and the norm of `f(n)` is bounded by `a(n)` in that neighborhood, and `a(n)` tends to zero according to the filter `t₀`, then `f(n)` tends to zero according to the filter `t₀`.
|
Submodule.norm_coe
theorem Submodule.norm_coe :
∀ {𝕜 : Type u_2} {E : Type u_6} [inst : Ring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
{s : Submodule 𝕜 E} (x : ↥s), ‖↑x‖ = ‖x‖
This theorem states that if `x` is an element of a submodule `s` of a normed group `E`, the norm of `x` in `E` is the same as its norm in `s`. The norm is a measure of the "length" or "size" of an element in a normed group. It means that the norm of an element doesn't change whether we consider it as part of a larger group or a smaller submodule. This is a reversed version of the `Submodule.coe_norm` lemma for use by `norm_cast`.
More concisely: The theorem asserts that the norm of an element in a submodule of a normed group equals its norm in the larger group.
|
Rat.norm_cast_real
theorem Rat.norm_cast_real : ∀ (r : ℚ), ‖↑r‖ = ‖r‖
This theorem states that for every rational number `r`, the norm (or absolute value) of `r` as a real number (indicated by `↑r`) is equal to the norm of `r` as a rational number. In other words, casting a rational number to a real number doesn't change its norm.
More concisely: For every rational number `r`, the absolute value of `r` as a real number equals the absolute value of `r` as a rational number. (i.e., `|↑r| = |r|`)
|
mem_emetric_ball_zero_iff
theorem mem_emetric_ball_zero_iff :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a : E} {r : ENNReal}, a ∈ EMetric.ball 0 r ↔ ↑‖a‖₊ < r
This theorem states that for any type `E` that forms a semi-normed additive group and any element `a` of `E` and `r` of type `ENNReal` (the extended nonnegative real numbers), `a` is in the `EMetric.ball` centered at 0 with radius `r` if and only if the semi-norm of `a` is less than `r`. In mathematical terms, it means that a point `a` lies within the open ball with radius `r` in a semi-normed additive group if and only if the semi-norm of `a` is less than `r`.
More concisely: For any semi-normed additive group `E` and element `a` in `E` and real number `r` > 0, `a` lies in the open ball of radius `r` if and only if the semi-norm of `a` is less than `r`.
|
LipschitzWith.norm_div_le
theorem LipschitzWith.norm_div_le :
∀ {E : Type u_6} {F : Type u_7} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {C : NNReal},
LipschitzWith C f → ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖
The theorem `LipschitzWith.norm_div_le` states that for all types `E` and `F`, which are seminormed groups, and a function `f` mapping from `E` to `F` with a nonnegative real number `C` as Lipschitz constant, if the function `f` is Lipschitz continuous with constant `C`, then for all elements `x` and `y` in `E`, the norm of the ratio of `f x` to `f y` is less than or equal to `C` times the norm of the ratio of `x` to `y`. In mathematical terms, this means that if $f$ is Lipschitz continuous with constant $C$, then $\|f(x) / f(y)\| \leq C * \|x / y\|$ for all $x, y$ in $E$.
More concisely: For any seminormed groups E and F, and a Lipschitz continuous function f from E to F with constant C, the norm of the ratio of f(x) to f(y) is bounded above by C times the norm of the ratio of x to y for all x, y in E.
|
Submodule.coe_norm
theorem Submodule.coe_norm :
∀ {𝕜 : Type u_2} {E : Type u_6} [inst : Ring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
{s : Submodule 𝕜 E} (x : ↥s), ‖x‖ = ‖↑x‖
This theorem states that for any element `x` of a given submodule `s` of a normed group `E` over a ring `𝕜`, the norm of `x` in the submodule `s` is equal to its norm in the group `E`. In other words, the norm of an element doesn't change whether it is considered within the entire group or just within a particular submodule.
More concisely: For any submodule `s` of a normed group `E` over a ring `𝕜` and any `x` in `s`, the norm of `x` in `s` equals its norm in `E`.
|
squeeze_zero_norm
theorem squeeze_zero_norm :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
(∀ (n : α), ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)
This is a special case of the squeeze theorem. For any seminormed add group `E` and any types `α`, given a function `f : α → E` and a real function `a : α → ℝ`, and a filter `t₀ : Filter α`, if the norm of `f` at any point `n` is less than or equal to `a(n)`, and `a` tends to `0` with respect to the filter `t₀`, then `f` also tends to `0` with respect to the same filter. In mathematical terms, this says that if ‖f(n)‖ ≤ a(n) for all `n` and a(n) → 0 as n approaches some limit under the filter `t₀`, then f(n) also approaches `0` as `n` approaches the same limit under the filter.
More concisely: If a seminormed add group homomorphism `f : α → E` and a real function `a : α → ℝ` satisfy `‖f(n)‖ ≤ a(n)` for all `n`, and `a(n)` converges to `0` in the filter `t₀`, then `f(n)` also converges to `0` in the same filter `t₀`.
|
continuous_norm
theorem continuous_norm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E], Continuous fun a => ‖a‖
This theorem states that the norm function is continuous for any given type `E` that forms a seminormed add group. In other words, for any point `a` in `E`, small changes in `a` will result in small changes in its norm `‖a‖`. The continuity of the norm function is a fundamental property used in various branches of mathematics, particularly in analysis and linear algebra.
More concisely: The norm function is continuous on any seminormed additive group.
|
norm_eq_zero
theorem norm_eq_zero : ∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, ‖a‖ = 0 ↔ a = 0
This theorem, `norm_eq_zero`, states that for any type `E` that has an instance of a NormedAddGroup, an element `a` of type `E` has a norm of zero if and only if `a` is zero. In mathematical terms, for any normed addition group, an element's norm is zero if and only if the element itself is zero. This theorem is a critical property of normed spaces in functional analysis.
More concisely: For any normed additive group, an element has norm zero if and only if it is the additive identity.
|
AddSubgroup.norm_coe
theorem AddSubgroup.norm_coe :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s), ‖↑x‖ = ‖x‖
This theorem states that for any element `x` in a subgroup `s` of a seminormed group `E`, the norm of `x` in `s` is the same as its norm in `E`. In other words, the process of computing the norm of `x` is invariant whether we consider `x` as an element of the larger group `E` or the subgroup `s`. This theorem is designed to be used with `norm_cast` tactics, and it's a reversed version of the `simp` lemma `AddSubgroup.coe_norm`.
More concisely: The norm of an element in a subgroup of a seminormed group is equal to its norm in the larger group.
|
eventually_ne_of_tendsto_norm_atTop'
theorem eventually_ne_of_tendsto_norm_atTop' :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedGroup E] {l : Filter α} {f : α → E},
Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop → ∀ (x : E), ∀ᶠ (y : α) in l, f y ≠ x
The theorem `eventually_ne_of_tendsto_norm_atTop'` states that for any type `α` and `E` where `E` is a semi-normed group, given a filter `l` on `α` and a function `f` from `α` to `E`, if the norm of `f y` tends to infinity (i.e., `Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop`), then for any element `x` in `E`, there will eventually (for all `y` far enough along `l`) be a point `y` in `α` such that `f y` is not equal to `x` (i.e., `∀ᶠ (y : α) in l, f y ≠ x`). In simpler terms, if the norm of the function's values is growing without bound, then after a certain point in the domain, the function's values will no longer be equal to any fixed value in the codomain.
More concisely: Given a semi-normed group `E`, a filter `l` on a type `α`, and a function `f` from `α` to `E` such that the norm of `f y` tends to infinity along `l`, there exists no element `x` in `E` that equals `f` of infinitely many elements in `α` under `l`.
|
eventually_ne_of_tendsto_norm_atTop
theorem eventually_ne_of_tendsto_norm_atTop :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] {l : Filter α} {f : α → E},
Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop → ∀ (x : E), ∀ᶠ (y : α) in l, f y ≠ x
The theorem `eventually_ne_of_tendsto_norm_atTop` states that for any types `α` and `E`, where `E` is a seminormed add group, and given a filter `l` of type `α` and a function `f` from `α` to `E`, if the norm of `f y` tends to infinity (as captured by the condition `Filter.Tendsto (fun y => ‖f y‖) l Filter.atTop`), then for any fixed element `x` of type `E`, there will eventually be a value `y` in the filter `l` such that `f y ≠ x`. This essentially means that if the norm of the function values is increasing without bound, there will always be a point where the function value is not equal to a fixed value.
More concisely: Given a seminormed add group `E`, a filter `l` on type `α`, and a function `f` from `α` to `E` such that the norm of `f y` tends to infinity along `l`, there exists `y` in `l` with `f y ≠ x` for any fixed `x` in `E`.
|
norm_nsmul_le
theorem norm_nsmul_le : ∀ {E : Type u_6} [inst : SeminormedAddCommGroup E] (n : ℕ) (a : E), ‖n • a‖ ≤ ↑n * ‖a‖ := by
sorry
This theorem states that for any seminormed additive commutative group `E` and any natural number `n` and element `a` of `E`, the norm of `n` times `a` (`n` "scaled" by `a`) is less than or equal to `n` times the norm of `a`. In mathematical terms, if `‖x‖` denotes the norm of x, then ‖n•a‖ ≤ n*‖a‖ for every natural number `n` and every `a` in the seminormed additive commutative group `E`.
More concisely: For any seminormed additive commutative group `E` and natural number `n` and element `a` in `E`, the norm of `n` times `a` is bounded above by `n` times the norm of `a`.
|
squeeze_one_norm'
theorem squeeze_one_norm' :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
(∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 1)
This is a special case of the sandwich theorem for seminormed groups. The theorem states that for any types `α` and `E`, if `E` is a seminormed group and `f` is a function from `α` to `E`, `a` is a function from `α` to the real numbers, and `t₀` is a filter on `α`, then if the norm of `f` is eventually (according to the filter `t₀`) bounded by the function `a`, and `a` tends to 0 (according to the same filter), then `f` tends to 1 (in the space of `E`, under the neighborhood filter at 1). The `'` in the theorem's name indicates that this version of the theorem is phrased in terms of "eventually" conditions, following a convention in similar theorems in topology and algebra.
More concisely: If `f` is a function from type `α` to a seminormed group `E`, `a` is a function from `α` to the real numbers, and `t₀` is a filter on `α` such that the norm of `f` is eventually bounded by `a(x)` for all `x ∈ α` (according to `t₀)` and `a(x)` tends to 0 (according to `t₀`), then `f` tends to 1 in the space of `E` (under the neighborhood filter at 1).
|
norm_mul_le'
theorem norm_mul_le' : ∀ {E : Type u_6} [inst : SeminormedGroup E] (a b : E), ‖a * b‖ ≤ ‖a‖ + ‖b‖
This is the **Triangle Inequality** for the norm in the context of seminormed groups. Given any seminormed group `E` and any two elements `a` and `b` from `E`, the norm of the product `a * b` is always less than or equal to the sum of the norms of `a` and `b`, denoted as `‖a * b‖ ≤ ‖a‖ + ‖b‖`.
More concisely: In a seminormed group, the norm of the product of two elements is less than or equal to the sum of their individual norms.
|
AddMonoidHomClass.isometry_of_norm
theorem AddMonoidHomClass.isometry_of_norm :
∀ {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
[inst_2 : FunLike 𝓕 E F] [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕), (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f
This theorem, named `AddMonoidHomClass.isometry_of_norm`, states that for any types `𝓕`, `E`, and `F`, where `E` and `F` are seminormed add groups, `𝓕` is a function-like object from `E` to `F`, and `𝓕` is an additive monoid homomorphism class, if a function `f` of type `𝓕` satisfies the property that the norm of `f(x)` is equal to the norm of `x` for all `x` in `E`, then this function `f` is an isometry. In other words, it is a map that preserves the distance (in this case, the edistance) between elements of the pseudometric spaces `E` and `F`.
More concisely: If `𝓕` is an additive monoid homomorphism class from a seminormed add group `E` to another seminormed add group `F`, such that `𝓕` preserves the norms of elements in `E`, then `𝓕` is an isometry between the pseudometric spaces `(E, edist)` and `(F, edist')`, where `edist` and `edist'` denote the respective edistances.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.9
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.9 :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, (b ∈ Metric.sphere a r) = (‖b - a‖ = r) := by
sorry
This theorem states that for any seminormed add group `E`, and any elements `a` and `b` of `E`, along with a real number `r`, `b` being in the sphere of radius `r` centered at `a` is equivalent to the norm of the difference between `b` and `a` being equal to `r`. In other words, it states that `b` lies on the sphere with center `a` and radius `r` if and only if the distance from `b` to `a` is exactly `r`.
More concisely: For any seminormed add group `E` and real number `r`, the element `b` lies in the sphere of radius `r` centered at `a` if and only if the norm of `a - b` is equal to `r`.
|
dist_mul_mul_le
theorem dist_mul_mul_le :
∀ {E : Type u_6} [inst : SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E),
dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂
This theorem states that in the context of a seminormed commutative group `E`, for any four elements `a₁`, `a₂`, `b₁`, `b₂` of `E`, the distance between the product `a₁ * a₂` and the product `b₁ * b₂` is less than or equal to the sum of the distances between `a₁` and `b₁`, and `a₂` and `b₂`. This is a property akin to the triangle inequality in a metric space.
More concisely: In a seminormed commutative group, the triangle inequality for the product holds: ||a₁ * a₂ - b₁ * b₂|| ≤ ||a₁ - b₁|| + ||a₂ - b₂||.
|
Filter.tendsto_neg_cobounded
theorem Filter.tendsto_neg_cobounded :
∀ {E : Type u_6} [inst : SeminormedAddGroup E],
Filter.Tendsto Neg.neg (Bornology.cobounded E) (Bornology.cobounded E)
The theorem `Filter.tendsto_neg_cobounded` states that in a seminormed addition group `E`, the function of negation (mapping `x` to `-x`) has the property that it tends to infinity as `x` tends to infinity. More formally, for every set that is cobounded (i.e., its complement is bounded) in the bornology of `E`, the preimage of this set under negation is also a cobounded set in the bornology of `E`. This captures the intuitive notion that as we take larger and larger values in `E`, their negations are also becoming larger (in the opposite direction).
More concisely: In a seminormed additive group, the negation function maps cobounded sets to cobounded sets.
|
norm_inv'
theorem norm_inv' : ∀ {E : Type u_6} [inst : SeminormedGroup E] (a : E), ‖a⁻¹‖ = ‖a‖
This theorem states that, for every type `E` that forms a seminormed group, the norm of the inverse of any element `a` from `E` is equal to the norm of `a` itself. In mathematical terms, this is saying that `‖a⁻¹‖ = ‖a‖` for all `a` in `E`. This is a property of seminorms in certain types of mathematical structures.
More concisely: For every seminormed group `E`, the norm of its inverse element is equal to the norm of the original element: `‖a⁻¹‖ = ‖a‖` for all `a` in `E`.
|
ContinuousOn.norm
theorem ContinuousOn.norm :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α},
ContinuousOn f s → ContinuousOn (fun x => ‖f x‖) s
This theorem states that for any seminormed add group `E` and any topological space `α`, if a function `f` from `α` to `E` is continuous on a set `s` (meaning it's continuous at every point in `s`), then the function that assigns to each `x` in `α` the norm of `f(x)` is also continuous on `s`. In other words, the norm of a continuous function over a set is also continuous over that set.
More concisely: If `f: α → E` is a continuous function from a topological space `α` to a seminormed add group `E`, then the function `x ∈ α => ‖f x‖: α → ℝ` assigning to each `x` in `α` its norm is also continuous on `α`.
|
Filter.tendsto_inv_cobounded
theorem Filter.tendsto_inv_cobounded :
∀ {E : Type u_6} [inst : SeminormedGroup E],
Filter.Tendsto Inv.inv (Bornology.cobounded E) (Bornology.cobounded E)
The theorem `Filter.tendsto_inv_cobounded` states that in a seminormed group `E`, the function that maps an element `x` to its inverse `x⁻¹` has the property that it tends to infinity as `x` tends to infinity. In more formal terms, for every set `A` that is bounded away from infinity in `E`, the preimage of `A` under the inversion function is also bounded away from infinity in `E`. Therefore, the inversion function is said to be cobounded in the bornology of `E`.
More concisely: In a seminormed group `E`, the inversion function is cobounded in the bornology of `E`, that is, for every bounded set `A`, the preimage of `A` under inversion is also bounded.
|
NormedAddCommGroup.dist_eq
theorem NormedAddCommGroup.dist_eq : ∀ {E : Type u_9} [self : NormedAddCommGroup E] (x y : E), dist x y = ‖x - y‖ := by
sorry
This theorem states that, for any type `E` that forms a Normed Additive Commutative Group, the distance between any two elements `x` and `y` of `E` is equal to the norm of their difference. Here, the norm function is represented by `‖x - y‖` and the distance function is represented by `dist x y`.
More concisely: For any Normed Additive Commutative Group `E` and elements `x` and `y` in `E`, the distance between `x` and `y` equals the norm of their difference: `dist x y = ‖x - y‖`.
|
MonoidHomClass.lipschitz_of_bound
theorem MonoidHomClass.lipschitz_of_bound :
∀ {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
[inst_2 : FunLike 𝓕 E F] [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ),
(∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → LipschitzWith C.toNNReal ⇑f
The theorem `MonoidHomClass.lipschitz_of_bound` states that for a given homomorphism `f` of seminormed groups, if there exists a real constant `C` such that for every element `x` in the domain, the norm of `f(x)` is less than or equal to `C` times the norm of `x`, then `f` is Lipschitz continuous with Lipschitz constant `C` (interpreted as a non-negative real number). This theorem is analogous to a similar condition for a linear map of normed or seminormed spaces, which can be found in the Lean Mathematical Library's analysis of normed spaces.
More concisely: If a homomorphism between seminormed groups satisfies the condition that the norm of the image of any element is less than or equal to a constant times the norm of the element, then the homomorphism is Lipschitz continuous with Lipschitz constant equal to that constant.
|
norm_sum_le
theorem norm_sum_le :
∀ {ι : Type u_9} {E : Type u_10} [inst : SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E),
‖s.sum fun i => f i‖ ≤ s.sum fun i => ‖f i‖
The theorem `norm_sum_le` states that for any finite set `s` of type `ι` and any function `f` from `ι` to a type `E` equipped with a seminorm (i.e., a type `E` that is a seminormed additive commutative group), the norm of the sum of `f(i)` over all `i` in `s` is less than or equal to the sum of the norms of `f(i)` for each `i` in `s`. In simpler terms, it says that the norm of the sum of a sequence of vectors is less than or equal to the sum of the norms of the vectors, a principle often encountered in vector spaces or more generally in seminormed groups.
More concisely: For any finite set `s` and function `f` from `s` to a seminormed additive commutative group `E`, the norm of the sum of `f(i)` for all `i` in `s` is less than or equal to the sum of the norms of `f(i)` for each `i` in `s`.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.24
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.24 :
∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, (y ∈ Metric.closedBall x ε) = (dist y x ≤ ε) := by
sorry
This theorem states that for any pseudometric space `α`, and given any two points `x` and `y` in `α` and a real number `ε`, the point `y` belongs to the closed ball centered at `x` with radius `ε` if and only if the distance between `y` and `x` is less than or equal to `ε`. This means that the `Metric.closedBall` function is correctly defined as the set of all points at a distance less than or equal to `ε` from the center point.
More concisely: For any pseudometric space `α` and points `x, y ∈ α`, the point `y` belongs to the closed ball centered at `x` with radius `ε` if and only if the distance `d(x, y) ≤ ε`.
|
Continuous.norm
theorem Continuous.norm :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
Continuous f → Continuous fun x => ‖f x‖
This theorem states that for any type `α` with a topological space structure, and any type `E` with a seminormed additive group structure, if a function `f` mapping from `α` to `E` is continuous, then the function that maps `α` to the norm of `f(x)` (denoted as `‖f x‖`) is also continuous. In other words, if a function is continuous in a topological space, its norm is also a continuous function.
More concisely: If `f : α → E` is a continuous function between a topological space `α` and a normed additive group `E`, then the function `x ↦ ‖f x‖` mapping `α` to the norms of `f(x)` is also continuous.
|
norm_mul_le_of_le
theorem norm_mul_le_of_le :
∀ {E : Type u_6} [inst : SeminormedGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ}, ‖a₁‖ ≤ r₁ → ‖a₂‖ ≤ r₂ → ‖a₁ * a₂‖ ≤ r₁ + r₂
This theorem states that for any seminormed group `E` and any elements `a₁` and `a₂` of `E`, along with any real numbers `r₁` and `r₂`, if the norm of `a₁` is less than or equal to `r₁` and the norm of `a₂` is less than or equal to `r₂`, then the norm of the product `a₁ * a₂` is less than or equal to `r₁ + r₂`. In mathematical terms, if ‖a₁‖ ≤ r₁ and ‖a₂‖ ≤ r₂, then ‖a₁ * a₂‖ ≤ r₁ + r₂.
More concisely: For any seminormed group and elements `a₁, a₂` with norms less than or equal to `r₁` and `r₂` respectively, the norm of their product is less than or equal to the sum of `r₁` and `r₂`.
|
dist_eq_norm_sub
theorem dist_eq_norm_sub : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), dist a b = ‖a - b‖
This theorem states that, for any seminormed add group `E` and any two elements `a` and `b` of `E`, the distance between `a` and `b` is equal to the norm of the difference between `a` and `b`. Here, `dist a b` represents the distance between `a` and `b`, and `‖a - b‖` represents the norm of the difference between `a` and `b`. This is a generalization of the familiar property from Euclidean space, where the distance between two points is the absolute value of the difference of their coordinates.
More concisely: For any seminormed add group `E` and elements `a, b` in `E`, the distance between `a` and `b` equals the norm of their difference: `dist a b = ‖a - b‖`.
|
norm_eq_of_mem_sphere
theorem norm_eq_of_mem_sphere :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {r : ℝ} (x : ↑(Metric.sphere 0 r)), ‖↑x‖ = r
This theorem, `norm_eq_of_mem_sphere`, states that for every type `E` which is a semi-normed addition group, and for every real number `r`, if `x` is a point in the metric sphere centered at the origin (0) with radius `r`, then the norm of `x` is equal to `r`. In mathematical terms, if a point `x` belongs to the sphere of radius `r` centered at the origin in a semi-normed addition group, then the norm of `x` (denoted as `‖x‖`) is equal to `r`.
More concisely: In a semi-normed additive group, the norm of a point in the metric sphere centered at the origin equals the sphere's radius.
|
LipschitzOnWith.norm_div_le
theorem LipschitzOnWith.norm_div_le :
∀ {E : Type u_6} {F : Type u_7} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {s : Set E} {f : E → F}
{C : NNReal}, LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
The theorem `LipschitzOnWith.norm_div_le` states that for a given nonnegative real number `C`, a function `f` from a normed group `E` to another normed group `F`, and a set `s` of elements from `E`, if `f` is Lipschitz continuous with constant `C` on `s`, then for any two elements `x` and `y` in `s`, the norm of the ratio of `f(x)` to `f(y)` is less than or equal to `C` times the norm of the ratio of `x` to `y`. In other words, the Lipschitz continuity of `f` on the set `s` implies a bound on the ratio of the norms of the images of any two points in `s` under `f`, in terms of the ratio of the norms of the points themselves.
More concisely: For a Lipschitz continuous function `f` from a normed group `E` to another normed group `F` with constant `C` on a set `s`, the norm of `f(x)/f(y)` is bounded above by `C` times the norm of `x/y` for any `x, y` in `s`.
|
norm_pow_le_mul_norm
theorem norm_pow_le_mul_norm : ∀ {E : Type u_6} [inst : SeminormedCommGroup E] (n : ℕ) (a : E), ‖a ^ n‖ ≤ ↑n * ‖a‖ := by
sorry
This theorem states that for any seminormed commutative group `E` and any element `a` of `E`, the norm of `a` raised to the power of a natural number `n` is less than or equal to `n` times the norm of `a`. Formally, for all `n` in ℕ and `a` in `E`, `‖a^n‖ ≤ n * ‖a‖`. This theorem holds for any Type `E` that has a seminormed commutative group structure.
More concisely: For any seminormed commutative group `E` and natural number `n`, the norm of `a` raised to the power of `n` in `E` is bounded above by `n` times the norm of `a`.
|
dist_eq_norm'
theorem dist_eq_norm' : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), dist a b = ‖b - a‖
This theorem, `dist_eq_norm'`, is a statement in the context of seminormed add groups. Given any two elements `a` and `b` from a seminormed add group `E`, the distance between `a` and `b` is defined to be the norm of the difference `b - a`. In other words, it provides an alternate expression for the distance between two points in such a group, namely as the norm (or length) of the vector representing the difference between the two points.
More concisely: In a seminormed add group, the distance between two elements is equal to the norm of their difference.
|
norm_sub_le
theorem norm_sub_le : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), ‖a - b‖ ≤ ‖a‖ + ‖b‖
This theorem, `norm_sub_le`, states that for any type `E` which is a seminormed add group, the norm of the difference between any two elements `a` and `b` of `E` is less than or equal to the sum of the norms of `a` and `b`. In mathematical terms, for any `a` and `b` in `E`, we have `‖a - b‖ ≤ ‖a‖ + ‖b‖`, where `‖‖` denotes the norm in the seminormed add group `E`.
More concisely: For any seminormed add group `E` and elements `a` and `b` in `E`, the norm of their difference is less than or equal to the sum of the norms of `a` and `b`: `‖a - b‖ ≤ ‖a‖ + ‖b‖`.
|
continuous_nnnorm
theorem continuous_nnnorm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E], Continuous fun a => ‖a‖₊
This theorem states that for any type `E` that has an instance of `SemionormedAddGroup`, the non-negative norm function, which takes a value `a` and returns its non-negative norm `‖a‖₊`, is continuous. In mathematical terms, if you have a seminormed additive group, the operation of finding the non-negative norm of any element in that group is a continuous operation.
More concisely: For any seminormed add group `E`, the non-negative norm function `‖._‖₊ : E → ℝ` is a continuous function.
|
nnnorm_le_insert'
theorem nnnorm_le_insert' : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊
This theorem, `nnnorm_le_insert'`, states that for any seminormed add group `E` of any type `u_6`, and any two elements `a` and `b` of this group, the nonnegative norm (denoted as `‖a‖₊`) of `a` is less than or equal to the sum of the nonnegative norm of `b` and the nonnegative norm of the difference `a - b` (denoted as `‖b‖₊ + ‖a - b‖₊`). Essentially, it's a statement of the triangle inequality in the context of a seminormed add group.
More concisely: For any seminormed add group (E, ‖·‖₊) and elements a, b in E, ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊.
|
dist_one_left
theorem dist_one_left : ∀ {E : Type u_6} [inst : SeminormedGroup E], dist 1 = norm
This theorem, named `dist_one_left`, states that for any type `E` which forms a seminormed group, the distance from the origin to `1` in this space is equal to the norm of the space. In mathematical terms, for any `E` where `E` is a seminormed group, the distance function `dist 1` is equivalent to the norm of the group.
More concisely: In a seminormed group `E`, the distance from the origin to `1` is equal to the norm of the identity element.
|
Bornology.IsBounded.exists_norm_le
theorem Bornology.IsBounded.exists_norm_le :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s → ∃ C, ∀ x ∈ s, ‖x‖ ≤ C := by
sorry
The theorem `Bornology.IsBounded.exists_norm_le` states that for any type `E` that is a `SeminormedAddGroup` and any set `s` of type `E`, if `s` is a bounded set relative to the given bornology on `E`, then there exists a constant `C` such that for all elements `x` in set `s`, the norm of `x` is less than or equal to `C`. This is essentially a formal statement of the property that a set is bounded if and only if there exists a constant that bounds the norm of all the elements within that set.
More concisely: For any seminormed add group `E` and bounded set `s` in `E`, there exists a constant `C` such that for all `x` in `s`, we have ||x|| ≤ C.
|
abs_norm_sub_norm_le
theorem abs_norm_sub_norm_le : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a b : E), |‖a‖ - ‖b‖| ≤ ‖a - b‖ := by
sorry
This theorem states that for any two elements `a` and `b` from a type `E` taking the guise of a seminormed add group, the absolute difference between their norms is less than or equal to the norm of their difference. In mathematical terms, it asserts that |‖a‖ - ‖b‖| ≤ ‖a - b‖ for any `a` and `b` in the seminormed add group `E`.
More concisely: For any elements `a` and `b` in a seminormed add group `E`, the triangle inequality holds: $|||a|| - ||b||| \leq ||a - b||$.
|
AddMonoidHomClass.continuous_of_bound
theorem AddMonoidHomClass.continuous_of_bound :
∀ {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
[inst_2 : FunLike 𝓕 E F] [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ),
(∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → Continuous ⇑f
The theorem `AddMonoidHomClass.continuous_of_bound` states that for a given homomorphism `f` of seminormed groups, if there exists a real constant `C` such that the norm of `f x` is less than or equal to `C` times the norm of `x` for all `x`, then the function `f` is continuous. This theorem applies to any types `𝓕`, `E`, and `F` where `𝓕` is a function from `E` to `F`, both `E` and `F` are seminormed add groups, and `𝓕` demonstrates the properties of an additive monoid homomorphism.
More concisely: If `f : E → F` is an additive homomorphism between seminormed add groups `E` and `F`, and there exists a constant `C` such that `‖f (x)‖ ≤ C * ‖x‖` for all `x` in `E`, then `f` is a continuous function.
|
Pi.nnnorm_def
theorem Pi.nnnorm_def :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (π i)]
(f : (i : ι) → π i), ‖f‖₊ = Finset.univ.sup fun b => ‖f b‖₊
The theorem `Pi.nnnorm_def` states that for any finite type `ι` (denoted as `Fintype ι`) and a function `f` that maps each element of `ι` to a seminormed add group `π i`, the nonnegative norm (denoted as `‖f‖₊`) of the function `f` is equal to the supremum (`Finset.sup`) of the nonnegative norms of the function `f` evaluated at each element in the universal finite set of type `Finset α` (denoted as `Finset.univ`). In mathematical terms, this could be written as: for all `f` from `ι` to `π i`, we have `‖f‖₊ = sup {‖f b‖₊ : b ∈ ι}`.
More concisely: The nonnegative norm of a function from a finite type to a seminormed add group is equal to the supremum of the nonnegative norms of the function evaluated at each element in the universal finite set.
|
nnnorm_neg
theorem nnnorm_neg : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), ‖-a‖₊ = ‖a‖₊
The theorem `nnnorm_neg` states that for any type `E` which is an instance of the `SemionormedAddGroup`, the non-negative norm of the negation of any element `a` from `E` is equal to the non-negative norm of `a` itself. In mathematical terms, this theorem expresses the property that negation doesn't change the non-negative norm of an element in a seminormed add group, i.e., ‖-a‖₊ = ‖a‖₊ for all `a` in `E`.
More concisely: For any element `a` in a seminormed add group `E`, the non-negative norm of `-a` is equal to the non-negative norm of `a`, i.e., ‖-a‖₊ = ‖a‖₊.
|
coe_nnnorm
theorem coe_nnnorm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), ↑‖a‖₊ = ‖a‖
This theorem, `coe_nnnorm`, states that for any instance `a` of a type `E`, which is a semi-normed add group, the non-negative real value of the norm of `a` is equal to the norm of `a`. In other words, it says that the norm of an element in a seminormed add group is always a non-negative real number, and when you convert this non-negative real number back into a real number, you get the original norm value.
More concisely: For any semi-normed add group element `a`, the norm of `a` equals its non-negative real value.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.40
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.40 :
∀ {E : Type u_6} [inst : SeminormedGroup E] (a : E), ‖a‖ = dist a 1
This theorem, `Mathlib.Analysis.Normed.Group.Basic._auxLemma.40`, states that for any element `a` of a seminormed group `E`, the norm of `a` is equal to the distance between `a` and `1`. In mathematical terms, this theorem asserts that for all `a` in `E`, ‖`a`‖ = dist(`a`, `1`). This relationship holds in any seminormed group, which is a group that is equipped with a seminorm, a generalization of the absolute value function that measures the "size" or "length" of elements in the group.
More concisely: In a seminormed group, the seminorm of an element is equal to its distance to the identity.
|
Pi.sum_norm_apply_le_norm'
theorem Pi.sum_norm_apply_le_norm' :
∀ {ι : Type u_4} {π : ι → Type u_9} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (π i)]
(f : (i : ι) → π i), (Finset.univ.sum fun i => ‖f i‖) ≤ Fintype.card ι • ‖f‖
This theorem states that for any function `f` mapping from a finite type `ι` to a set of semi-normed groups `π i`, the L^1 norm of `f` (the sum of the norms of `f i` for all `i` in `ι`) is less than or equal to the L^∞ norm of `f` (the `supremum` of the norms of `f i` for all `i` in `ι`) scaled by the cardinality of `ι`.
More concisely: For any function from a finite type to a set of semi-normed groups, the L^1 norm is less than or equal to the L^∞ norm multiplied by the size of the finite type.
|
edist_eq_coe_nnnorm
theorem edist_eq_coe_nnnorm : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (x : E), edist x 0 = ↑‖x‖₊
This theorem states that for any seminormed add group `E` and any element `x` in `E`, the extended distance (`edist`) between `x` and the zero element is equal to the non-negative real number equivalent (`↑‖x‖₊`) of the norm of `x`. In other words, in a seminormed add group, the distance from any point to the origin is precisely the norm of that point.
More concisely: For any seminormed add group `E` and its element `x`, the extended distance from `x` to the zero element equals the norm of `x`. (edist x 0 = ‖x‖₊)
|
Real.norm_of_nonneg
theorem Real.norm_of_nonneg : ∀ {r : ℝ}, 0 ≤ r → ‖r‖ = r
This theorem, `Real.norm_of_nonneg`, asserts that in the real number system, for every real number `r` that is nonnegative (i.e., `r` is greater than or equal to 0), the norm (or absolute value) of `r` is equal to `r` itself. It reflects the property of the norm function where it returns the input value for nonnegative numbers.
More concisely: For all real numbers `r`, if `r` is nonnegative, then the absolute value of `r` equals `r`.
|
dist_zero_left
theorem dist_zero_left : ∀ {E : Type u_6} [inst : SeminormedAddGroup E], dist 0 = norm
This theorem, `dist_zero_left`, states that for any type `E` that is an instance of a seminormed add group, the distance from zero is equal to the norm. In other words, in the context of a seminormed add group, the norm function can be used to measure the distance from the zero element.
More concisely: In a seminormed add group, the norm of an element is equal to its distance to the zero element.
|
norm_neg
theorem norm_neg : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), ‖-a‖ = ‖a‖
This theorem, `norm_neg`, states that for any type `E` that forms a semi-normed addition group, the norm of the negation of any element `a` in that group is equal to the norm of `a` itself. In mathematical terms, for a seminormed addition group `E`, for all `a` in `E`, the norm of `-a` is equal to the norm of `a`. This is usually denoted as `‖-a‖ = ‖a‖`.
More concisely: For any seminormed additive group `E`, the negation of an element `a` in `E` has the same norm as `a`, i.e., `‖-a‖ = ‖a‖`.
|
SeminormedGroup.dist_eq
theorem SeminormedGroup.dist_eq : ∀ {E : Type u_9} [self : SeminormedGroup E] (x y : E), dist x y = ‖x / y‖
This theorem states that in any seminormed group `E`, the distance between any two elements `x` and `y` of `E` is equal to the norm of the division of `x` by `y`. In the context of math, seminormed groups generalize the notion of normed vector spaces and the theorem essentially states that the metric induced by the seminorm (distance between elements) is equivalent to the norm of their quotient.
More concisely: In a seminormed group, the distance between two elements is equal to the norm of their quotient inverse (when it exists).
|
ofReal_norm_eq_coe_nnnorm
theorem ofReal_norm_eq_coe_nnnorm :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] (a : E), ENNReal.ofReal ‖a‖ = ↑‖a‖₊
This theorem, `ofReal_norm_eq_coe_nnnorm`, states that for all type `E` which is a seminormed add group, the extended nonnegative real number representation (`ENNReal`) of the norm of any element `a` of `E` is equal to the nonnegative real number (`ℝ≥0`) representation of the norm of `a`. In other words, the function `ENNReal.ofReal` applied to the norm of `a` (expressed as `‖a‖`) is equivalent to the nonnegative real number representation of the norm of `a` (expressed as `↑‖a‖₊`).
More concisely: For any seminormed add group `E` and its element `a`, the extended nonnegative real number representation of `‖a‖` equals the nonnegative real number representation of `‖a‖`. In Lean, this is represented as `ENNReal.ofReal ‖a‖ = ↑‖a‖₊`.
|
norm_one'
theorem norm_one' : ∀ {E : Type u_6} [inst : SeminormedGroup E], ‖1‖ = 0
This theorem, named `norm_one'`, states that for any given type `E` that forms a seminormed group, the norm of `1` is equal to `0`. In mathematical terms, it could be written as ‖1‖ = 0 for all seminormed groups `E`. This theorem is important in the field of functional analysis, where norms and seminorms are used to measure the size or length of elements in a vector space.
More concisely: For any seminormed group `E`, the norm of the identity element 1 is zero.
|
ContinuousAt.norm
theorem ContinuousAt.norm :
∀ {α : Type u_3} {E : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {a : α},
ContinuousAt f a → ContinuousAt (fun x => ‖f x‖) a
The theorem `ContinuousAt.norm` states that for any seminormed add group `E` and any topological space `α`, if a function `f : α → E` is continuous at a point `a` in `α`, then the function that takes `x` in `α` to the norm of `f x` is also continuous at `a`. In other words, if the function values `f x` approach `f a` as `x` approaches `a`, then the norms `‖f x‖` also approach `‖f a‖` as `x` approaches `a`.
More concisely: If `f : α → E` is a continuous function at `a ∈ α` in the seminormed add group `E`, then the norm function `x ↦ ||f x||` is also continuous at `a`.
|
Mathlib.Analysis.Normed.Group.Basic._auxLemma.34
theorem Mathlib.Analysis.Normed.Group.Basic._auxLemma.34 :
∀ {E : Type u_6} [inst : NormedAddGroup E] {a : E}, (‖a‖ ≤ 0) = (a = 0)
This theorem states that for any type `E` that forms a normed add group, the norm of an element `a` from `E` is less than or equal to zero if and only if `a` is zero. In mathematical terms, for a given element `a` in a normed add group `E`, the statement `‖a‖ ≤ 0` is equivalent to `a = 0`. A normed add group is a type of mathematical structure that combines a group and a vector space with a norm operation.
More concisely: In a normed add group, the element with zero norm is precisely the additive identity.
|
Filter.HasBasis.cobounded_of_norm
theorem Filter.HasBasis.cobounded_of_norm :
∀ {E : Type u_6} [inst : SeminormedAddGroup E] {ι : Sort u_9} {p : ι → Prop} {s : ι → Set ℝ},
Filter.atTop.HasBasis p s → (Bornology.cobounded E).HasBasis p fun i => norm ⁻¹' s i
This theorem states that, for any seminormed add group `E` and any set `s` of real numbers indexed by `ι` and filtered by a predicate `p`, if `Filter.atTop` has a basis given by `p` and `s`, then `Bornology.cobounded E` also has a basis, where the basis elements are the preimages of `s` under the norm function. In simpler terms, the theorem relates the behavior of a filter at positive infinity and a filter of cobounded sets in a bornology under the norm function, asserting the existence of a basis for the latter if one exists for the former.
More concisely: Given a seminormed add group `E`, a set `s` of real numbers indexed by `ι` filtered by a predicate `p`, and assuming `Filter.atTop` has a basis given by `p` and `s`, the bornology of cobounded sets in `E` has a basis consisting of the preimages of `s` under the norm function.
|
norm_le_insert'
theorem norm_le_insert' : ∀ {E : Type u_6} [inst : SeminormedAddGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖u - v‖
This theorem, named `norm_le_insert'`, is an alias of another theorem `norm_le_norm_add_norm_sub'`. It states a property pertaining to seminormed add groups of type `E`. For any two elements `u` and `v` of this seminormed add group, the theorem asserts that the norm of `u` (`‖u‖`) is less than or equal to the sum of the norm of `v` (`‖v‖`) and the norm of the difference between `u` and `v` (`‖u - v‖`).
More concisely: For any seminormed add group `E` and elements `u` and `v` in `E`, the norm of `u` is less than or equal to the sum of the norms of `v` and `u - v`.
|