NormedOrderedGroup.dist_eq
theorem NormedOrderedGroup.dist_eq : ∀ {α : Type u_2} [self : NormedOrderedGroup α] (x y : α), dist x y = ‖x / y‖ := by
sorry
This theorem states that, for any two elements `x` and `y` of a type `α` that forms a Normed Ordered Group, the distance between `x` and `y` is equal to the norm of the ratio `x / y`. In mathematical notation, we might express this as `dist(x, y) = ‖x / y‖` for all `x, y ∈ α`. This theorem essentially provides a relationship between the concept of distance and the norm operation in the context of Normed Ordered Groups.
More concisely: In a Normed Ordered Group, the distance between two elements is equal to the norm of their quotient.
|
NormedLinearOrderedAddGroup.dist_eq
theorem NormedLinearOrderedAddGroup.dist_eq :
∀ {α : Type u_2} [self : NormedLinearOrderedAddGroup α] (x y : α), dist x y = ‖x - y‖
This theorem states that for any normed linear ordered additive group `α`, the distance between any two elements `x` and `y` in this group is equal to the norm of their difference. In mathematical notation, this is represented as `dist(x, y) = ‖x - y‖`. The theorem is valid for all instances `x` and `y` of the type `α`.
More concisely: For any normed linear ordered additive group `α`, the distance between any two elements `x` and `y` is equal to the norm of their difference: `dist(x, y) = ‖x - y‖`.
|
NormedLinearOrderedField.norm_mul'
theorem NormedLinearOrderedField.norm_mul' :
∀ {α : Type u_2} [self : NormedLinearOrderedField α] (x y : α), ‖x * y‖ = ‖x‖ * ‖y‖
This theorem states that the norm operation in a normed linear ordered field is multiplicative. In more detail, for any two elements `x` and `y` in a normed linear ordered field `α`, the norm of the product of `x` and `y` is equal to the product of the norm of `x` and the norm of `y`. We can express this mathematically as ‖x * y‖ = ‖x‖ * ‖y‖.
More concisely: The norm of the product of two elements in a normed linear ordered field is equal to the product of their individual norms.
|
NormedLinearOrderedField.dist_eq
theorem NormedLinearOrderedField.dist_eq :
∀ {α : Type u_2} [self : NormedLinearOrderedField α] (x y : α), dist x y = ‖x - y‖
This theorem states that for any normed linear ordered field `α`, the distance function between two elements `x` and `y` of `α` is induced by the norm of the difference between `x` and `y`. In other words, the distance between `x` and `y` is equal to the norm of `x - y`.
More concisely: For any normed linear ordered field `α`, the distance between `x` and `y` equals the norm of `x - y`.
|
NormedLinearOrderedGroup.dist_eq
theorem NormedLinearOrderedGroup.dist_eq :
∀ {α : Type u_2} [self : NormedLinearOrderedGroup α] (x y : α), dist x y = ‖x / y‖
This theorem states that in any normed linear ordered group, the distance between any two elements `x` and `y` is equal to the norm of the quotient `x / y`. Here, `α` is a type representing the normed linear ordered group, `x` and `y` are elements of `α`, and `‖x / y‖` represents the norm of `x / y`. The norm function `‖_‖` 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. The distance function, denoted by `dist`, measures the distance between two elements in the group.
More concisely: In a normed linear ordered group, the distance between two elements is equal to the norm of their quotient.
|
NormedOrderedAddGroup.dist_eq
theorem NormedOrderedAddGroup.dist_eq :
∀ {α : Type u_2} [self : NormedOrderedAddGroup α] (x y : α), dist x y = ‖x - y‖
This theorem states that for any normed ordered add group `α` and any two elements `x` and `y` of `α`, the distance between `x` and `y` is equal to the norm of the difference between `x` and `y` (denoted as `‖x - y‖`). Here, 'normed ordered add group' is a kind of mathematical structure that has a notion of distance (or norm), addition, and an order consistent with these operations.
More concisely: For any normed ordered add group `α`, the distance between two elements `x` and `y` is equal to the norm of their difference: `‖x - y‖ = d(x, y)`.
|