AffineIsometry.map_vsub
theorem AffineIsometry.map_vsub :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] (f : P โแตโฑ[๐] Pโ) (p1 p2 : P),
f.linearIsometry (p1 -แตฅ p2) = f p1 -แตฅ f p2
This theorem states that for any normed field `๐`, seminormed add commutative groups `V` and `Vโ`, normed spaces over `๐` for `V` and `Vโ`, pseudometric spaces `P` and `Pโ`, and normed add torsors for `P` with `V` and `Pโ` with `Vโ`, if you have an affine isometry `f` from `P` to `Pโ` and two points `p1` and `p2` from `P`, then applying the linear isometry of `f` to the vector from `p2` to `p1` (denoted `p1 -แตฅ p2`) is equivalent to taking the vector from `f p2` to `f p1` (denoted `f p1 -แตฅ f p2`). In simpler terms, an affine isometry preserves the vectors between points under its linear part.
More concisely: Given an affine isometry between two normed pseudometric spaces and two points in the first space, the vectors between the points are equivalent under the affine isometry's linear part.
|
AffineIsometry.isometry
theorem AffineIsometry.isometry :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] (f : P โแตโฑ[๐] Pโ), Isometry โf
The theorem `AffineIsometry.isometry` states that for any normed field `๐`, seminormed add-commutative group `V` and `Vโ`, normed spaces over `๐` for `V` and `Vโ`, pseudometric spaces `P` and `Pโ`, where `V` and `Vโ` are normed add-torsors for `P` and `Pโ` respectively, the function `f` which is an affine isometry from `P` to `Pโ` over `๐`, is an isometry. In other words, it preserves the edistance, meaning that the edistance between the images of any two points under `f` is equal to the edistance between the points themselves in the original space.
More concisely: If `f` is an affine isometry from a normed add-torsor `(V, P)` to a normed add-torsor `(Vโ, Pโ)` over a normed field `๐`, then `f` preserves the Euclidean distance, i.e., `d(x, y) = d(f(x), f(y))` for all `x, y` in `V`.
|
AffineIsometryEquiv.continuous
theorem AffineIsometryEquiv.continuous :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] (e : P โแตโฑ[๐] Pโ), Continuous โe
This theorem states that for any affine isometry equivalence `e` between two points `P` and `Pโ` in different types (or spaces), the function represented by `e` is continuous. The spaces `P` and `Pโ` are associated with the seminormed additive commutative groups `V` and `Vโ`, respectively, both of which are normed over a normed field `๐`. Additionally, both `P` and `Pโ` are pseudometric spaces, and `V` and `Vโ` are normed add-torsors over `P` and `Pโ`, respectively. The theorem holds for any such setup.
More concisely: For any affine isometry equivalence between points in normed additive commutative groups over a normed field, the represented function is continuous.
|
AffineMap.continuous_linear_iff
theorem AffineMap.continuous_linear_iff :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] {f : P โแต[๐] Pโ},
Continuous โf.linear โ Continuous โf
This theorem states that for any affine map `f` from a point in a pseudo metric space `P` to a point in another pseudo metric space `Pโ`, the continuity of the linear part of `f` is equivalent to the continuity of `f` itself. Here, both `P` and `Pโ` are normed add torsors over seminormed add commutative groups `V` and `Vโ` respectively, and these groups are normed spaces over a normed field `๐`.
More concisely: For any affine map between two normed add torsors over seminormed add commutative groups, the continuity of its linear part is equivalent to the continuity of the entire map.
|
AffineMap.isOpenMap_linear_iff
theorem AffineMap.isOpenMap_linear_iff :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] {f : P โแต[๐] Pโ},
IsOpenMap โf.linear โ IsOpenMap โf
The theorem `AffineMap.isOpenMap_linear_iff` states that for any affine map `f` from a pseudo-metric space `P` to another pseudo-metric space `Pโ`, the linearity part of `f` is an open map if and only if `f` itself is an open map. An open map is a function where the image of any open set of `P` remains open in `Pโ`. Here the normed field `๐` and normed vector spaces `V` and `Vโ` are part of the structures of the pseudo-metric spaces `P` and `Pโ`, and affine maps from `P` to `Pโ`.
More concisely: An affine map from a pseudo-metric space to another is open if and only if its linear part is an open map.
|
AffineIsometryEquiv.injective
theorem AffineIsometryEquiv.injective :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] (e : P โแตโฑ[๐] Pโ), Function.Injective โe
The theorem `AffineIsometryEquiv.injective` states that for any normed field `๐`, seminormed add commutative group `V` and `Vโ`, normed space over `๐` for `V` and `Vโ`, pseudometric spaces `P` and `Pโ`, and normed add torsors `P` over `V` and `Pโ` over `Vโ`, any affine isometry equivalence `e` between `P` and `Pโ` (denoted as `P โแตโฑ[๐] Pโ`), the function `e` is injective. In other words, if two points in `P` are mapped to the same point in `Pโ` by `e`, then those two points must be the same. This is a property of affine isometry equivalences in the context of normed field and normed spaces.
More concisely: Given any affine isometry equivalence between two normed add torsors over normed spaces and seminormed add commutative groups in a normed field, the equivalence function is injective.
|
AffineIsometry.dist_map
theorem AffineIsometry.dist_map :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] (f : P โแตโฑ[๐] Pโ) (x y : P),
dist (f x) (f y) = dist x y
This theorem states that for an affine isometry `f`, taken from the space `P` to the space `Pโ` in a normed field `๐`, and for any two points `x` and `y` in `P`, the distance between the image points `f(x)` and `f(y)` in `Pโ` is the same as the distance between `x` and `y` in `P`. This property characterizes an important aspect of affine isometries: they preserve distances.
More concisely: For any affine isometry f from a normed field P to Pโ, and for all x, y in P, the distance between f(x) and f(y) in Pโ equals the distance between x and y in P.
|
AffineIsometryEquiv.ext
theorem AffineIsometryEquiv.ext :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] {e e' : P โแตโฑ[๐] Pโ},
(โ (x : P), e x = e' x) โ e = e'
The theorem `AffineIsometryEquiv.ext` states that for any field ๐, vector spaces V and Vโ, affine spaces P and Pโ, if e and e' are affine isometry equivalences (isomorphisms that preserve the affine structure and the distance) between P and Pโ, then e is equal to e' if they are equal for every point x in P. Essentially, it ensures that two affine isometry equivalences are the same if they map each point in the original space to the same point in the target space.
More concisely: For any fields ๐, vector spaces V and Vโ, and affine spaces P and Pโ, if two affine isometry equivalences between P and Pโ agree on every point, then they are equal.
|
AffineIsometryEquiv.vadd_vsub
theorem AffineIsometryEquiv.vadd_vsub :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst : NormedSpace ๐ Vโ]
[inst : PseudoMetricSpace Pโ] [inst_6 : NormedAddTorsor Vโ Pโ] {f : P โ Pโ},
Isometry f โ โ {p : P} {g : V โ Vโ}, (โ (v : V), g v = f (v +แตฅ p) -แตฅ f p) โ Isometry g
The theorem `AffineIsometryEquiv.vadd_vsub` states that, given a map `f` from a pseudometric space `P` to another pseudometric space `Pโ`, and a base point `p` in `P`, if `f` is an isometry (i.e., it preserves the distance or `edistance` between any two points), then another map `g` from a normed space `V` to another normed space `Vโ`, defined by `g v = f (v +แตฅ p) -แตฅ f p`, is also an isometry. Here, `+แตฅ` and `-แตฅ` denote addition and subtraction of a vector from a point, respectively. This theorem essentially asserts that the isometric property of a map is preserved under affine transformations.
More concisely: If `f: P -> Pโ` is an isometry between pseudometric spaces and `p` is a point in `P`, then the map `g: V -> Vโ` defined by `g v = f (v + p) - f p` is also an isometry between normed spaces.
|
AffineIsometryEquiv.isometry
theorem AffineIsometryEquiv.isometry :
โ {๐ : Type u_1} {V : Type u_2} {Vโ : Type u_5} {P : Type u_10} {Pโ : Type u_11} [inst : NormedField ๐]
[inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace ๐ V] [inst_3 : PseudoMetricSpace P]
[inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup Vโ] [inst_6 : NormedSpace ๐ Vโ]
[inst_7 : PseudoMetricSpace Pโ] [inst_8 : NormedAddTorsor Vโ Pโ] (e : P โแตโฑ[๐] Pโ), Isometry โe
This theorem states that for any Affine Isometry Equivalence `e` between two points `P` and `Pโ` in two pseudometric spaces (spaces where the "distance" between any two points is non-negative and satisfies certain properties), the function defined by `e` is an Isometry. In other words, this function preserves the "distance" (as measured by the edistance) between any two points that it maps from the first space to the second. This holds for any fields `๐`, any normed spaces `V` and `Vโ`, and any normed add torsors `P` and `Pโ`, where the normed spaces and the normed add torsors have some additional properties given by the type classes `SeminormedAddCommGroup`, `NormedSpace`, and `NormedAddTorsor`.
More concisely: Given any Affine Isometry Equivalence between two points in two pseudometric spaces with normed add torsors over the same field, the equivalence function is an isometry preserving the "edistance" between any two points.
|