AffineEquiv.pointReflection_self
theorem AffineEquiv.pointReflection_self :
∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
[inst_3 : AddTorsor V₁ P₁] (x : P₁), (AffineEquiv.pointReflection k x) x = x
This theorem states that for any point `x` in an affine space `P₁`, which is over a ring `k` and has difference group `V₁`, the point reflection of `x` with respect to itself is `x`. In other words, if you reflect a point with respect to itself, you get the same point back. This is a property of point reflection in an affine space.
More concisely: In an affine space over a ring, the point reflection of a point with respect to itself is equal to the original point.
|
AffineEquiv.image_symm
theorem AffineEquiv.image_symm :
∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
[inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂), ⇑f.symm '' s = ⇑f ⁻¹' s
This theorem states that for any given ring `k`, additive commutative groups `V₁` and `V₂`, and affine spaces `P₁` and `P₂` over `V₁` and `V₂` respectively, and an affine equivalence `f` from `P₁` to `P₂`, the image of a set `s` in `P₂` under the inverse of `f` is the same as the preimage of `s` under `f`. In simpler terms, applying `f` inverse and then `f` to a set `s` will just give you back the set `s`.
More concisely: For any affine equivalence `f` between affine spaces `P₁` and `P₂` over additive commutative groups `V₁` and `V₂`, and any set `s` in `P₂`, we have `f⁻¹(s) = {x : P₁ | f(x) ∈ s}`.
|
AffineEquiv.pointReflection_apply
theorem AffineEquiv.pointReflection_apply :
∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
[inst_3 : AddTorsor V₁ P₁] (x y : P₁), (AffineEquiv.pointReflection k x) y = x -ᵥ y +ᵥ x
The theorem `AffineEquiv.pointReflection_apply` states that for any type `k` having a ring structure, types `P₁` and `V₁` where `V₁` is an additive commutative group and a module over `k`, and `P₁` is an additive torsor over `V₁`, for any points `x` and `y` in `P₁`, applying the point reflection affine equivalence at `x` to `y` gives `x -ᵥ y +ᵥ x`. In other words, the point reflection of a point `y` in a point `x` is obtained by subtracting the vector from `y` to `x` from `x`, and then adding the result to `x`.
More concisely: For any additive torsor `P₁` over an additive commutative group `V₁` (which is a module over a ring `k`), and any points `x` and `y` in `P₁`, the point reflection of `y` in `x` is given by `x - y + x`.
|
AffineEquiv.symm_apply_apply
theorem AffineEquiv.symm_apply_apply :
∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
[inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁), e.symm (e p) = p
This theorem states that for any affine transformation `e` from one point space `P₁` to another `P₂` over a ring `k`, with associated vector spaces `V₁` and `V₂`, the application of the inverse of `e` ('symm e') to the result of applying `e` to any point `p` in `P₁` will yield `p` itself. Essentially, this confirms that the inverse of the affine transformation undoes the effect of the transformation, returning us to the original point.
More concisely: For any affine transformation `e` from point space `P₁` to `P₂` over ring `k` with associated vector spaces `V₁` and `V₂`, `symm e (e (p)) = p` for all points `p` in `P₁`.
|
AffineEquiv.pointReflection_fixed_iff_of_injective_bit0
theorem AffineEquiv.pointReflection_fixed_iff_of_injective_bit0 :
∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
[inst_3 : AddTorsor V₁ P₁] {x y : P₁},
Function.Injective bit0 → ((AffineEquiv.pointReflection k x) y = y ↔ y = x)
This theorem states that for any point 'y' in a torsor 'P₁' over a vector space 'V₁' of a ring 'k', 'y' is a fixed point of the point reflection in 'x' if and only if 'y' equals 'x'. This holds under the condition that the operation 'bit0', which doubles elements, is injective, i.e., it always maps distinct elements to distinct elements. In simpler terms, the only point that doesn't move when we reflect the whole space across 'x' is 'x' itself, provided that doubling a point's position always gives us a unique result.
More concisely: For any torsor P₁ over a ring k with injective point reflection operation 'bit0' around a point x, point reflection fixes exactly the point x.
|
AffineEquiv.ext
theorem AffineEquiv.ext :
∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
[inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂}, (∀ (x : P₁), e x = e' x) → e = e'
The theorem `AffineEquiv.ext` states that given any ring `k`, types `P₁`, `P₂`, `V₁`, `V₂` representing points and vectors in affine spaces, and instances asserting that `V₁` and `V₂` are additive commutative groups and `k`-modules, and that they act on `P₁` and `P₂` via an operation that satisfies the properties of an additive torsor, then for any two affine equivalences `e` and `e'` from `P₁` to `P₂`, if for every point in `P₁`, `e` and `e'` map it to the same point in `P₂`, then `e` is equal to `e'`. Basically, it's saying that two affine transformations are equal if they map every point to the same point in the target space.
More concisely: Given affine spaces `P₁` and `P₂` over a ring `k`, if `V₁` and `V₂` are additive commutative groups and `k`-modules acting on `P₁` and `P₂`, and if `e` and `e'` are affine equivalences from `P₁` to `P₂` such that `e(x) = e'(x)` for all `x` in `P₁`, then `e = e'`.
|
AffineEquiv.apply_lineMap
theorem AffineEquiv.apply_lineMap :
∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
[inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k),
e ((AffineMap.lineMap a b) c) = (AffineMap.lineMap (e a) (e b)) c
The theorem `AffineEquiv.apply_lineMap` states that for any ring `k`, any types `P₁`, `P₂`, `V₁`, and `V₂`, given certain algebraic structures (an additive commutative group and a module over the ring for each of `V₁` and `V₂`, and an affine space structure for each of `P₁` and `P₂`), and given an affine equivalence `e` from `P₁` to `P₂`, for any points `a` and `b` in `P₁` and any element `c` in `k`, applying the affine equivalence `e` to the point on the line from `a` to `b` determined by `c` (as computed by the function `AffineMap.lineMap`) is the same as first applying `e` to `a` and `b` to get points in `P₂`, and then using `AffineMap.lineMap` to find the corresponding point on the line from `e a` to `e b` determined by `c`. In other words, affine equivalences commute with the operation of finding a point on a line connecting two given points.
More concisely: Given affine spaces `P₁` and `P₂` over a ring `k`, an affine equivalence `e : P₁ ≃ P₂`, and points `a, b : P₁` and `c : k`, the application of `e` to the points on the line between `a` and `b` determined by `c` is equal to the point on the line between `e a` and `e b` determined by `c`.
|
AffineEquiv.surjective
theorem AffineEquiv.surjective :
∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
[inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), Function.Surjective ⇑e
The theorem `AffineEquiv.surjective` states that for any ring `k`, any types `P₁` and `P₂` representing affine spaces, and types `V₁` and `V₂` representing vector spaces, along with the necessary structures on them (such as `P₁` being an affine torsor over `V₁`, and `P₂` being an affine torsor over `V₂`, with both `V₁` and `V₂` being `k`-modules), every affine equivalence `e` from `P₁` to `P₂` is a surjective function. In other words, for every point in `P₂`, there exists a point in `P₁` such that applying the affine equivalence `e` to this point results in the desired point in `P₂`.
More concisely: Given affine spaces `P₁` and `P₂` over a ring `k`, represented as affine torsors over vector spaces `V₁` and `V₂` respectively, every affine equivalence `e` from `P₁` to `P₂` is a surjective function.
|
AffineEquiv.injective
theorem AffineEquiv.injective :
∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
[inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), Function.Injective ⇑e
The theorem `AffineEquiv.injective` states that for any ring `k`, types `P₁`, `P₂`, `V₁`, and `V₂`, given that `V₁` is an additive commutative group, `V₁` is a module over `k`, `P₁` is an additive torsor over `V₁`, `V₂` is an additive commutative group, `V₂` is a module over `k`, and `P₂` is an additive torsor over `V₂`, and given an affine equivalence `e` from `P₁` to `P₂`, the function `e` is injective. In other words, for any two elements `x` and `y` in `P₁`, if `e(x)` is equal to `e(y)`, then `x` is equal to `y`.
More concisely: Given rings `k`, additive commutative groups `V₁` and `V₂`, modules over `k` `P₁` and `P₂`, additive torsors over `V₁` and `V₂` `P₁` and `P₂`, and an affine equivalence `e` from `P₁` to `P₂`, `e` is injective.
|