dist_vsub_cancel_right
theorem dist_vsub_cancel_right :
∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] (x y z : P), dist (x -ᵥ z) (y -ᵥ z) = dist x y
This theorem, `dist_vsub_cancel_right`, states that for any three points `x, y, z` in a pseudometric space `P`, which is a normed add torsor over a seminormed add commutative group `V`, the distance between `(x - z)` and `(y - z)` is the same as the distance between `x` and `y`. Here, the `-ᵥ` operation represents the difference of the vectors pointing to `x` and `z`, and `y` and `z`, respectively. In other words, subtracting the same point `z` from two other points `x` and `y` does not change the distance between `x` and `y`.
More concisely: In a pseudometric space over a seminormed add commutative group, the distance between `(x - z)` and `(y - z)` equals the distance between `x` and `y`, for any points `x`, `y`, and `z`.
|
dist_vadd_left
theorem dist_vadd_left :
∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] (v : V) (x : P), dist (v +ᵥ x) x = ‖v‖
This theorem, `dist_vadd_left`, states that for any vector `v` and point `x`, where `V` is a seminormed add commutative group and `P` is a pseudometric space with `V` acting on `P` in a normed add torsor fashion, the distance between the translated point `v +ᵥ x` and the original point `x` is equal to the norm of the vector `v`. In other words, the distance function behaves as expected when translating a point along a vector in a vector space with a norm and pseudometric.
More concisely: For any vector `v` in a seminormed add commutative group `V` and point `x` in a pseudometric space `P` with `V` acting on `P` as a normed add torsor, the distance between `x` and `v +_× x` is equal to the norm of `v`.
|
Continuous.vsub
theorem Continuous.vsub :
∀ {α : Type u_1} {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] [inst_3 : TopologicalSpace α] {f g : α → P},
Continuous f → Continuous g → Continuous (f -ᵥ g)
This theorem states that for any types `α`, `V`, and `P`, if `V` is a semi-normed additive commutative group, `P` is a pseudo metric space, and `V` is a normed add-torsor over `P`, and if `α` is a topological space, then for any two functions `f` and `g` from `α` to `P`, if both `f` and `g` are continuous, then their group difference (defined as `f -ᵥ g`) is also continuous. This theorem is a statement about the continuity of the difference of two continuous functions in the context of normed add-torsors.
More concisely: If `V` is a normed add-torsor over a pseudo metric space `P`, and `α` is a topological space, then for any two continuous functions `f` and `g` from `α` to `P`, their group difference `f -ᵥ g` is also continuous.
|
dist_vadd_cancel_right
theorem dist_vadd_cancel_right :
∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] (v₁ v₂ : V) (x : P), dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
The theorem `dist_vadd_cancel_right` states that for any types `V` and `P`, where `V` is a seminormed add commutative group and `P` is a pseudometric space, and `V` acts on `P` as a normed add torsor, the distance between the point obtained by adding a vector `v₁` to a point `x` and the point obtained by adding a vector `v₂` to the same point `x` is equal to the distance between `v₁` and `v₂`. This essentially means that adding the same point `x` to two vectors `v₁` and `v₂` does not change the distance between `v₁` and `v₂`.
More concisely: For any seminormed add commutative group `V` and pseudometric space `P`, if `V` acts on `P` as a normed add torsor, then the distance between `x + v₁` and `x + v₂` equals the distance between `v₁` and `v₂` for all `x` in `P` and `v₁`, `v₂` in `V`.
|
Filter.Tendsto.vsub
theorem Filter.Tendsto.vsub :
∀ {α : Type u_1} {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] {l : Filter α} {f g : α → P} {x y : P},
Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (f -ᵥ g) l (nhds (x -ᵥ y))
This theorem states that for any types `α`, `V`, and `P`, given `V` is a seminormed add commutative group, `P` is a pseudometric space, and `V` is a normed add-torsor over `P`. If `f` and `g` are functions from `α` to `P`, and `l` is a filter on `α`; if `f` tends to `x` and `g` tends to `y` (in the sense that for every neighborhood of `x` and `y`, the preimage of that neighborhood under `f` and `g` respectively is eventually in `l`), then the difference `(f -ᵥ g)` tends to `(x -ᵥ y)` (in the same sense of "tends to" as before).
More concisely: Given functions `f` and `g` from type `α` to a seminormed add commutative group `V`, which is a normed add-torsor over a pseudometric space `P`, if `f` converges to `x` and `g` converges to `y` (in the sense of having preimages of every neighborhood of `x` and `y` eventually in a given filter `l`), then their difference `f -ᵥ g` converges to `x -ᵥ y`.
|
dist_eq_norm_vsub'
theorem dist_eq_norm_vsub' :
∀ (V : Type u_2) {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] (x y : P), dist x y = ‖y -ᵥ x‖
This theorem states that the distance between two points, `x` and `y`, in a pseudometric space `P` over a seminormed additive commutative group `V` (which is also a normed additive torsor) is equal to the norm of the vector obtained by subtracting `x` from `y`. It's important to explicitly specify `V` as an argument in this theorem, as without it, rewriting using `dist_eq_norm_vsub'` may sometimes fail.
More concisely: In a pseudometric space over a seminormed additive commutative group, the distance between two points is equal to the norm of their difference.
|
dist_eq_norm_vsub
theorem dist_eq_norm_vsub :
∀ (V : Type u_2) {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] (x y : P), dist x y = ‖x -ᵥ y‖
This theorem states that the distance between two points is equal to the norm of the vector obtained by subtracting the two points. Here, `V` represents a seminormed additive commutative group, `P` represents a pseudo metric space, and the relation between `V` and `P` is that `P` is a torsor (or a translated space) over `V`. In other words, it's saying that in a space where you can both measure distances (a pseudo metric space) and have a compatible way of "subtracting" points (a normed add torsor), the distance between two points `x` and `y` is the same as the "length" (`norm`) of the "difference" (`vsub`) between `x` and `y`. This theorem requires `V` to be explicitly given as an argument to ensure correct functioning of the rewrite rule based on this theorem.
More concisely: In a seminormed additive commutative group `V` making up a torsor over a pseudo metric space `P`, the distance between two points `x` and `y` equals the norm of their difference `x - y`.
|