mulRight_bound
theorem mulRight_bound :
∀ {α : Type u_1} [inst : NonUnitalSeminormedRing α] (x y : α), ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖
This theorem states that in a non-unital seminormed ring, the right-multiplication add monoid homomorphism is bounded. More specifically, for any two elements 'x' and 'y' from this ring, the norm of the result of applying the right-multiplication homomorphism on 'y' with 'x' as the multiplier is less than or equal to the product of the norms of 'x' and 'y'.
More concisely: In a non-unital seminormed ring, the norm of the right-multiplication by an element is bounded by the product of the norms of the element and the multiplier.
|
NNReal.nnnorm_eq
theorem NNReal.nnnorm_eq : ∀ (x : NNReal), ‖↑x‖₊ = x
This theorem establishes that for any nonnegative real number `x`, the nonnegative norm of `x` (denoted as `‖↑x‖₊`) is equal to `x` itself. In other words, when a nonnegative real number is lifted to a higher type (indicated by `↑x`), the nonnegative norm of the result remains unchanged and is the same as the original nonnegative real number. This property holds for all nonnegative real numbers.
More concisely: For all non-negative real numbers x, ‖↑x‖₊ = x holds. (The non-negative norm of a lifted non-negative real number is equal to the original number.)
|
SeminormedCommRing.mul_comm
theorem SeminormedCommRing.mul_comm : ∀ {α : Type u_5} [self : SeminormedCommRing α] (x y : α), x * y = y * x := by
sorry
The theorem `SeminormedCommRing.mul_comm` asserts that multiplication is commutative in a semi-normed commutative ring. Specifically, for any type `α` that is a semi-normed commutative ring, for any two elements `x` and `y` of `α`, the product `x * y` is equal to the product `y * x`. This is a fundamental property of multiplication in commutative algebraic structures.
More concisely: In a commutative semi-normed ring, multiplication is commutative. That is, for all elements x and y, x * y = y * x.
|
norm_pow_le'
theorem norm_pow_le' : ∀ {α : Type u_1} [inst : SeminormedRing α] (a : α) {n : ℕ}, 0 < n → ‖a ^ n‖ ≤ ‖a‖ ^ n
This theorem states that if `α` is a type that has a structure of a seminormed ring, then for any element `a` of type `α` and any natural number `n` greater than zero, the norm of `a` raised to the power `n` is less than or equal to the norm of `a` itself raised to the power `n`. In other words, in a seminormed ring, the norm of the power of an element does not exceed the power of the element's norm, for positive powers.
More concisely: In a seminormed ring, the norm of an element raised to any positive power is less than or equal to the norm of that element raised to the power of one.
|
NonUnitalNormedRing.dist_eq
theorem NonUnitalNormedRing.dist_eq : ∀ {α : Type u_5} [self : NonUnitalNormedRing α] (x y : α), dist x y = ‖x - y‖
The theorem `NonUnitalNormedRing.dist_eq` states that for any type `α` that forms a non-unital normed ring, the distance between any two elements `x` and `y` of the ring is equal to the norm of their difference, i.e., `dist x y = ‖x - y‖`.
More concisely: For any non-unital normed ring `α`, the distance between `x` and `y` is equal to the norm of their difference, i.e., `dist x y = ‖x - y‖`.
|
Filter.tendsto_inv₀_cobounded
theorem Filter.tendsto_inv₀_cobounded :
∀ {α : Type u_1} [inst : NormedDivisionRing α], Filter.Tendsto Inv.inv (Bornology.cobounded α) (nhds 0)
This theorem states that for any normed division ring `α`, the inverse function `Inv.inv` tends to the neighborhood filter at `0` when applied to the filter of cobounded sets in the bornology of `α`. In other words, for every neighborhood of `0`, the preimage of this neighborhood under the inverse function is a cobounded set in `α`. This is a generalized result in the field of topology, particularly dealing with concepts of limits and continuity of the inverse function in normed division rings.
More concisely: For any normed division ring `α`, the inverse function `Inv.inv` maps the filter of cobounded sets in the bornology of `α` to the neighborhood filter at `0`.
|
NormedRing.norm_mul
theorem NormedRing.norm_mul : ∀ {α : Type u_5} [self : NormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
The theorem `NormedRing.norm_mul` states that in any normed ring `α`, the norm function is submultiplicative. That is, for any two elements `a` and `b` in `α`, the norm of the product `a * b` is less than or equal to the product of the individual norms of `a` and `b`. In mathematical notation, this can be written as `‖a * b‖ ≤ ‖a‖ * ‖b‖`.
More concisely: In any normed ring, the norm of the product of two elements is less than or equal to the product of their individual norms. That is, `‖a * b‖ ≤ ‖a‖ * ‖b‖` for all `a, b` in the ring.
|
NormedAddCommGroup.tendsto_atTop
theorem NormedAddCommGroup.tendsto_atTop :
∀ {α : Type u_1} [inst : Nonempty α] [inst : SemilatticeSup α] {β : Type u_5} [inst_1 : SeminormedAddCommGroup β]
{f : α → β} {b : β},
Filter.Tendsto f Filter.atTop (nhds b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → ‖f n - b‖ < ε
This theorem is a restatement of `MetricSpace.tendsto_atTop` in terms of the norm for a normed add commutative group. It states that, given a function `f` from a nonempty type `α` with a supremum semilattice structure to a seminormed add commutative group `β`, the function `f` tends to a certain value `b` as `α` goes to infinity if and only if for every real number `ε` greater than zero, there exists an element `N` in `α` such that for every element `n` in `α` greater than or equal to `N`, the norm of the difference between `f(n)` and `b` is less than `ε`. This is a formal statement of the idea that the function `f` gets arbitrarily close to `b` as `α` gets arbitrarily large.
More concisely: A function from a nonempty type with a supremum semilattice structure to a seminormed add commutative group tends to a value in the group if and only if for every ε > 0, there exists an N such that for all n ≥ N, the norm of f(n) - the value is less than ε.
|
NonUnitalSeminormedRing.dist_eq
theorem NonUnitalSeminormedRing.dist_eq :
∀ {α : Type u_5} [self : NonUnitalSeminormedRing α] (x y : α), dist x y = ‖x - y‖
This theorem states that in any non-unital seminormed ring α, the distance between any two elements x and y is equivalent to the norm of the difference between x and y. In mathematical notation, this is expressed as `dist x y = ‖x - y‖`.
More concisely: In a non-unital seminormed ring, the distance between any two elements is equal to the norm of their difference.
|
norm_mul_le
theorem norm_mul_le : ∀ {α : Type u_1} [inst : NonUnitalSeminormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
This theorem states that for any non-unital semi-normed ring of type `α`, the norm of the product of any two elements `a` and `b` is less than or equal to the product of their norms. In mathematical notation, this can be written as `‖a * b‖ ≤ ‖a‖ * ‖b‖` for all `a, b` in the ring `α`. This theorem is a reflection of the sub-multiplicative property of norms in semi-normed rings.
More concisely: In any semi-normed ring, the product of two elements satisfies the norm inequality: $\|a \cdot b\| \leq \|a\| \cdot \|b\|$.
|
NormedField.exists_one_lt_norm
theorem NormedField.exists_one_lt_norm : ∀ (α : Type u_1) [inst : NontriviallyNormedField α], ∃ x, 1 < ‖x‖
This theorem states that for every non-trivial normed field `α`, there exists an element `x` in `α` whose norm is greater than 1. In other words, in any non-trivial normed field, we can always find an element whose length or magnitude (as determined by the field's norm function) is more than one.
More concisely: In every non-trivial normed field, there exists an element with norm greater than 1.
|
NonUnitalNormedRing.norm_mul
theorem NonUnitalNormedRing.norm_mul : ∀ {α : Type u_5} [self : NonUnitalNormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
This theorem states that in a non-unital normed ring, the norm of the product of two elements is less than or equal to the product of their norms. In other words, for any two elements `a` and `b` in a non-unital normed ring `α`, the inequality ‖a * b‖ ≤ ‖a‖ * ‖b‖ holds true. This property is known as submultiplicativity of the norm.
More concisely: In a non-unital normed ring, the norm of the product is less than or equal to the product of the norms. That is, ‖a * b‖ ≤ ‖a‖ * ‖b‖ for all `a` and `b` in the ring.
|
norm_pow_le
theorem norm_pow_le :
∀ {α : Type u_1} [inst : SeminormedRing α] [inst_1 : NormOneClass α] (a : α) (n : ℕ), ‖a ^ n‖ ≤ ‖a‖ ^ n
The theorem `norm_pow_le` states that for any seminormed ring `α` where the norm of 1 is equal to 1, the norm of `a` raised to the power `n` is less than or equal to the norm of `a` raised to the power `n`. In terms of mathematical notation, if `α` is a seminormed ring with `‖1‖ = 1`, then for any element `a` in `α` and any natural number `n`, we have `‖a ^ n‖ ≤ ‖a‖ ^ n`. This theorem is also related to `norm_pow_le'`.
More concisely: In a seminormed ring where the norm of 1 is 1, the norm of any element raised to a natural power is less than or equal to the norm raised to that power.
|
NormedField.exists_lt_norm
theorem NormedField.exists_lt_norm : ∀ (α : Type u_1) [inst : NontriviallyNormedField α] (r : ℝ), ∃ x, r < ‖x‖ := by
sorry
This theorem states that for any real number `r` and any non-trivial normed field `α`, there exists an element `x` in `α` such that the norm of `x` is greater than `r`. In other words, in every non-trivial normed field, one can find an element whose norm (also known as length or magnitude) exceeds any given real number.
More concisely: In every non-trivial normed field, there exists an element with a norm greater than any given real number.
|
NormedField.dist_eq
theorem NormedField.dist_eq : ∀ {α : Type u_5} [self : NormedField α] (x y : α), dist x y = ‖x - y‖
This theorem states that in any normed field, the distance between two elements, `x` and `y`, is equal to the norm of their difference. Here, `α` is the type representing the normed field, and `x` and `y` are elements of this field. In mathematical terms, this theorem translates to the equation: `dist(x, y) = ||x - y||`, where `dist` is the distance function, `||.||` is the norm, and `x` and `y` are elements in the normed field `α`.
More concisely: In a normed field, the distance between two elements is equal to the norm of their difference.
|
RingHomIsometric.is_iso
theorem RingHomIsometric.is_iso :
∀ {R₁ : Type u_5} {R₂ : Type u_6} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Norm R₁] [inst_3 : Norm R₂]
{σ : R₁ →+* R₂} [self : RingHomIsometric σ] {x : R₁}, ‖σ x‖ = ‖x‖
This theorem states that for any ring homomorphism `σ` from a semiring `R₁` to another semiring `R₂`, where both `R₁` and `R₂` have a norm, the homomorphism `σ` is an isometry. In other words, the norm of the image of any element `x` from `R₁` under the homomorphism `σ` is equal to the norm of `x` itself.
More concisely: For any ring homomorphism σ from a semiring equipped with a norm to another such semiring, σ preserves the norm, i.e., ||σ(x)|| = ||x|| for all x in the source semiring.
|
mulLeft_bound
theorem mulLeft_bound :
∀ {α : Type u_1} [inst : NonUnitalSeminormedRing α] (x y : α), ‖(AddMonoidHom.mulLeft x) y‖ ≤ ‖x‖ * ‖y‖
The theorem `mulLeft_bound` states that in a non-unital seminormed ring, the norm of left-multiplication by an element, considered as an additive monoid homomorphism, applied to another element, is less than or equal to the product of the norms of the two elements. In other words, for any two elements `x` and `y` of the ring, the norm of the result of left-multiplication by `x` on `y` is bounded by the product of the norms of `x` and `y`.
More concisely: In a non-unital seminormed ring, the norm of the left-multiplication by an element is less than or equal to the product of the norms of the element and the multiplicand.
|
norm_div
theorem norm_div : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a b : α), ‖a / b‖ = ‖a‖ / ‖b‖
This theorem states that for any normed division ring `α` and any elements `a` and `b` of `α`, the norm of the quotient `a / b` is equal to the quotient of the norms `‖a‖ / ‖b‖`. Here, the norm of an element in a normed division ring is a function that assigns a non-negative real number to each element such that it satisfies certain properties.
More concisely: In a normed division ring, the norm of the quotient of two elements is equal to the quotient of their respective norms.
|
norm_pow
theorem norm_pow : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a : α) (n : ℕ), ‖a ^ n‖ = ‖a‖ ^ n
This theorem is stating that for any normed division ring `α` and any element `a` of that ring, as well as any natural number `n`, the norm of `a` raised to the power of `n` is equal to the norm of `a` raised to the power of `n`. In mathematical terms, it says that for all `a` in `α` and for all natural numbers `n`, `||a^n|| = ||a||^n`.
More concisely: For any normed division ring `α` and element `a` in `α`, the norm of `a` raised to the power of a natural number `n` equals the norm of `a` raised to the power of `n`. In other words, `||a^n|| = ||a||^n`.
|
NonUnitalSeminormedCommRing.mul_comm
theorem NonUnitalSeminormedCommRing.mul_comm :
∀ {α : Type u_5} [self : NonUnitalSeminormedCommRing α] (x y : α), x * y = y * x
This theorem states that multiplication is commutative in a non-unital seminormed commutative ring. In other words, for any two elements `x` and `y` of a type `α`, where `α` is a non-unital seminormed commutative ring, the result of multiplying `x` by `y` is the same as the result of multiplying `y` by `x`.
More concisely: In a commutative, non-unital seminormed ring, multiplication is commutative: `x * y = y * x` for all `x` and `y` in the ring.
|
DenselyNormedField.lt_norm_lt
theorem DenselyNormedField.lt_norm_lt :
∀ {α : Type u_5} [self : DenselyNormedField α] (x y : ℝ), 0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y
This theorem states that for any densely normed field `α`, and any two non-negative real numbers `x` and `y` such that `x` is less than `y`, there exists an element `a` in the field `α` whose norm is greater than `x` and less than `y`. In other words, the norm function maps elements of `α` onto the entire non-negative real number line, filling it densely.
More concisely: For any densely normed field `α`, given `x` and `y` in the real numbers with `x < y`, there exists an element `a` in `α` such that `‖a‖ > x` and `‖a‖ < y`.
|
NormedField.norm_mul'
theorem NormedField.norm_mul' : ∀ {α : Type u_5} [self : NormedField α] (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
This theorem states that the norm function in a Normed Field is multiplicative. Specifically, for any type `α` that has a Normed Field structure, the norm of the product of two elements `a` and `b` (denoted as `‖a * b‖`) is equal to the product of their norms (denoted as `‖a‖ * ‖b‖`). That is, the norm preserves the multiplication operation.
More concisely: For any normed field `α`, the norm function satisfies the multiplicative property: `‖a * b‖ = ‖a‖ * ‖b‖`, where `a` and `b` are elements of `α`.
|
NormedAddCommGroup.tendsto_atTop'
theorem NormedAddCommGroup.tendsto_atTop' :
∀ {α : Type u_1} [inst : Nonempty α] [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] {β : Type u_5}
[inst_2 : SeminormedAddCommGroup β] {f : α → β} {b : β},
Filter.Tendsto f Filter.atTop (nhds b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N < n → ‖f n - b‖ < ε
This theorem, `NormedAddCommGroup.tendsto_atTop'`, states that for any non-empty type `α` with a supremum semilattice structure and no maximum element, and any semi-normed additive commutative group `β`, a function `f` from `α` to `β` tends to a limit `b` as `α` goes to infinity (represented by `Filter.Tendsto f Filter.atTop (nhds b)`) if and only if for every positive real number `ε`, there exists an element `N` in `α` such that for all elements `n` in `α` greater than `N`, the semi-norm of `f n - b` is less than `ε`. This is essentially a variation of the epsilon-N definition of limits, but with a strict inequality for `n`.
More concisely: A function from a non-empty type with a supremum semilattice structure and no maximum element to a semi-normed additive commutative group tends to a limit if and only if for every positive real number ε, there exists an element N such that for all n greater than N, the semi-norm of fn - b < ε.
|
NormedCommRing.mul_comm
theorem NormedCommRing.mul_comm : ∀ {α : Type u_5} [self : NormedCommRing α] (x y : α), x * y = y * x
This theorem states that multiplication is commutative in a normed commutative ring. Specifically, for all types α that form a normed commutative ring, for any elements x and y of α, the product of x and y equals the product of y and x. That is, swapping the order of multiplication doesn't change the result, which is the formal definition of commutativity in multiplication.
More concisely: In a commutative normed ring, multiplication is commutative, that is, x * y = y * x for all elements x and y.
|
NormedDivisionRing.norm_mul'
theorem NormedDivisionRing.norm_mul' : ∀ {α : Type u_5} [self : NormedDivisionRing α] (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
The theorem `NormedDivisionRing.norm_mul'` states that the norm function is multiplicative in a Normed Division Ring. Specifically, for any elements `a` and `b` from a specified Normed Division Ring `α`, the norm of the product `a * b` is equal to the product of the norms of `a` and `b`. In mathematical terms, this can be written as ‖a * b‖ = ‖a‖ * ‖b‖.
More concisely: In a Normed Division Ring, the norm of the product of two elements is equal to the product of their norms. That is, ‖a * b‖ = ‖a‖ * ‖b‖ for all elements a and b from the ring.
|
SeminormedRing.norm_mul
theorem SeminormedRing.norm_mul : ∀ {α : Type u_5} [self : SeminormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
This theorem states that for any seminormed ring of type `α`, the norm of the product of any two elements `a` and `b` is less than or equal to the product of the norms of `a` and `b`. This property is known as the submultiplicativity of the norm. In mathematical notation, this is expressed as ‖a * b‖ ≤ ‖a‖ * ‖b‖.
More concisely: The norm of the product of two elements in a seminormed ring is less than or equal to the product of their individual norms. (‖a * b‖ ≤ ‖a‖ * ‖b‖)
|
norm_mul
theorem norm_mul : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
This theorem, `norm_mul`, states that for all elements `a` and `b` in a normed division ring `α`, the norm of the product of `a` and `b` (`‖a * b‖`) is equal to the product of the norms of `a` and `b` (`‖a‖ * ‖b‖`). In other words, it confirms the property of multiplicative compatibility with a norm in a normed division ring, which means that the norm of a product is the product of the norms.
More concisely: For all elements `a` and `b` in a normed division ring `α`, `‖a * b‖ = ‖a‖ * ‖b‖`.
|
NormOneClass.induced
theorem NormOneClass.induced :
∀ {F : Type u_8} (R : Type u_9) (S : Type u_10) [inst : Ring R] [inst_1 : SeminormedRing S]
[inst_2 : NormOneClass S] [inst_3 : FunLike F R S] [inst_4 : RingHomClass F R S] (f : F), NormOneClass R
The theorem `NormOneClass.induced` states that for any type `F`, and types `R` and `S` with `R` being a ring, `S` being a seminormed ring, `S` having a norm of one (`NormOneClass`), and `F` being a function from `R` to `S` that respects the ring structure (`RingHomClass`), if there exists a ring homomorphism from `R` to `S` that induces the seminormed ring structure on `R`, then `R` also has a norm of one. In other words, if the norm of one in `S` is one, then the induced norm of one in `R` via the ring homomorphism is also one.
More concisely: If `F` is a ring homomorphism from a ring `R` to a seminormed ring `S` with norm one, and `S` induces a norm on `R`, then `R` also has a norm of one.
|
nnnorm_pow_le
theorem nnnorm_pow_le :
∀ {α : Type u_1} [inst : SeminormedRing α] [inst_1 : NormOneClass α] (a : α) (n : ℕ), ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n := by
sorry
This theorem states that, for any seminormed ring `α` where the non-negative norm of `1` is `1`, the non-negative norm of any element `a` raised to the `n`th power is less than or equal to the non-negative norm of `a` raised to the `n`th power. In other words, if `α` is a seminormed ring with `‖1‖₊ = 1`, then `‖a ^ n‖₊ ≤ ‖a‖₊ ^ n` for any `a` in `α` and any natural number `n`. This is a statement about the behavior of norms in seminormed rings.
More concisely: In a seminormed ring with norm of 1 for 1, the norm of any element raised to any natural power is bounded above by the norm of that element raised to the same power.
|
NonUnitalNormedCommRing.mul_comm
theorem NonUnitalNormedCommRing.mul_comm :
∀ {α : Type u_5} [self : NonUnitalNormedCommRing α] (x y : α), x * y = y * x
This theorem states that multiplication is commutative in a non-unital normed commutative ring. In other words, for any given type `α` that has a structure of a non-unital normed commutative ring, the order in which two elements `x` and `y` of type `α` are multiplied does not matter; the result of `x` multiplied by `y` is the same as `y` multiplied by `x`.
More concisely: In a non-unital normed commutative ring, multiplication is commutative.
|
Filter.inv_cobounded₀
theorem Filter.inv_cobounded₀ :
∀ {α : Type u_1} [inst : NormedDivisionRing α], (Bornology.cobounded α)⁻¹ = nhdsWithin 0 {0}ᶜ
The theorem `Filter.inv_cobounded₀` states that for any normed division ring `α`, the inverse of the filter of cobounded sets in the bornology of `α` is equal to the "neighborhood within" filter at 0 for the set that is the complement of the singleton set containing 0. In other words, this theorem is establishing a relationship between two different ways of describing certain types of "large" sets in a normed division ring: one using the concept of a cobounded set in a bornology, and the other using the concept of a "neighborhood within" a certain set.
More concisely: The filter of cobounded sets in the bornology of a normed division ring is equal to the "neighborhood within" filter at 0 for the set of sets containing 0 as an interior point.
|
NormedRing.dist_eq
theorem NormedRing.dist_eq : ∀ {α : Type u_5} [self : NormedRing α] (x y : α), dist x y = ‖x - y‖
This theorem, `NormedRing.dist_eq`, states that for any type `α` that is a Normed Ring, the distance between any two elements `x` and `y` of type `α` is equal to the norm of the difference between `x` and `y`. The term 'distance' here is based on the metric space structure induced by the norm, which is a function assigning a non-negative real number to each member of the Normed Ring in such a way that the distance between any two members is zero if and only if they are identical.
More concisely: For any Normed Ring `α`, the metric induced by its norm is such that `||x - y|| = d(x, y)` for all `x, y` in `α`, where `||.||` is the norm and `d(.,.)` is the metric.
|
NonUnitalSeminormedRing.norm_mul
theorem NonUnitalSeminormedRing.norm_mul :
∀ {α : Type u_5} [self : NonUnitalSeminormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
This theorem states that in a non-unital semi-normed ring (a ring which might not have a multiplicative identity, but has a norm function defined), the norm of the product of two elements is less than or equal to the product of their norms. More formally, for any two elements `a` and `b` in such a ring `α`, the norm of `a` multiplied by `b` is always less than or equal to the norm of `a` times the norm of `b`. In the context of the theorem, the norm of an element is denoted by `‖a‖` or `‖b‖`. This property is known as the submultiplicativity of the norm.
More concisely: In a non-unital semi-normed ring, the norm of the product of any two elements is less than or equal to the product of their individual norms. (i.e., ‖ab‖ ≤ ‖a‖ * ‖b‖)
|
nnnorm_mul
theorem nnnorm_mul : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a b : α), ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊
This theorem states that for any type `α` that forms a Normed Division Ring, the non-negative norm of the product of any two elements `a` and `b` from `α` is equal to the product of the non-negative norms of `a` and `b`. In mathematical terms, this can be written as ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊ for all `a` and `b` in `α`.
More concisely: For any normed division ring `α`, the norm of the product of two elements `a` and `b` is equal to the product of their norms: `‖a * b‖₊ = ‖a‖₊ * ‖b‖₊`.
|
norm_inv
theorem norm_inv : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a : α), ‖a⁻¹‖ = ‖a‖⁻¹
This theorem, titled "norm_inv", states that for any type `α` that forms a normed division ring, the norm of the inverse of any element `a` from `α` is equal to the inverse of the norm of `a`. In mathematical terms, this is saying that ‖a⁻¹‖ = ‖a‖⁻¹ for any `a` in `α`.
More concisely: For any normed division ring `α`, the norm of the multiplicative inverse of any `a` in `α` is the reciprocal of the norm of `a`.
|
NontriviallyNormedField.non_trivial
theorem NontriviallyNormedField.non_trivial : ∀ {α : Type u_5} [self : NontriviallyNormedField α], ∃ x, 1 < ‖x‖ := by
sorry
This theorem states that in any nontrivially normed field, there exists an element whose norm exceeds 1. In other words, for any type `α` that has a `NontriviallyNormedField` structure, there is an element `x` such that the norm of `x` (`‖x‖`) is greater than 1.
More concisely: In any nontrivially normed field, there exists an element with norm greater than 1.
|
Mathlib.Analysis.Normed.Field.Basic._auxLemma.3
theorem Mathlib.Analysis.Normed.Field.Basic._auxLemma.3 : ∀ {α : Type u} [inst : Preorder α] {a : α}, (a ≤ a) = True
This theorem states that for any type `α` with a preorder relation defined on it and any element `a` of type `α`, the proposition that `a` is less than or equal to itself is always true. This is a reflection of the reflexivity property of preorders in mathematics, where for any element in a set, it is always less than or equal to itself.
More concisely: For any preorder `α` and its element `a`, `a ≤ a` holds true.
|
norm_norm
theorem norm_norm : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] (x : α), ‖‖x‖‖ = ‖x‖
This theorem states that for all elements `x` of a given type `α`, where `α` is a seminormed add commutative group, the norm of the norm of `x` is equal to the norm of `x`. In mathematical terms, this is stating that for any `x` in our group, ||||x|||| = ||x||. This theorem is essentially saying that applying the norm function twice doesn't change the result; the norm of `x` is the same whether you calculate it once or twice.
More concisely: The norm of an element in a seminormed add commutative group is equal to the square of its norm.
|
nnnorm_inv
theorem nnnorm_inv : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a : α), ‖a⁻¹‖₊ = ‖a‖₊⁻¹
This theorem states that for every element `a` of a normed division ring `α`, the non-negative norm of the inverse of `a` is equal to the inverse of the non-negative norm of `a`. This is often expressed in mathematical notation as ‖a⁻¹‖₊ = ‖a‖₊⁻¹. This theorem holds under the assumption that `α` is a normed division ring, which is a particular kind of structured mathematical set.
More concisely: In a normed division ring, the non-negative norm of an element's inverse is equal to the reciprocal of its non-negative norm. (‖a⁻¹‖₊ = ‖a‖₊⁻¹)
|
nnnorm_pow_le'
theorem nnnorm_pow_le' : ∀ {α : Type u_1} [inst : SeminormedRing α] (a : α) {n : ℕ}, 0 < n → ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n := by
sorry
This theorem states that for any seminormed ring 'α', and any element 'a' of 'α', the non-negative norm (‖ ‖₊) of 'a' raised to any positive integer 'n' is always less than or equal to the non-negative norm of 'a' raised to 'n'. In other words, the norm of a power is less than or equal to the power of the norm in a seminormed ring. This is a general property in the context of seminormed rings.
More concisely: For any seminormed ring 'α' and positive integer 'n', the norm of an element 'a' in 'α' raised to the power 'n' is less than or equal to the norm of 'a' raised to the power 'n' (i.e., ‖aⁱ‖₊ ≤ ‖aⁱ‖₊).
|
List.norm_prod_le'
theorem List.norm_prod_le' :
∀ {α : Type u_1} [inst : SeminormedRing α] {l : List α}, l ≠ [] → ‖l.prod‖ ≤ (List.map norm l).prod
This theorem, `List.norm_prod_le'`, states that for any given list `l` of elements of a type `α`, where `α` is a seminormed ring, if the list `l` is not empty, the norm of the product of all elements in `l` is less than or equal to the product of the norms of all elements in `l`. In mathematical terms, if we denote the list as $l = [a_1, a_2, ..., a_n]$, the theorem states that $\| a_1 \times a_2 \times ... \times a_n \| \leq \|a_1\| \times \|a_2\| \times ... \times \|a_n\|$.
More concisely: For any non-empty list `l` of elements from a seminormed ring `α`, the norm of their product is less than or equal to the product of their individual norms: $\| \prod_{i=1}^n a\_i \| \leq \prod_{i=1}^n \|a\_i\|$.
|
NormOneClass.norm_one
theorem NormOneClass.norm_one : ∀ {α : Type u_5} [inst : Norm α] [inst_1 : One α] [self : NormOneClass α], ‖1‖ = 1 := by
sorry
This theorem states that for any type `α`, given that `α` is equipped with a norm and a multiplicative identity, and assuming `α` belongs to the `NormOneClass` class, the norm of the multiplicative identity (denoted as `1`) is equal to `1`. In mathematical terms, if `‖‧‖` is a norm on `α` and `α` has a multiplicative identity, then the norm of this identity is `1`.
More concisely: For any type `α` equipped with a norm and a multiplicative identity belonging to the `NormOneClass`, the norm of the identity is equal to 1.
|
NormedField.exists_norm_lt
theorem NormedField.exists_norm_lt :
∀ (α : Type u_1) [inst : NontriviallyNormedField α] {r : ℝ}, 0 < r → ∃ x, 0 < ‖x‖ ∧ ‖x‖ < r
This theorem states that for any nontrivially normed field `α` and any positive real number `r`, there exists an element `x` in `α` such that the norm of `x` is positive and less than `r`. In other words, we can always find an element in the normed field whose norm is between 0 and any given positive real number.
More concisely: For any nontrivially normed field `α` and positive real number `r`, there exists an element `x` in `α` with `0 < ||x|| < r`.
|
Filter.tendsto_mul_right_cobounded
theorem Filter.tendsto_mul_right_cobounded :
∀ {α : Type u_1} [inst : NormedDivisionRing α] {a : α},
a ≠ 0 → Filter.Tendsto (fun x => x * a) (Bornology.cobounded α) (Bornology.cobounded α)
The theorem `Filter.tendsto_mul_right_cobounded` states that for any type `α` that forms a normed division ring, and for any non-zero element `a` of type `α`, the function `f(x) = x * a` tends to infinity as `x` tends to infinity. This means that for every neighbourhood of infinity in the `α` space, the preimage under `f` of this neighbourhood is a neighbourhood of infinity in the cobounded filter of `α`, where the cobounded filter of `α` is defined as the filter of cobounded sets in a bornology. In other words, as `x` gets arbitrarily large, `x * a` also gets arbitrarily large, provided that `a` is not zero.
More concisely: For any normed division ring type `α` and non-zero element `a` of `α`, the function `x ↦ x * a` tends to infinity in the cobounded filter as `x` approaches infinity.
|
eventually_norm_pow_le
theorem eventually_norm_pow_le :
∀ {α : Type u_1} [inst : SeminormedRing α] (a : α), ∀ᶠ (n : ℕ) in Filter.atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n
This theorem, `eventually_norm_pow_le`, states that for every type `α` which forms a seminormed ring, for any element `a` of `α`, after a certain natural number `n`, the norm of `a` to the power of `n` is less than or equal to the norm of `a` itself to the power of `n`. In other words, `∀ᶠ (n : ℕ) in Filter.atTop` means that this inequality holds eventually as `n` goes to infinity.
More concisely: For every seminormed ring `α` and element `a` in `α`, there exists a natural number `n` such that for all `m ≥ n`, the norm of `a` raised to the power of `m` is less than or equal to the norm of `a` raised to the power of `n`.
|
NormedDivisionRing.dist_eq
theorem NormedDivisionRing.dist_eq : ∀ {α : Type u_5} [self : NormedDivisionRing α] (x y : α), dist x y = ‖x - y‖ := by
sorry
This theorem states that for any given type `α`, which is a Normed Division Ring, the distance between any two elements `x` and `y` of this type is equal to the norm of the difference between `x` and `y`. In mathematical terms, this is written as `dist(x, y) = ||x - y||`. The norm here is a function that assigns a strictly positive length or size to each vector in a vector space, except for the zero vector which is assigned a length of zero.
More concisely: For any Normed Division Ring `α`, the distance between elements `x` and `y` is equal to the norm of their difference: `dist(x, y) = ||x - y||`.
|
nnnorm_one
theorem nnnorm_one :
∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] [inst_1 : One α] [inst_2 : NormOneClass α], ‖1‖₊ = 1
This theorem states that for any type `α` that is a semi-normed addition commutative group with a unit element and adheres to the `NormOneClass` (meaning the norm of the unit element equals one), the non-negative norm (notated as `‖1‖₊`) of the unit element (`1`) is `1`.
More concisely: For any commutative semINormed additive group `α` with a unit element and `NormOneClass`, the norm of the unit element equals 1.
|
Filter.tendsto_mul_left_cobounded
theorem Filter.tendsto_mul_left_cobounded :
∀ {α : Type u_1} [inst : NormedDivisionRing α] {a : α},
a ≠ 0 → Filter.Tendsto (fun x => a * x) (Bornology.cobounded α) (Bornology.cobounded α)
The theorem `Filter.tendsto_mul_left_cobounded` asserts that for any normed division ring `α` and any non-zero element `a` of `α`, the function which multiplies each element of `α` by `a` has a property that it tends to infinity as we move towards the boundary of `α` (formally, within the filter of cobounded sets in a bornology of `α`). This "tending to infinity" is expressed in terms of filter: for any set in the filter of cobounded sets of `α` (which can be seen as a "neighborhood" of infinity), the preimage under the multiplication function is also in the filter, i.e., it is also a cobounded set, or equivalently, the function's values become unboundedly large.
More concisely: For any normed division ring α and non-zero element a, the function multiplying elements by a is tendsto (in the filter of cobounded sets) to infinity.
|
SeminormedRing.dist_eq
theorem SeminormedRing.dist_eq : ∀ {α : Type u_5} [self : SeminormedRing α] (x y : α), dist x y = ‖x - y‖
This theorem states that in a semi-normed ring α, the distance between any two elements x and y is defined by the norm of the difference between x and y. In mathematical notation, this is expressed as dist(x, y) = ‖x - y‖. Here, dist refers to the metric or distance function, and ‖.‖ indicates the norm function. This theorem shows the connection between the norm and the metric in the context of a semi-normed ring.
More concisely: In a semi-normed ring, the metric is given by the norm of the difference between any two elements.
|