AffineSubspace.direction_affineSpan_insert
theorem AffineSubspace.direction_affineSpan_insert :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p1 p2 : P},
p1 ∈ s → (affineSpan k (insert p2 ↑s)).direction = Submodule.span k {p2 -ᵥ p1} ⊔ s.direction
The theorem `AffineSubspace.direction_affineSpan_insert` states that for any ring `k`, abelian group `V`, and affine space `P` over `V`, any affine subspace `s` of `P`, and any two points `p1` and `p2` such that `p1` is in `s`, the direction of the affine span of the set obtained by inserting `p2` into the carrier set of `s` is the least upper bound (supremum) of the direction of `s` and the submodule spanned by the singleton set containing the difference vector `p2 -ᵥ p1`.
More concisely: The direction of an affine subspace of an abelian group over a ring is the supremum of its direction and the submodule generated by the difference between any point in the subspace and a fixed point.
|
vectorSpan_range_eq_span_range_vsub_left_ne
theorem vectorSpan_range_eq_span_range_vsub_left_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i₀ : ι),
vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i₀ -ᵥ p ↑i)
The theorem `vectorSpan_range_eq_span_range_vsub_left_ne` states that for any type `k` and a ring structure on `k`, for any types `V` and `P` with `V` being an additive commutative group and a module over `k`, and `P` being an additive torsor over `V`, for any type `ι` and a function `p` from `ι` to `P`, and for any element `i₀` of `ι`, the vector span (defined as the smallest submodule containing all differences of pairs of points) of the range of the function `p` is equal to the span (defined as the smallest submodule containing a set) of the range of the function that subtracts from `p i₀` the image under `p` of every other element in `ι`. The subtraction of `p i₀` from itself is excluded.
More concisely: For any additive commutative group `V` over a ring `k`, module `P` over `V`, additive torsor `P` over `V`, function `p` from an index set `ι` to `P`, and element `i₀` in `ι`, the vector span of `p` equals the span of `p(i) - p(i₀)` for all `i` in `ι`, excluding `i = i₀`.
|
left_mem_affineSpan_pair
theorem left_mem_affineSpan_pair :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p₁ p₂ : P), p₁ ∈ affineSpan k {p₁, p₂}
This theorem states that for any given ring `k` and a set of two points `p₁` and `p₂` in an affine space `P` (where `P` is an additive torsor over a vector space `V`, which in turn is a module over the ring `k`), the first point `p₁` always lies in the affine span of these two points. The affine span of a set of points is the smallest affine subspace that contains those points.
More concisely: For any ring `k`, affine space `P` over a vector space `V` as an additive torsor over `k`, and two points `p₁` and `p₂` in `P`, `p₁` lies in the affine span of `p₁` and `p₂`.
|
Set.Nonempty.affineSpan
theorem Set.Nonempty.affineSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P}, s.Nonempty → (↑(affineSpan k s)).Nonempty
The theorem `Set.Nonempty.affineSpan` states that for any set `s` of points in an affine space `P` over a ring `k`, with associated vector space `V` that forms an additive commutative group and is a module over the ring `k`, if the set `s` is non-empty, then the affine span of `s` (which is the smallest affine subspace that contains all points in `s`) is also non-empty. This theorem is essentially an alias for the reverse direction of the theorem `affineSpan_nonempty` -- it confirms that the presence of at least one element in a set ensures the non-emptiness of its affine span.
More concisely: If `s` is a non-empty set of points in an affine space over a ring, then the affine span of `s` is non-empty.
|
AffineSubspace.span_univ
theorem AffineSubspace.span_univ :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P], affineSpan k Set.univ = ⊤
The theorem `AffineSubspace.span_univ` states that for any defined types `k`, `V`, `P` where `k` is a ring, `V` is an additive commutative group, `V` is a module over `k`, and `P` is an additive torsor over `V`, the affine span of the universal set `Set.univ` is the top element `⊤`. In layman's terms, it means that the smallest affine subspace that contains all elements of the given types is the entire space itself.
More concisely: The theorem asserts that the affine span of the universal set in an additive commutative group `V` made an `k`-module and an additive torsor, for a ring `k`, is equal to the top element in the lattice of affine subspaces.
|
AffineSubspace.not_mem_bot
theorem AffineSubspace.not_mem_bot :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (p : P), p ∉ ⊥
This theorem states that no points are in the bottom element (`⊥`) of the affine subspace. Specifically, given any types `k`, `V`, and `P`, where `k` is a ring, `V` is an additive commutative group, and `V` is a `k`-module, if you have an additive torsor `S` over `V` acting on `P`, then for any point `p` of type `P`, `p` is not an element of `⊥`.
More concisely: Given a ring `k`, an additive commutative group `V` that is a `k`-module, and an additive torsor `S` over `V` acting on a type `P`, there are no points `p` in `P` that belong to the bottom element `⊥` of the affine subspace.
|
mem_vectorSpan_pair
theorem mem_vectorSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ : P} {v : V}, v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
This theorem states that for any field `k`, an additive commutative group `V`, a module `V` over the field `k`, an additive torsor `P`, two points `p₁` and `p₂` from `P`, and a vector `v` from `V`, the vector `v` lies in the `vectorSpan` of the two points `p₁` and `p₂` if and only if there exists a scalar `r` from the field `k` such that `r` times the difference between `p₁` and `p₂` equals `v`. In mathematical terms, a vector is in the span of two points if and only if it is a scalar multiple of the vector determined by the two points.
More concisely: A vector lies in the span of two points in a module over a field if and only if it is a scalar multiple of the difference between the points.
|
vectorSpan_range_eq_span_range_vsub_right
theorem vectorSpan_range_eq_span_range_vsub_right :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i0 : ι),
vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i -ᵥ p i0)
The theorem `vectorSpan_range_eq_span_range_vsub_right` states that, for a given indexed family of points `p` in an additive torsor `P` over a vector space `V` with scalars in a ring `k`, the `vectorSpan` of the set of all points in this family is equal to the submodule spanned by the set of all vector differences obtained by subtracting a fixed point `p i0` from each point `p i` in the family. In other words, the space generated by all the points in the family is precisely the space generated by the differences between each point and a specific reference point in the family.
More concisely: The `vectorSpan` of an indexed family of points in an additive torsor over a vector space is equal to the submodule spanned by the vector differences between each point and a fixed point in the family.
|
AffineSubspace.mk'_eq
theorem AffineSubspace.mk'_eq :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → AffineSubspace.mk' p s.direction = s
The theorem `AffineSubspace.mk'_eq` states that for any given ring `k`, additive commutative group `V`, module `V` over `k`, and an affine torsor `P` over `V`, if we have an affine subspace `s` of `P` and a point `p` from `s`, then constructing an affine subspace from the point `p` and the direction of subspace `s` will yield the original subspace `s`. In essence, the affine subspace constructed from any point in the subspace and the direction of the subspace itself will always be the same as the original subspace.
More concisely: Given a ring `k`, an additive commutative group `V` with `k`-module structure, an affine torsor `P` over `V`, an affine subspace `s` of `P`, and a point `p` in `s`, the subspace spanned by `p` and the direction vector of `s` equals `s`.
|
AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty
theorem AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s : Set P}, s.Nonempty → (affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤)
The theorem `AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty` states that for any non-empty set `s` of points from a type `P`, the affine span of `s` is equivalent to the whole space (denoted by the top element `⊤`) if and only if the vector span of `s` is also equivalent to the whole space. This is established under the conditions that `k` is a ring, `V` is an additive commutative group, `V` is a module over `k`, and `P` is an affine torsor over `V`.
More concisely: For a non-empty set `s` of points in an affine torsor `P` over a commutative ring `k`, the affine span and vector span of `s` are equal to the whole space if and only if `k` is a field. (Note: This is an approximation, as the theorem does not explicitly state that `k` being a field is a sufficient condition for `⊤` being the affine span or vector span of `s`, but it is a common assumption in the context of affine geometry over fields.)
|
vectorSpan_def
theorem vectorSpan_def :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : Set P), vectorSpan k s = Submodule.span k (s -ᵥ s)
The theorem `vectorSpan_def` describes the equivalency between the definition of `vectorSpan` and `Submodule.span` for a given set of points. Specifically, for any field `k` and set `s`, the `vectorSpan` of `s` in `k` is exactly the same as the span of the differences of `s` in `k`. Here, the `vectorSpan` is defined as the submodule spanning the differences of a set of points, while `Submodule.span` is defined as the smallest submodule that contains the set. The differences of a set `s` is represented as `s -ᵥ s` in Lean 4.
More concisely: For any field `k` and set `s` in `k`, the submodule generated by the differences of `s` is equal to the span of `s` in `k`. In Lean 4 notation, `vectorSpan s = Submodule.span (s -ᵥ s)`.
|
AffineSubspace.inf_coe
theorem AffineSubspace.inf_coe :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), ↑s1 ⊓ ↑s2 = ↑s1 ∩ ↑s2
This theorem states that for any two affine subspaces (s1 and s2) in a vector space over a ring, the infimum (greatest lower bound) of these two subspaces, when treated as sets, is equal to the intersection of the two sets. The underlying vector space is defined over a ring and forms an additive commutative group. Furthermore, this space is a module over the ring, and an AddTorsor structure is defined over the vector space and another type.
More concisely: For any two affine subspaces s1 and s2 of a commutative additive group and module over a ring, their infimum as sets equals their intersection.
|
AffineSubspace.bot_coe
theorem AffineSubspace.bot_coe :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P], ↑⊥ = ∅
This theorem states that the bottom element (`⊥`), when coerced to a set, is the empty set (`∅`). The statement holds for any types `k`, `V`, and `P`; with `k` being a ring, `V` an additive commutative group, and `V` a `k`-module; and considering `S` as an additive torsor structure over `V` and `P`. The `⊥` here is used in the context of affine subspaces.
More concisely: The bottom element `⊥` of an affine subspace over a ring `k`, an additive commutative group `V`, and a `k`-module `P`, coerced to a set, equals the empty set `∅`.
|
AffineSubspace.sup_direction_le
theorem AffineSubspace.sup_direction_le :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), s1.direction ⊔ s2.direction ≤ (s1 ⊔ s2).direction
This theorem states that for any two affine subspaces `s1` and `s2` in a module over a ring (the module being an additive torsor of an additive commutative group), the sup (supremum, in the lattice-theoretic sense) of the directions of `s1` and `s2` is less than or equal to the direction of the sup of `s1` and `s2`. In other words, the combined direction of the two subspaces is always within the direction of the combined subspace.
More concisely: For any two affine subspaces in an additive torsor of an additive commutative group over a ring, the direction of their supremum is less than or equal to the direction of the sup of each subspace.
|
AffineSubspace.mem_coe
theorem AffineSubspace.mem_coe :
∀ (k : Type u_1) {V : Type u_2} (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P) (s : AffineSubspace k P), p ∈ ↑s ↔ p ∈ s
This theorem states that for any type `k` with ring structure, a type `V` with additive commutative group structure, a module structure of `V` over `k`, and `V` acting on a type `P` via an additive torsor structure, a point `p` of type `P` is contained in the set representation of an affine subspace `s` of `P` if and only if it is in the affine subspace `s` itself. In mathematical terms, this theorem asserts the equivalence between set membership and subspace membership for affine spaces.
More concisely: For any affine space (V, +, mul over a ring k), module action of V on type P, additive torsor structure on P, and subset s of P representing an affine subspace, the point p in P belongs to s if and only if it is in the subspace s itself.
|
AffineSubspace.vadd_mem_iff_mem_of_mem_direction
theorem AffineSubspace.vadd_mem_iff_mem_of_mem_direction :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {v : V}, v ∈ s.direction → ∀ {p : P}, v +ᵥ p ∈ s ↔ p ∈ s
This theorem states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, given an affine subspace `s` of `P` and a vector `v` in the direction of `s`, for any point `p`, the operation of adding the vector `v` to the point `p` results in a point in the subspace `s` if and only if the original point `p` is in the subspace `s`. This theorem essentially provides a condition for when a point, after being moved along a certain vector, still remains in the same affine subspace.
More concisely: For any additive torsor `P` over an additive commutative group `V` in a ring `k`, a point `p` in the affine subspace `s` of `P` and a vector `v` in the direction of `s`, if and only if `p` is in `s`, then `p + v` is in `s`.
|
vectorSpan_mono
theorem vectorSpan_mono :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s₁ s₂ : Set P}, s₁ ⊆ s₂ → vectorSpan k s₁ ≤ vectorSpan k s₂
The theorem `vectorSpan_mono` asserts the monotonicity of the `vectorSpan` function. In particular, it states that for any ring `k`, additive commutative group `V`, and additive torsor `P`, and any two sets `s₁` and `s₂` of elements of `P` such that `s₁` is a subset of `s₂`, the vector span of `s₁` is a submodule of, or equal to, the vector span of `s₂`. This means that expanding the set of points from which we form differences to compute the vector span only results in a larger (or equal) spanned submodule.
More concisely: For any additive torsor P over a commutative ring k, if s1 is a subset of s2 in P, then the vector span of s1 is contained in the vector span of s2.
|
AffineSubspace.direction_mk'
theorem AffineSubspace.direction_mk' :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P) (direction : Submodule k V),
(AffineSubspace.mk' p direction).direction = direction
The theorem `AffineSubspace.direction_mk'` states that for any ring `k`, additive commutative group `V`, and affine torsor `P`, given any point `p` of type `P` and any direction which is a submodule of type `V`, the direction of the affine subspace that is constructed using this point and direction, is equal to the original direction. In other words, if you construct an affine subspace from a point and a direction, the direction of the resulting affine subspace is the same as the direction that was used to construct it.
More concisely: For any ring `k`, additive commutative group `V`, affine torsor `P`, point `p` in `P`, and submodule `d` of `V`, the direction of the affine subspace `AffineSubspace.mk p d` is equal to `d`.
|
AffineSubspace.directionOfNonempty_eq_direction
theorem AffineSubspace.directionOfNonempty_eq_direction :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} (h : (↑s).Nonempty),
AffineSubspace.directionOfNonempty h = s.direction
The theorem `AffineSubspace.directionOfNonempty_eq_direction` states that for any given ring `k`, additive commutative group `V`, module `V` over `k`, and a non-empty affine subspace `s` of `P` (where `P` is an affine space over `V`), the direction of the non-empty affine subspace `s` (obtained using the function `directionOfNonempty`) is the same as the direction of the affine subspace `s` (obtained using the `.direction` attribute).
More concisely: For any non-empty affine subspace `s` of an affine space `P` over a ring `k` and additive commutative group `V`, the direction of `s` (as obtained from `directionOfNonempty s`) equals the direction of `s` (as obtained from the `.direction` attribute).
|
affineSpan_pair_le_of_right_mem
theorem affineSpan_pair_le_of_right_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P},
p₁ ∈ affineSpan k {p₂, p₃} → affineSpan k {p₂, p₁} ≤ affineSpan k {p₂, p₃}
This theorem states that given any ring `k`, an additive commutative group `V`, and an affine torsor `P` over `V`, along with any three points `p₁`, `p₂`, and `p₃` in `P`, if `p₁` is in the affine span of the set `{p₂, p₃}`, then the affine span of the set `{p₂, p₁}` is a subset of or equal to the affine span of the set `{p₂, p₃}`. In other words, one line (defined by points `p₂` and `p₁`) is contained within another line (defined by points `p₂` and `p₃`) if the second point (`p₁`) of the first line is contained within the second line (the line defined by `p₂` and `p₃`).
More concisely: Given a ring `k`, an additive commutative group `V`, an affine torsor `P` over `V`, and points `p₁`, `p₂`, `p₃` in `P` such that `p₁` is in the affine span of `{p₂, p₃}`, then the affine span of `{p₂, p₁}` is contained in the affine span of `{p₂, p₃}`.
|
AffineSubspace.direction_bot
theorem AffineSubspace.direction_bot :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P], ⊥.direction = ⊥
This theorem states that the direction of the bottom (`⊥`) affine subspace is the bottom (`⊥`) submodule. This applies for any type `k` with a Ring structure, any type `V` with an Additive Commutative Group structure and is a module over `k`, and any type `P` that forms an Additive Torsor with `V`. In other words, in any vector space, the direction of the empty subspace is the zero vector.
More concisely: In any vector space over a ring, the direction of the zero subspace is the zero vector.
|
AffineSubspace.le_def
theorem AffineSubspace.le_def :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), s1 ≤ s2 ↔ ↑s1 ⊆ ↑s2
The theorem `AffineSubspace.le_def` states that for any ring `k`, additive commutative group `V`, module `k V`, and additive torsor `S` over `V` and `P`, the `≤` (less than or equal to) order relation on two affine subspaces `s1` and `s2` is equivalent to the subset relation `⊆` (subset or equal to) between their corresponding sets. In other words, `s1` is less than or equal to `s2` if and only if the set of elements in `s1` is a subset of the set of elements in `s2`.
More concisely: For any ring `k`, additive commutative group `V`, module `k V`, additive torsor `S` over `V` and `P`, the affine subspaces `s1` and `s2` of `S` have the relation `s1 ≤ s2` if and only if `s1` is a subset of `s2`.
|
AffineSubspace.map_span
theorem AffineSubspace.map_span :
∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [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₁),
AffineSubspace.map f (affineSpan k s) = affineSpan k (⇑f '' s)
The theorem `AffineSubspace.map_span` states that for any ring `k`, additive commutative groups `V₁` and `V₂`, torsors `P₁` and `P₂` under these groups respectively, and an affine map `f` from `P₁` to `P₂`, the affine image of the affine span of a set `s` in `P₁` under the map `f` is the same as the affine span of the image of `s` under `f`. In other words, mapping the smallest affine subspace containing `s` (the affine span of `s`) under `f` results in the smallest affine subspace containing the image of `s`.
More concisely: For any ring `k`, additive commutative groups `V₁` and `V₂`, torsors `P₁` and `P₂` under `V₁` and `V₂` respectively, and an affine map `f : P₁ → P₂`, the affine image of the affine span of a set `s` in `P₁` under `f` equals the affine span of the image of `s` in `P₂`.
|
AffineSubspace.vsub_right_mem_direction_iff_mem
theorem AffineSubspace.vsub_right_mem_direction_iff_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ∀ (p2 : P), p2 -ᵥ p ∈ s.direction ↔ p2 ∈ s
This theorem states that for any given point in an affine subspace of a vector space, the result of subtracting that point from another point is in the direction of the affine subspace if and only if the other point is also in the affine subspace. This holds for any field `k`, any additive commutative group `V`, and any module space `P`, as well as any point `p` in the affine subspace `s`. In other words, the relative position of two points in an affine subspace can only be expressed as a vector in the direction of that subspace if both points are actually part of the subspace.
More concisely: For any affine subspace of a vector space over a field, the difference of two points in the subspace is collinear with the second point if and only if both points belong to the subspace.
|
affineSpan_nonempty
theorem affineSpan_nonempty :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P}, (↑(affineSpan k s)).Nonempty ↔ s.Nonempty
This theorem states that for any given set `s` of points `P` in an affine space, the affine span of `s` is nonempty if and only if the set `s` itself is nonempty. This holds true for any type `k` with a ring structure, where `V` is an additive commutative group and also a `k`-module, and `P` is an `V`-additive torsor. In simpler terms, it means that the smallest affine subspace containing the points of a set is nonempty exactly when the set itself is nonempty.
More concisely: The affine span of a nonempty set of points in an affine space over a ring with additive commutative group and `k`-module structure is nonempty.
|
AffineSubspace.coe_direction_eq_vsub_set_right
theorem AffineSubspace.coe_direction_eq_vsub_set_right :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ↑s.direction = (fun x => x -ᵥ p) '' ↑s
This theorem states that for any given point `p` in an affine subspace `s`, the set of vectors in the direction of the subspace is equal to the set of vectors obtained by subtracting `p` from each point in the subspace `s`. Here, the direction of `s` is the submodule spanned by the pairwise differences of points in `s`. The subtraction operation `x -ᵥ p` denotes the vector obtained by subtracting the position vector of `p` from that of `x`. So, every vector in the direction of `s` can be represented as the difference between a point in `s` and `p`. Note that the types `k`, `V` and `P` denote a ring, a commutative additive group and an affine torsor respectively, and `s` is a subset of `P` with the structure of an affine space over `V` with scalars `k`.
More concisely: The direction vectors of an affine subspace are equal to the differences between any point in the subspace and a given point.
|
mem_spanPoints
theorem mem_spanPoints :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P) (s : Set P), p ∈ s → p ∈ spanPoints k s
The theorem `mem_spanPoints` states that for any point `p` in a set `s` of points, `p` is also in the affine span of the set `s`. Here, the affine span is defined within a certain mathematical context specified by a ring `k`, an additive commutative group `V`, a module `V` over the ring `k`, and an additive torsor `V` for the type `P`. The theorem essentially guarantees that any point in a set is also in the affine span of that set, which is a fundamental property in affine geometry.
More concisely: For any point `p` and set `s` of points in a vector space `V` over a ring `k`, `p` is in the affine span of `s`.
|
affineSpan_mono
theorem affineSpan_mono :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s₁ s₂ : Set P}, s₁ ⊆ s₂ → affineSpan k s₁ ≤ affineSpan k s₂
The theorem `affineSpan_mono` states that the operation `affineSpan` is monotone. In more concrete terms, if we have a ring `k` and `V` is an additive commutative group, `P` is a set such that `V` acts on `P` by translations (i.e., `V` and `P` form an affine space over `k`), then for any two sets of points `s₁` and `s₂` in `P`, if `s₁` is a subset of `s₂` then the affine span of `s₁` (the smallest affine subspace containing `s₁`) is a subspace of or equal to the affine span of `s₂` (the smallest affine subspace containing `s₂`).
More concisely: If `s₁` is a subset of `s₂` in an affine space `P` over a ring `k`, then the affine span of `s₁` is contained in the affine span of `s₂`.
|
AffineSubspace.mem_inf_iff
theorem AffineSubspace.mem_inf_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (p : P) (s1 s2 : AffineSubspace k P), p ∈ s1 ⊓ s2 ↔ p ∈ s1 ∧ p ∈ s2
This theorem states that for any given point `p` and two affine subspaces `s1` and `s2`, the point `p` is in the intersection of `s1` and `s2` if and only if `p` is in both `s1` and `s2`. Here, `k` is a ring, `V` is an additive commutative group, `P` is a module over `k`, and `S` is an additive torsor for `V` acting on `P`. The symbol `⊓` represents the intersection operation on these subspaces.
More concisely: For any point `p` in the vector space `P` over a commutative ring `k`, `p` is in the intersection of affine subspaces `s1` and `s2` if and only if `p` is in both `s1` and `s2` (denoted as `s1 ∩ s2 = {p : P | p ∈ s1 ∧ p ∈ s2}`).
|
vsub_mem_vectorSpan
theorem vsub_mem_vectorSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p1 p2 : P}, p1 ∈ s → p2 ∈ s → p1 -ᵥ p2 ∈ vectorSpan k s
This theorem states that for any pair of points `p1` and `p2` in a set `s` of points in an affine space (over a ring `k` with an associated vector space `V` and point module `P`), the vector difference of `p1` and `p2` belongs to the vector span of `s`. This vector span is a submodule in `V` generated by all pairwise differences of points in `s`. The theorem essentially says that any pairwise difference of points in a set is a combination of other pairwise differences in the same set.
More concisely: For any two points `p1` and `p2` in a set `s` of points in an affine space over a ring `k`, the vector difference `p1 - p2` lies in the submodule of `k-V` generated by all pairwise differences of points in `s`.
|
smul_vsub_mem_vectorSpan_pair
theorem smul_vsub_mem_vectorSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₁ -ᵥ p₂) ∈ vectorSpan k {p₁, p₂}
This theorem states that for any given field `k`, a vector space `V` over `k`, and an affine space `P` with difference group `V`, if you take any scalar `r` from `k` and any two points `p₁` and `p₂` from `P`, then the scalar multiple `r` times the difference between `p₁` and `p₂` is an element of the submodule spanned by the differences of the set containing `p₁` and `p₂`. This submodule is denoted by `vectorSpan k {p₁, p₂}`. In other words, any scaled difference between two points is in the vector span of those two points.
More concisely: For any field `k`, vector space `V` over `k`, affine space `P` with difference group `V`, and points `p₁, p₂ ∈ P`, the scalar multiple `r` times the difference `p₁ - p₂` is in the vector span `vectorSpan k {p₁, p₂}`.
|
vectorSpan_singleton
theorem vectorSpan_singleton :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P), vectorSpan k {p} = ⊥
This theorem states that the `vectorSpan` of a single point is the bottom element `⊥`. In more detail, for any ring `k`, any additive commutative group `V`, any module of `k` over `V`, any additive torsor of `V` over another type `P`, and any point `p` of type `P`, the `vectorSpan` of the set containing only the point `p` is `⊥`, which represents a zero-dimensional subspace in the context of modules or vector spaces.
More concisely: For any additive torsor P over a module or vector space V over a ring k, the `vectorSpan` of the set {p} for any point p in P is the zero subspace ⊥.
|
vectorSpan_range_eq_span_range_vsub_left
theorem vectorSpan_range_eq_span_range_vsub_left :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i0 : ι),
vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i0 -ᵥ p i)
This theorem states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and an additive torsor `P` over `V`, if we take an indexed family of points `p` from type `ι` to `P` and any element `i0` of type `ι`, then the vector span of the set of all the points in the family is equal to the span of the set of vectors formed by subtracting each point in the family from the point at index `i0`. In simpler terms, the space spanned by all the points in the family is the same as the space spanned by the vectors resulting from subtracting each point from a fixed point in the family.
More concisely: For any additive torsor `P` over an additive commutative group `V` and module `V` over a ring `k`, if `p` is an indexed family of points in `P`, then the span of `{p(i) | i ∈ ι}` equals the span of `{p(i) - p(i0) | i ∈ ι}`.
|
affineSpan_induction
theorem affineSpan_induction :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {x : P} {s : Set P} {p : P → Prop},
x ∈ affineSpan k s → (∀ x ∈ s, p x) → (∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)) → p x
This theorem, titled `affineSpan_induction`, is an induction principle for membership in the affine span of a set of points. The theorem states that if a property `p` holds for all elements in the given set `s` and the property remains `true` under certain affine combinations, then `p` holds for all elements in the affine span of `s`.
Specifically, given a ring `k`, an additive commutative group `V`, a `k`-module structure on `V`, an add-torsor structure on `P` with respect to `V`, a point `x` in `P`, a set of points `s` in `P`, and a property `p` that holds for points in `P`, if `x` belongs to the affine span of `s`, all points in `s` satisfy property `p`, and for any scalar `c` in `k` and points `u`, `v`, and `w` in `P` for which `p` holds, `p` also holds for the point obtained by the affine combination `c • (u -ᵥ v) +ᵥ w`, then `p` holds for `x`.
More concisely: If a property holds for all points in a set and their affine combinations, then it holds for any point in the affine span of that set.
|
smul_vsub_rev_mem_vectorSpan_pair
theorem smul_vsub_rev_mem_vectorSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₂ -ᵥ p₁) ∈ vectorSpan k {p₁, p₂}
The theorem `smul_vsub_rev_mem_vectorSpan_pair` states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, and for any scalar `r` in `k` and points `p₁` and `p₂` in `P`, the result of scaling the difference `p₂ -ᵥ p₁` by `r` (denoted as `r • (p₂ -ᵥ p₁)`) is an element of the submodule generated by the differences of the set containing `p₁` and `p₂`. This submodule is known as the `vectorSpan` of `{p₁, p₂}`.
In simpler terms, this theorem is saying that the scaled difference of any two points in a space lies within the vector span of those two points.
More concisely: For any ring `k`, additive commutative group `V`, module `V` over `k`, additive torsor `P` over `V`, scalar `r` in `k`, and points `p₁, p₂` in `P`, the scalar multiple `r • (p₂ - p₁)` belongs to the submodule generated by the differences `{p₂ - p₁}`.
|
AffineSubspace.ext_iff
theorem AffineSubspace.ext_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), ↑s₁ = ↑s₂ ↔ s₁ = s₂
This theorem states that for any two affine subspaces `s₁` and `s₂` of a given type `P`, under the conditions that `k` is a ring, `V` is an additive commutative group, and `V` is a `k`-module, and `P` is an AddTorsor over `V`, the equivalence of their coercion to sets implies their equality. In other words, if two affine subspaces are equivalent when considered as sets, then they are equal as affine subspaces.
More concisely: If `s₁` and `s₂` are affine subspaces of a `k`-module `V` over a ring `k`, and their coercions to sets are equal, then `s₁ = s₂`.
|
AffineSubspace.vadd_mem_iff_mem_direction
theorem AffineSubspace.vadd_mem_iff_mem_direction :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} (v : V) {p : P}, p ∈ s → (v +ᵥ p ∈ s ↔ v ∈ s.direction)
The theorem `AffineSubspace.vadd_mem_iff_mem_direction` states that for any ring `k`, additive commutative group `V`, module over `k` with `V`, and add torsor `V` for `P`, and given an affine subspace `s` of `P`, a vector `v` in `V`, and a point `p` in `P` that belongs to the subspace `s`, adding the vector `v` to the point `p` results in a point that is in the subspace `s` if and only if the vector `v` is in the direction of the subspace `s`.
In simpler terms, this theorem says that in an affine subspace, you can add a vector to a point to get another point in the subspace, but only if the vector is along the direction of the subspace. The 'direction' of a subspace is defined as the set of all possible vectors that can be achieved by subtracting any two points within the subspace.
More concisely: For an affine subspace of a module over a ring and a point in the subspace, a vector belongs to the subspace if and only if it is in the direction of the subspace, i.e., is obtained by subtracting any two points in the subspace.
|
vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan
theorem vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p : P} {v : V},
p ∈ spanPoints k s → v ∈ vectorSpan k s → v +ᵥ p ∈ spanPoints k s
This theorem states that for any ring `k`, additive commutative group `V`, and affine torsor `P`, given a set `s` of points in `P`, if a point `p` is in the affine span of `s` and a vector `v` is in the submodule spanned by the differences of `s`, then the result of adding `v` to `p` (denoted as `v +ᵥ p`) is also in the affine span of `s`. In other words, within the context of affine spaces, adding a vector from the spanning submodule to a point in the affine span, yields another point in the affine span.
More concisely: If a point in an affine torsor lies in the affine span of a set of points and a vector is in the submodule spanned by the differences of those points, then the sum of that vector and the point is also in the affine span.
|
AffineSubspace.direction_eq_vectorSpan
theorem AffineSubspace.direction_eq_vectorSpan :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : AffineSubspace k P), s.direction = vectorSpan k ↑s
The theorem `AffineSubspace.direction_eq_vectorSpan` asserts that for any affine subspace `s` in a vector space over a ring `k`, the direction of the affine subspace `s` is precisely the vector span of the set of points in `s`. In other words, the set of all possible vectors that can be formed by difference of points in `s` spans the direction of the affine subspace `s`. Here, the `AffineSubspace` and `vectorSpan` are defined in the context of a ring `k`, an additive commutative group `V`, and a module `V` over `k`, where `V` acts as an additively written torsor for the points `P`.
More concisely: The direction of an affine subspace in a vector space over a ring is equal to the vector span of any set of points lying in the subspace.
|
AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl
theorem AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s1 s2 : AffineSubspace k P},
(↑s1).Nonempty → (↑s2).Nonempty → IsCompl s1.direction s2.direction → ∃ p, ↑s1 ∩ ↑s2 = {p}
This theorem states that if there are two nonempty affine subspaces such that their directions are complements of each other, then these subspaces intersect at exactly one point. The subspaces are given in a context where there is a Ring `k`, an Additive Commutative Group `V`, and `V` is a Module over `k`. Additionally, there is an Additive Torsor `S` over `V` and `P`. The theorem further requires the existence of at least one point each in both subspaces and that the direction of one subspace is the complement of the direction of the other subspace. Under these conditions, the theorem guarantees the existence of a point `p` such that the intersection of the two subspaces is the singleton set containing `p`.
More concisely: Given two nonempty affine subspaces of a module over a ring with complementary directions, there exists exactly one point of intersection.
|
AffineSubspace.vsub_left_mem_direction_iff_mem
theorem AffineSubspace.vsub_left_mem_direction_iff_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ∀ (p2 : P), p -ᵥ p2 ∈ s.direction ↔ p2 ∈ s
This theorem states that given a point `p` in an affine subspace `s`, the result of subtracting another point `p2` from `p` will be in the direction of the subspace `s` if and only if `p2` is a point in the subspace `s`. Here, all the elements are over a Ring `k`, the vector space is of type `V` with addition operation from commutative group and scalar multiplication from the module `k V`, and the affine space is of type `P` with a subtract operation over the vector space `V`.
More concisely: A point `p2` is in an affine subspace `s` if and only if the difference `p - p2` is in the direction of `s`, where `p` is a point in `s` and the operations are defined over a ring `k` with vector space `V` and affine space `P`.
|
AffineSubspace.affineSpan_coe
theorem AffineSubspace.affineSpan_coe :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s : AffineSubspace k P), affineSpan k ↑s = s
This theorem states that for any affine subspace `s` of a type `P` over a ring `k`, if you coerce that subspace to a set and then take the affine span of that set, you will get back the original subspace `s`. This is true for any ring `k` and types `V` and `P`, where `V` is an additive commutative group and a module over `k`, and `P` is an affine torsor over `V`.
More concisely: For any affine subspace `s` of an affine torsor `P` over a ring `k`, where `P` is a module over an additive commutative group `V` as a set, the affine span of `s` equals `s`.
|
vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints
theorem vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p1 p2 : P},
p1 ∈ spanPoints k s → p2 ∈ spanPoints k s → p1 -ᵥ p2 ∈ vectorSpan k s
This theorem states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, if a set `s` of points `P` is given, and `p1` and `p2` are any two points in the affine span of `s` (indicated by `p1 ∈ spanPoints k s` and `p2 ∈ spanPoints k s`), then the vector obtained by subtracting `p2` from `p1` (denoted by `p1 -ᵥ p2`) is a member of the submodule spanned by the differences of the points in `s` (signified by `p1 -ᵥ p2 ∈ vectorSpan k s`). In mathematical terms, if two points belong to the affine span of a set, their difference belongs to the vector space spanned by the set.
More concisely: For any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, if `p1, p2` are points in `P` lying in the affine span of a set `s`, then `p1 - p2` is in the submodule of `P` spanned by the differences of points in `s`.
|
affineSpan_coe_preimage_eq_top
theorem affineSpan_coe_preimage_eq_top :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (A : Set P) [inst_4 : Nonempty ↑A], affineSpan k (Subtype.val ⁻¹' A) = ⊤
This theorem states that for any set `A` of points in an affine space `P` over a ring `k`, with the vector space `V` as the associated vector space, if `A` is nonempty, then the preimage under the subtype projection of `A`, when considered as a subset of its own affine span, spans the whole of this affine subspace. In other words, the smallest affine subspace containing the set `A` is spanned by `A` itself.
More concisely: If `A` is a nonempty subset of an affine space `P` over a ring `k`, then the affine subspace spanned by `A` is equal to the subspace spanned by `A` considered as a subset of its affine span.
|
spanPoints_nonempty
theorem spanPoints_nonempty :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : Set P), (spanPoints k s).Nonempty ↔ s.Nonempty
The theorem `spanPoints_nonempty` states that for any type `k`, which is a ring, and types `V` and `P` where `V` is an additive commutative group and `P` is an additive torsor over `V`, the span of points of a set `s` of type `Set P` is nonempty if and only if the set `s` itself is nonempty. This span of points, denoted by `spanPoints k s`, is defined in terms of the existence of a point in the set `s` and a vector in the vector span of the set `s`, such that any point `p` in the span is a translation of the point in the set by the vector. The theorem relates the non-emptiness of the original set with the non-emptiness of its affine span.
More concisely: For any additive commutative group V, ring k, and additive torsor P over V, the span of a nonempty set of points in P is a nonempty subspace of P.
|
AffineSubspace.eq_of_direction_eq_of_nonempty_of_le
theorem AffineSubspace.eq_of_direction_eq_of_nonempty_of_le :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P},
s₁.direction = s₂.direction → (↑s₁).Nonempty → s₁ ≤ s₂ → s₁ = s₂
This theorem states that if we have two affine subspaces `s₁` and `s₂` in a module over a ring, and if `s₁` is nonempty and contained within `s₂`, then if `s₁` and `s₂` share the same direction, they must be equal. This theorem is relevant in the context of linear algebra and affine geometry.
More concisely: If `s₁` is a nonempty affine subspace contained in `s₂` with the same direction in a module over a ring, then `s₁` equals `s₂`.
|
AffineSubspace.mem_direction_iff_eq_vsub
theorem AffineSubspace.mem_direction_iff_eq_vsub :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P},
(↑s).Nonempty → ∀ (v : V), v ∈ s.direction ↔ ∃ p1 ∈ s, ∃ p2 ∈ s, v = p1 -ᵥ p2
This theorem states that for any given nonempty affine subspace `s` over a field `k` with associated vector space `V` and points `P`, a vector `v` is in the direction of `s` if and only if there exists a pair of points `p1` and `p2` in `s` such that `v` is the vector obtained by subtracting `p2` from `p1`. The subtraction operation used here is the one defined for affine spaces, which takes two points and returns the vector from the second to the first.
More concisely: A vector is in the direction of an affine subspace if and only if it is the vector between two points in the subspace.
|
AffineMap.lineMap_rev_mem_affineSpan_pair
theorem AffineMap.lineMap_rev_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), (AffineMap.lineMap p₂ p₁) r ∈ affineSpan k {p₁, p₂}
This theorem states that for any ring 'k', any commutative additive group 'V', any type 'P' with 'V' acting freely and transitively on 'P', and any scalar 'r' and points 'p₁' and 'p₂' of type 'P', the map 'lineMap' from 'p₂' to 'p₁' applied to 'r' results in a point that lies in the affine span of the set containing 'p₁' and 'p₂'. In other words, any point on the line segment between two points 'p₁' and 'p₂', including 'p₁' and 'p₂' themselves and their extensions, belongs to the smallest affine subspace that contains 'p₁' and 'p₂'.
More concisely: For any ring 'k', commutative additive group 'V', type 'P' with 'V' acting freely and transitively on 'P', and points 'p₁', 'p₂' in 'P', the image of 'lineMap' from 'p₂' to 'p₁' applied to any scalar 'r' lies in the affine span of '{p₁, p₂}'.
|
AffineSubspace.gc_map_comap
theorem AffineSubspace.gc_map_comap :
∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [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₂),
GaloisConnection (AffineSubspace.map f) (AffineSubspace.comap f)
The theorem `AffineSubspace.gc_map_comap` states that for any type `k` with a ring structure, types `V₁`, `P₁`, `V₂`, `P₂` with respective additive commutative group structures and module structures over `k`, and the types `P₁` and `P₂` further possessing an affine space structure over `V₁` and `V₂` respectively, and for any affine map `f` from `P₁` to `P₂`, there exists a Galois connection between the function `AffineSubspace.map f` and the function `AffineSubspace.comap f`. A Galois connection, in this context, means that for all affine subspaces `a` of `P₁` and `b` of `P₂`, `f` mapping the affine subspace `a` is a subset of `b` if and only if `a` is a subset of `f` reverse-mapped from the subspace `b`.
More concisely: For any affine spaces `P₁` and `P₂` over a ring `k` with an affine map `f` between them, `AffineSubspace.map f` and `AffineSubspace.comap f` form a Galois connection on affine subspaces of `P₁` and `P₂`.
|
vectorSpan_eq_span_vsub_set_right
theorem vectorSpan_eq_span_vsub_set_right :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p : P},
p ∈ s → vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' s)
This theorem states that for a given set `s` of points in a module over a ring, and a specific point `p` in that set, the `vectorSpan` of the set `s` is equal to the submodule spanned by the set of vectors obtained by subtracting `p` from each point in `s`. In mathematical terms, it says that if `s` is a subset of `P` and `p` is an element of `s`, then the vector span of `s` is the same as the span of the set `{x - p | x ∈ s}` in the module `V` over `k`, where `V` is an additive commutative group and `P` is an additive torsor over `V`.
More concisely: Given a set `s` of points in an additive commutative group `V` over a ring `k`, with `p` as an element of `s`, the vector span of `s` equals the submodule spanned by the set `{x - p | x ∈ s}`.
|
AffineSubspace.span_union
theorem AffineSubspace.span_union :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s t : Set P), affineSpan k (s ∪ t) = affineSpan k s ⊔ affineSpan k t
This theorem states that the affine span of the union of two sets is equal to the supremum of their individual affine spans. In other words, the smallest affine subspace containing all points in either of two sets is equivalent to the largest affine subspace that is contained in the individual affine spans of these sets. This is a property that holds for any field `k`, any additive commutative group `V`, and any torsor `P` over `V`, where `V` is a module over `k`.
More concisely: The affine span of the union of two sets is equal to the supremum of their individual affine spans in any additive commutative group over a field, for any torsor over the group.
|
AffineSubspace.direction_eq_top_iff_of_nonempty
theorem AffineSubspace.direction_eq_top_iff_of_nonempty :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s : AffineSubspace k P}, (↑s).Nonempty → (s.direction = ⊤ ↔ s = ⊤)
This theorem states that for any non-empty affine subspace 's', defined over a ring 'k', with an underlying vector space 'V' and point space 'P', the direction of 's' is equal to the top element (denoted as '⊤') if and only if 's' itself is the top element. Here, the top element typically represents the entire space. In other words, an affine subspace spans the entire space if and only if its direction (a linear subspace that can be obtained from it) also spans the entire space.
More concisely: An affine subspace of a vector space over a ring is the entire space if and only if its direction is the top element (the entire vector space).
|
AffineSubspace.coe_affineSpan_singleton
theorem AffineSubspace.coe_affineSpan_singleton :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (p : P), ↑(affineSpan k {p}) = {p}
The theorem `AffineSubspace.coe_affineSpan_singleton` states that the affine span of a single point, when coerced to a set, contains only that point. This is applicable across any ring `k`, additive commutative group `V`, and module `k V`, where `P` is an add-torsor over `V`. In other words, when the affine span operation is applied to a set containing just one point `p`, and the resultant affine subspace is transformed to a set, it's equal to the original singleton set `{p}`.
More concisely: The theorem `AffineSubspace.coe_affineSpan_singleton` asserts that the set representation of the affine span of a single point is equal to that point itself.
|
AffineSubspace.coe_eq_bot_iff
theorem AffineSubspace.coe_eq_bot_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (Q : AffineSubspace k P), ↑Q = ∅ ↔ Q = ⊥
This theorem states that for any field `k`, additive commutative group `V`, and `P` with the structure of an `AddTorsor` with respect to `V`, an affine subspace `Q` of `P` is empty if and only if `Q` is equal to the bottom element (i.e., the smallest element in the lattice of subspaces). In simpler words, it asserts that an affine subspace is empty if and only if it is the minimal possible subspace.
More concisely: A subspace of an additive commutative group carrying the structure of an additive torsor over a field is empty if and only if it is the bottom element in the lattice of subspaces.
|
AffineSubspace.span_iUnion
theorem AffineSubspace.span_iUnion :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {ι : Type u_4} (s : ι → Set P), affineSpan k (⋃ i, s i) = ⨆ i, affineSpan k (s i)
The theorem `AffineSubspace.span_iUnion` states that for any type `k` which has a ring structure, type `V` which forms an additive commutative group and a module over `k`, and type `P` that forms an additive torsor over `V`, the affine span (smallest affine subspace) of a union of an indexed family of sets of points in `P` is equivalent to the sup (supremum or least upper bound) of the affine spans of the individual sets in the family. This is similar to the principle that the span of the union of a collection of subsets is equal to the sup of their individual spans.
More concisely: For any ring `k`, additive commutative group and `k`-module `V`, and additive torsor `P` over `V`, the affine span of a union of sets of points in `P` is equal to the supremum of the affine spans of the individual sets.
|
AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top
theorem AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s1 s2 : AffineSubspace k P},
(↑s1).Nonempty → (↑s2).Nonempty → s1.direction ⊔ s2.direction = ⊤ → (↑s1 ∩ ↑s2).Nonempty
This theorem states that given two nonempty affine subspaces in a module, if their directions span the entire module, then the intersection of these two subspaces is nonempty. This is provided under the conditions where the underlying field `k` is a ring and type `V` is an additive commutative group that also forms a module over `k`. Additionally, there's a condition that type `V` forms an additive torsor over points `P`.
More concisely: Given two nonempty affine subspaces in a commutative `k`-module `V` that form a spanning set, their intersection is nonempty.
|
affineSpan_pair_le_of_mem_of_mem
theorem affineSpan_pair_le_of_mem_of_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ : P} {s : AffineSubspace k P}, p₁ ∈ s → p₂ ∈ s → affineSpan k {p₁, p₂} ≤ s
The theorem `affineSpan_pair_le_of_mem_of_mem` states that for any ring `k`, an additive commutative group `V`, and an affine torsor `P`, given two points `p₁` and `p₂` and an affine subspace `s` of `P`, if both `p₁` and `p₂` are elements of `s`, then the affine span of `p₁` and `p₂` is a subset of or equal to `s`. In other words, the smallest affine subspace that contains both `p₁` and `p₂` is contained within the original subspace `s`. This theorem is a statement about the geometric property of affine subspaces.
More concisely: For any ring `k`, additive commutative group `V`, affine torsor `P`, points `p₁, p₂` in `P`, and affine subspace `s` of `P` containing `p₁` and `p₂`, the affine span of `{p₁, p₂}` is contained in `s`.
|
vectorSpan_image_eq_span_vsub_set_right_ne
theorem vectorSpan_image_eq_span_vsub_set_right_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) {s : Set ι} {i : ι},
i ∈ s → vectorSpan k (p '' s) = Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))
The theorem `vectorSpan_image_eq_span_vsub_set_right_ne` states that for any ring `k`, any additive commutative group `V`, any `V`-module `P`, any function `p` from some type `ι` to `P`, any set `s` of type `ι`, and any element `i` of type `ι` that is a member of `s`, the vector span (the submodule generated by the differences) of the image under `p` of the set `s` is equal to the submodule spanned by the image of the set `s` excluding `i`, under the function that subtracts `p i` from each element. Here, subtraction is defined using the vector space structure of `P`.
More concisely: For any ring `k`, additive commutative group `V`, `V`-module `P`, function `p` from set `ι` to `P`, set `s` of `ι`, and `i` in `s`, the vector span of `p`(s) is equal to the span of `p`(s \ {i}) in `P` with respect to subtraction.
|
AffineMap.lineMap_mem
theorem AffineMap.lineMap_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {Q : AffineSubspace k P} {p₀ p₁ : P} (c : k),
p₀ ∈ Q → p₁ ∈ Q → (AffineMap.lineMap p₀ p₁) c ∈ Q
This theorem states that for any types `k`, `V`, and `P`, where `k` is a ring, `V` is an abelian (or commutative) group, `V` is a module over `k`, and `P` is a torsor for `V`, for any affine subspace `Q` of `P`, two points `p₀` and `p₁` in `P`, and any scalar `c` from `k`, if `p₀` and `p₁` are in `Q`, then the point resulting from the affine map `lineMap`, which maps from `k` to `P` sending `0` to `p₀` and `1` to `p₁`, applied to `c`, is also in `Q`. In simpler terms, if `p₀` and `p₁` are points in an affine subspace, then any point on the line segment between `p₀` and `p₁` (defined by `c`) is also in the subspace.
More concisely: Given any affine subspace Q of a V-torsor P over a ring k, if two points p₀ and p₁ in P lie in Q, then the point on the line segment between p₀ and p₁ defined by the scalar c is also in Q.
|
AffineSubspace.vadd_mem_of_mem_direction
theorem AffineSubspace.vadd_mem_of_mem_direction :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {v : V}, v ∈ s.direction → ∀ {p : P}, p ∈ s → v +ᵥ p ∈ s
The theorem `AffineSubspace.vadd_mem_of_mem_direction` states that for any ring `k`, additive commutative group `V`, and affine torsor `P`, if we have an affine subspace `s` of `P` and a vector `v` in the direction of this subspace, then for any point `p` in `s`, the vector `v` added to the point `p` (notated as `v +ᵥ p`) is also in the subspace `s`. In other words, if we move along the direction of an affine subspace from a point within the subspace, we remain within the subspace.
More concisely: For any affine subspace `s` of an affine torsor `P` over a ring `k` and any vector `v` in the direction of `s`, if `p` is a point in `s`, then `v +ᵥ p` is also in `s`.
|
AffineSubspace.ext
theorem AffineSubspace.ext :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p q : AffineSubspace k P}, (∀ (x : P), x ∈ p ↔ x ∈ q) → p = q
This theorem states that for any two affine subspaces `p` and `q` in an affine space `P` over a ring `k` with an associated vector space `V`, if every point in `P` has the same membership status in `p` and `q` (i.e., each point in `P` is in `p` if and only if it is in `q`), then `p` and `q` are the same affine subspace. The vector space `V` is equipped with operations from the commutative group of addition (`AddCommGroup V`) and the module structure (`Module k V`), and the affine space `P` is related to the vector space `V` through the `AddTorsor` structure.
More concisely: If two affine subspaces in an affine space over a ring have the same membership for all points, they are equal subspaces.
|
AffineSubspace.eq_iff_direction_eq_of_mem
theorem AffineSubspace.eq_iff_direction_eq_of_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p : P},
p ∈ s₁ → p ∈ s₂ → (s₁ = s₂ ↔ s₁.direction = s₂.direction)
This theorem states that, for any two affine subspaces ('s₁' and 's₂') of a given type 'P', and a point 'p' of that type, if 'p' belongs to both 's₁' and 's₂', then 's₁' equals 's₂' if and only if the direction of 's₁' equals the direction of 's₂'. Here, the ring is of type 'k', the additive commutative group is of type 'V', and the module is of type 'V' over the ring 'k'. The addition of a group element of 'V' to a point of 'P' results in another point of 'P' (represented by AddTorsor V P).
More concisely: Given affine subspaces $s\_1$ and $s\_2$ of type $P$ in a vector space $V$ over a field $k$, and a point $p$ in $P$, if $p$ belongs to both $s\_1$ and $s\_2$, then $s\_1 = s\_2$ if and only if the directions of $s\_1$ and $s\_2$ are equal.
|
AffineSubspace.lt_iff_le_and_exists
theorem AffineSubspace.lt_iff_le_and_exists :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), s1 < s2 ↔ s1 ≤ s2 ∧ ∃ p ∈ s2, p ∉ s1
This theorem states that for any two subspaces, `s1` and `s2`, in an affine space, `s1` is strictly less than `s2` if and only if two conditions are met: `s1` is less than or equal to `s2`, and there exists a point `p` that is in `s2` but not in `s1`. The affine space is characterized by a ring `k`, an additive commutative group `V`, and a module `P` over `k` with `V` as its additive group. In this context, 'less than' and 'less than or equal to' refer to the subset relationships between the subspaces.
More concisely: For subspaces `s1` and `s2` of an affine space over a ring `k` with additive group `V` and module `P`, `s1` is a proper subset of `s2` if and only if `s1` is a subset of `s2` and there exists a point in `s2` not in `s1`.
|
vsub_rev_mem_vectorSpan_pair
theorem vsub_rev_mem_vectorSpan_pair :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p₁ p₂ : P), p₂ -ᵥ p₁ ∈ vectorSpan k {p₁, p₂}
The theorem `vsub_rev_mem_vectorSpan_pair` states that for any field `k`, additive commutative group `V`, additive torsor `P`, and two points `p₁` and `p₂` in `P`, the vector resulting from subtracting `p₁` from `p₂` (in that order) is an element of the vector span of the set containing `p₁` and `p₂`. In other words, the reversed difference vector between two points lies within the subspace spanned by the vectors defined by differences of the pair of points.
More concisely: For any additive torsor P over a field k, and any two points p₁ and p₂ in P, the vector p₂ - p₁ is in the span of {p₁, p₂}.
|
AffineSubspace.mem_top
theorem AffineSubspace.mem_top :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (p : P), p ∈ ⊤
This theorem states that for any point `p` in an affine space `P`, where `P` is a torsor for a vector space `V` over a ring `k`, the point `p` is an element of the top subspace. In other words, all points in the affine space are included in the top subspace.
More concisely: Every point in an affine space over a ring, which is a torsor for a vector space, lies in the top subspace.
|
direction_affineSpan
theorem direction_affineSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : Set P), (affineSpan k s).direction = vectorSpan k s
The theorem `direction_affineSpan` states that for any set `s` of points in an affine space `P` over a ring `k`, with the associated vector space `V`, the direction of the affine subspace spanned by `s` is equal to the submodule spanned by the pairwise differences of the points in `s`. Here, the direction of an affine subspace is understood as the set of all vectors that can be obtained by subtracting any two points in the subspace, and the affine span of a set of points is the smallest affine subspace that contains all of those points.
More concisely: The direction of the affine subspace spanned by a set of points in an affine space is equal to the submodule generated by the pairwise differences of those points.
|
AffineSubspace.top_coe
theorem AffineSubspace.top_coe :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P], ↑⊤ = Set.univ
The theorem `AffineSubspace.top_coe` states that, for any field `k`, additive commutative group `V`, and module `P` over `k` and `V`, where `V` acts on `P` by addition (making `P` a "torso" under `V`), the top element (denoted by `⊤`) coerced to a set equals the universal set (`Set.univ`). This means that the entirety of `P` is encapsulated by the top affine subspace, when viewed as a set. In other words, when we consider the whole affine subspace, it covers all possible points in our space `P`.
More concisely: For any additive commutative group `V`, field `k`, and `k`-module `P` with `V` acting on `P` by addition, the top element `⊤` of the affine subspace of `P` coincides with the universal set `Set.univ`.
|
AffineSubspace.le_def'
theorem AffineSubspace.le_def' :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), s1 ≤ s2 ↔ ∀ p ∈ s1, p ∈ s2
This theorem states that for any two subspaces `s1` and `s2` in an affine space, `s1` is less than or equal to `s2` if and only if every point `p` that belongs to `s1` also belongs to `s2`. The affine space is defined over a ring `k` with an associated module `V` over `k` and an additive torsor `S` over `V`.
More concisely: For subspaces `s1` and `s2` in an affine space over a ring `k` with module `V` and additive torsor `S`, `s1 ⊆ s2` if and only if `p ∈ s1` implies `p ∈ s2` for all points `p` in the affine space.
|
vectorSpan_empty
theorem vectorSpan_empty :
∀ (k : Type u_1) {V : Type u_2} (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P], vectorSpan k ∅ = ⊥
The theorem `vectorSpan_empty` states that for any ring `k`, additive commutative group `V`, type `P`, and an affine space `P` over `V` with coefficients in `k`, the vector span of the empty set is the bottom element, `⊥`. In mathematical terms, this means the smallest possible subspace, in the given module, that the vector span of an empty set can generate is the zero subspace.
More concisely: The vector span of the empty set in an affine space over a ring is the zero subspace.
|
AffineSubspace.coe_direction_eq_vsub_set
theorem AffineSubspace.coe_direction_eq_vsub_set :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P}, (↑s).Nonempty → ↑s.direction = ↑s -ᵥ ↑s
This theorem states that for any nonempty affine subspace, the set of vectors in the direction of this subspace is given by `vsub_set`, that is, the result of subtracting every point in the subspace from every other point. This involves several mathematical structures such as a ring, an additive commutative group, a module over the ring, and an affine torsor.
More concisely: For any nonempty affine subspace in a vector space, the set of vectors in the subspace's direction is equal to the span of the differences between any two points in the subspace.
|
vadd_right_mem_affineSpan_pair
theorem vadd_right_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ : P} {v : V}, v +ᵥ p₂ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
This theorem states that for any ring `k`, additively commutative group `V`, module over `k` on `V`, pointed module `V` over `P`, and points `p₁`, `p₂` in `P`, and a vector `v` in `V`, the vector `v` added to the second point `p₂` is in the affine span of the points `p₁` and `p₂` if and only if there exists a scalar `r` in `k` such that `r` times the difference between points `p₁` and `p₂` equals `v`. This theorem links the concept of an affine span with scalar multiplication and difference of points.
More concisely: For any ring `k`, additively commutative group `V` as a `k`-module, pointed `k`-module `(V, P)`, and points `p₁, p₂ in P` and vector `v in V`, `v` lies in the affine span of `{p₁, p₂}` if and only if there exists `r in k` such that `v = r * (p₁ - p₂)`.
|
subset_spanPoints
theorem subset_spanPoints :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : Set P), s ⊆ spanPoints k s
The theorem `subset_spanPoints` states that for any set of points `s` in an affine space `P` over a ring `k` with associated vector space `V`, the set `s` is always a subset of its span points. In other words, every point in `s` can be represented as a combination of a point and a vector, where the point is in `s` and the vector is in the vector span of `s`.
More concisely: For any set of points `s` in an affine space `P` over a ring `k`, the span of `s` contains `s`.
|
AffineSubspace.map_id
theorem AffineSubspace.map_id :
∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
[inst_3 : AddTorsor V₁ P₁] (s : AffineSubspace k P₁), AffineSubspace.map (AffineMap.id k P₁) s = s
This theorem states that for every type `k` with a ring structure, type `V1` forming an additive commutative group and a `k`-module, type `P1` forming a torsor under `V1`, and any affine subspace `s` of `P1`, the result of mapping `s` through the identity affine map (which maps every point to itself) is `s` itself. In other words, applying the identity affine map to an affine subspace doesn't change the subspace.
More concisely: For every ring `k`, additive commutative group `V1` with `k`-module structure, and torsor `P1` under `V1`, the application of the identity affine map to an affine subspace of `P1` results in the same subspace.
|
AffineSubspace.lt_def
theorem AffineSubspace.lt_def :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), s1 < s2 ↔ ↑s1 ⊂ ↑s2
This theorem asserts that the "less than" (`<`) relation for affine subspaces in the context of a ring and an additive commutative group is equivalent to the strict subset relation (`⊂`) between the sets that correspond to these subspaces. In other words, for any two given affine subspaces `s1` and `s2`, `s1` is considered "less than" `s2` if and only if the set of points in `s1` is a strict subset of the set of points in `s2`.
More concisely: The theorem asserts that for affine subspaces $s\_1$ and $s\_2$ in a ring and additive commutative group, $s\_1 \subset s\_2$ if and only if $s\_1 \subsetneq s\_2$ (i.e., $s\_1$ is a proper subset of $s\_2$), where $\subset$ denotes set inclusion and $\subsetneq$ denotes strict set inclusion. In terms of the affine subspaces themselves, $s\_1 < s\_2$ (where $<$ represents the "less than" relation for subspaces in Lean 4) if and only if the corresponding sets of points have this relationship.
|
vadd_left_mem_affineSpan_pair
theorem vadd_left_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ : P} {v : V}, v +ᵥ p₁ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
The theorem `vadd_left_mem_affineSpan_pair` states that for any given field `k`, additive commutative group `V`, and an `AddTorsor` `P` (a torsor is a non-empty set where the action of an additive group is free and transitive), for any points `p₁` and `p₂` in `P`, and a vector `v` in `V`, the vector `v` added to the first point `p₁` (`v +ᵥ p₁`) is in the affine span of the two points `p₁` and `p₂` if and only if there exists a scalar `r` in `k` such that the scalar multiplication of `r` and the difference of the two points (`r • (p₂ -ᵥ p₁)`) equals to `v`. In mathematical terms, this theorem establishes the relationship between the condition of a vector lying in the affine span of two points and being a scalar multiple of the difference of these two points.
More concisely: A vector is in the affine span of two points in a vector space if and only if it is a scalar multiple of the difference between the points.
|
AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial
theorem AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s : Set P} [inst_3 : Nontrivial P], affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
This theorem states that in a non-trivial space, the affine span of a set is equal to the entirety of the space if and only if the vector span of the set is also equal to the entirety of the space. Here, the affine span of a set of points is defined as the smallest affine subspace that contains those points, and the vector span is the submodule spanning the differences of a set of points. The space is considered non-trivial if it contains at least two distinct points. The theorem is valid in the context of a ring and a module over that ring, an additive commutative group, and an add-torsor, which provides a geometric structure to the vectors.
More concisely: In a non-trivial vector space, the affine span of a set equals the entire space if and only if the vector span of the set does.
|
coe_affineSpan
theorem coe_affineSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : Set P), ↑(affineSpan k s) = spanPoints k s
The theorem `coe_affineSpan` states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and an additive torsor `P` of `V`, the set representation (`↑`) of the affine span of any set `s` of points in `P` is equivalent to the span of points of `s` in `P`. In other words, the set of points in the smallest affine subspace containing the set `s` (`affineSpan k s`) is exactly the same as the set of points that can be expressed as a linear combination of vectors in `s` (`spanPoints k s`).
More concisely: For any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` of `V`, the set representation of the affine span of a set `s` of points in `P` equals the span of points in `s` in `P`.
|
vectorSpan_eq_span_vsub_set_left_ne
theorem vectorSpan_eq_span_vsub_set_left_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p : P},
p ∈ s → vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))
The theorem `vectorSpan_eq_span_vsub_set_left_ne` states that, for a given ring `k`, the vector space `V` of some type, a point `P`, and a set `s` of points of type `P` which includes the point `p`, the `vectorSpan` of `s` (which represents the submodule generated by the differences of all pairs of points in the set) is equal to the `Submodule.span` of the set of differences between `p` and all other points in `s` (excluding the difference of `p` with itself). In other words, the set of all pairwise differences in `s` generates the same subspace as the set of differences between a fixed point `p` in `s` and all the other points in `s`.
More concisely: For any ring `k`, vector space `V` of type `P`, point `p` in `V`, and set `s` of points in `V` containing `p`, the submodule generated by the differences of all pairs of distinct points in `s` is equal to the submodule generated by the differences between `p` and all other points in `s`.
|
vsub_set_subset_vectorSpan
theorem vsub_set_subset_vectorSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : Set P), s -ᵥ s ⊆ ↑(vectorSpan k s)
This theorem states that for any ring `k`, any set `s` of points in an additive torsor `P` over a module `V` over `k` (with `V` being an additive commutative group), the set of all differences of points in `s` (denoted as `s -ᵥ s`) is a subset of the vector span of `s`. In other words, any vector that can be formed by subtracting two points in `s` can be expressed as a linear combination of vectors in the vector span of `s`.
More concisely: For any ring `k`, any additive torsor `P` over a module `V` (an additive commutative group) over `k`, the differences of points in `P` form a subset of the vector span of `P`.
|
AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top
theorem AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s : Set P}, affineSpan k s = ⊤ → vectorSpan k s = ⊤
The theorem `AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top` states that for any type `k` with a Ring structure, types `V` and `P` where `V` is an additive commutative group and `P` is an affine torsor over `V`, and any set `s` of points in `P`, if the affine span of the set `s` is the total space (`⊤`), then the vector span of the same set `s` is also the total space (`⊤`). In simpler terms, if all points in the affine space can be expressed as affine combinations of points in `s`, then all vectors in the vector space can be expressed as linear combinations of differences of points in `s`.
More concisely: If the affine span of a set of points in an affine torsor over a vector space is the total space, then the vector span of the same set is also the total space.
|
AffineSubspace.span_empty
theorem AffineSubspace.span_empty :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P], affineSpan k ∅ = ⊥
The theorem `AffineSubspace.span_empty` states that in any Affine space, the span of the empty set is the smallest possible Affine subspace (`⊥`). This holds for any scalar field `k`, vector space `V` over `k`, and Affine space `P` based on `V`, given that `k` forms a Ring, `V` forms an Additive Commutative Group, and `V` is a module over `k`.
More concisely: In any Affine space based on a module over a ring, the span of the empty set is the trivial subspace.
|
mem_vectorSpan_pair_rev
theorem mem_vectorSpan_pair_rev :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ : P} {v : V}, v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
The theorem `mem_vectorSpan_pair_rev` states that for any ring `k`, additively commutative group `V`, additive torsor `P`, and points `p₁` and `p₂` in `P`, and a vector `v` in `V`, the vector `v` belongs to the `vectorSpan` of `p₁` and `p₂` if and only if there exists a scalar `r` in the ring `k` such that `r * (p₂ - p₁)` is equal to `v`. In simple terms, it indicates that a vector is in the span of two points if and only if it can be expressed as a multiple of the difference of the two points, with the order reversed.
More concisely: For any ring `k`, additively commutative group `V`, additive torsor `P` with points `p₁, p₂`, and vector `v` in `V`, `v` is in the span of `p₁` and `p₂` if and only if there exists a scalar `r` in `k` such that `v = r * (p₂ - p₁)`.
|
AffineSubspace.nonempty_iff_ne_bot
theorem AffineSubspace.nonempty_iff_ne_bot :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (Q : AffineSubspace k P), (↑Q).Nonempty ↔ Q ≠ ⊥
This theorem, titled `AffineSubspace.nonempty_iff_ne_bot`, states that for any field `k`, any additive commutative group `V`, any `P` which is a module over `k` with `V` as its corresponding vector space (`V` is an additive torsor for `P`), and any affine subspace `Q` of `P`, the set `Q` is nonempty (i.e., there exists an element in `Q`) if and only if `Q` is not the bottom element (`⊥`, which represents the empty set in this context).
More concisely: An affine subspace of a module over a field is nonempty if and only if it is not the empty set.
|
AffineSubspace.affineSpan_eq_sInf
theorem AffineSubspace.affineSpan_eq_sInf :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s : Set P), affineSpan k s = sInf {s' | s ⊆ ↑s'}
The theorem `AffineSubspace.affineSpan_eq_sInf` states that, for any field `k`, any additive commutative group `V`, and any type `P` that is an affine space with respect to `V`, along with a set `s` of points in `P`, the affine span of `s` is equal to the infimum (`sInf`) of the set of all affine subspaces that contain `s`. In other words, the affine span of a set of points is the smallest affine subspace that contains all the points in the set.
More concisely: The affine span of a set of points in an affine space is the smallest affine subspace that contains them.
|
affineSpan_induction'
theorem affineSpan_induction' :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p : (x : P) → x ∈ affineSpan k s → Prop},
(∀ (y : P) (hys : y ∈ s), p y ⋯) →
(∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P)
(hw : w ∈ affineSpan k s), p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯) →
∀ {x : P} (h : x ∈ affineSpan k s), p x h
The theorem `affineSpan_induction'` is a dependent version of `affineSpan_induction`. It states that for any types `k`, `V`, and `P`, any ring structure on `k`, any additive commutative group structure on `V`, any module structure on `V` over `k`, any affine torsor structure on `P` with respect to `V`, any set `s` of points in `P`, and any property `p` of points in the affine span of `s` such that:
- `p` holds for all points in `s`, and
- for any scalar `c` in `k` and any points `u`, `v`, and `w` in the affine span of `s` such that `p` holds for `u`, `v`, and `w`, `p` also holds for the point resulting from scaling the vector from `v` to `u` by `c` and then translating `w` by the resulting vector,
then `p` holds for all points in the affine span of `s`. This theorem can be used for induction on properties of points in the affine span of a set.
More concisely: Given a set `s` of points in an affine torsor `P` over a module `V` with respect to a ring `k`, if a property `p` holds for all points in `s` and is closed under scaling and translation within the affine span of `s`, then `p` holds for all points in the affine span of `s`.
|
smul_vsub_rev_vadd_mem_affineSpan_pair
theorem smul_vsub_rev_vadd_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ affineSpan k {p₁, p₂}
The theorem `smul_vsub_rev_vadd_mem_affineSpan_pair` states that for any ring `k`, additive commutative group `V`, module `k V` and `V`-torsor `P`, and any scalar `r` in `k` and points `p₁` and `p₂` in `P`, the operation of scaling the vector difference of `p₁` and `p₂` by `r` and then adding the result to `p₂` results in a point which lies in the affine span of the set `{p₁, p₂}`. This essentially says that the set of all points obtainable by taking a particular linear combination of the differences of two points includes all points in the smallest affine subspace containing those two points.
More concisely: For any additive commutative group V, ring k, k-module V, V-torsor P, scalars r in k, and points p₁, p₂ in P, the point r * (p₁ - p₂) + p₂ is in the affine span of {p₁, p₂}.
|
subset_affineSpan
theorem subset_affineSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (s : Set P), s ⊆ ↑(affineSpan k s)
This theorem asserts that for any set `s` of points of type `P`, in a context where `k` is a ring, `V` is an additive commutative group, `P` is a module over `k` with `V` as the underlying additive group, and `P` forms an additive torsor over `V`, the set `s` is a subset of its affine span. More intuitively, this states that every point in a set is contained within the smallest affine subspace that includes the entire set, which reflects the geometric notion that the span of a set of points includes those points themselves.
More concisely: For any additive torsor `s` of a `k`-module `P` with underlying additive group `V`, `s` is contained in its affine span.
|
AffineSubspace.direction_lt_of_nonempty
theorem AffineSubspace.direction_lt_of_nonempty :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s1 s2 : AffineSubspace k P}, s1 < s2 → (↑s1).Nonempty → s1.direction < s2.direction
The theorem `AffineSubspace.direction_lt_of_nonempty` states that for any ring `k`, an additive commutative group `V`, and a module `V` over `k`, given an affine torsor `S` over `V`, if one nonempty affine subspace `s1` is a proper subset of another affine subspace `s2` (`s1` is strictly less than `s2`), then the direction of `s1` is also a proper subset of the direction of `s2`.
More concisely: If `s1` is a proper subset of `s2` in the hierarchy of affine subspaces of a vector space `V` over a ring `k`, then the direction of `s1` is contained in the direction of `s2`.
|
AffineSubspace.direction_inf_of_mem_inf
theorem AffineSubspace.direction_inf_of_mem_inf :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p : P},
p ∈ s₁ ⊓ s₂ → (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction
This theorem states that if a point `p` belongs to the intersection of two affine subspaces `s₁` and `s₂`, then the direction of the intersection of `s₁` and `s₂` is the same as the intersection of the directions of `s₁` and `s₂`. Here, the underlying field is `k`, the vector space is `V`, and the affine space is `P`, where `k` is a ring, `V` is an additive commutative group, and `V` is a module over `k`. Moreover, `S` is an add-torsor that converts differences between points in `P` into vectors in `V`.
More concisely: If subspaces $S\_1$ and $S\_2$ of an affine space $P$ over a commutative ring $k$ with a vector space $V$ and an add-torsor $S$ intersect at a point $p$, then the direction of their intersection is the same as the direction of the intersection of $S\_1$ and $S\_2$ as subspaces of $V$.
|
vsub_mem_vectorSpan_pair
theorem vsub_mem_vectorSpan_pair :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p₁ p₂ : P), p₁ -ᵥ p₂ ∈ vectorSpan k {p₁, p₂}
The theorem `vsub_mem_vectorSpan_pair` states that for any ring `k`, and for any vector space `V` over `k` that is also an additive group, and for any torsor `P` over `V`, the difference `p₁ -ᵥ p₂` between any two points `p₁` and `p₂` in `P` lies in the `vectorSpan` of the set containing `p₁` and `p₂`. In more mathematical terms, this means that the difference vector between any two points is a linear combination of the vectors that span the set that contains these two points.
More concisely: For any vector space V over a ring k and any torsor P over V, the difference between any two points in P lies in the vector span of {p₁, p₂}.
|
AffineSubspace.not_le_iff_exists
theorem AffineSubspace.not_le_iff_exists :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), ¬s1 ≤ s2 ↔ ∃ p ∈ s1, p ∉ s2
This theorem states that for any two affine subspaces `s1` and `s2` of a module over a ring, `s1` is not a subset of or equal to `s2` if and only if there exists a point `p` in `s1` that does not belong to `s2`. In other words, if there is at least one point in `s1` that `s2` does not contain, then `s1` is not a subset of `s2`. This theorem connects the concepts of subset relation and point membership in the context of affine subspaces.
More concisely: For affine subspaces `s1` and `s2` of a module over a ring, `s1` is properly contained in or disjoint from `s2` if and only if there exists a point in `s1` not in `s2`.
|
affineSpan_insert_eq_affineSpan
theorem affineSpan_insert_eq_affineSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p : P} {ps : Set P},
p ∈ affineSpan k ps → affineSpan k (insert p ps) = affineSpan k ps
The theorem `affineSpan_insert_eq_affineSpan` states that for any ring `k`, an additive commutative group `V`, a module `V` over `k`, an additive torsor `P` over `V`, a point `p` of type `P`, and a set `ps` of points of type `P`, if `p` is in the affine span of `ps`, then adding `p` to `ps` does not change the affine span of `ps`. In other words, the affine span of a set of points remains the same even if we add a point which is already in the affine span of the set. This theorem is relevant in the field of affine geometry.
More concisely: If a point is in the affine span of a set in a module over a ring, then adding that point to the set does not change the affine span.
|
vectorSpan_eq_span_vsub_set_left
theorem vectorSpan_eq_span_vsub_set_left :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p : P},
p ∈ s → vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' s)
The theorem `vectorSpan_eq_span_vsub_set_left` expresses that, given a set of points `s` in an additive torsor space `P` over a module `V`, and a point `p` within `s`, the vector span of `s` is equivalent to the span of the set of vectors formed by subtracting each point in `s` from `p`. Here, the vector subtraction `-ᵥ` returns a vector in `V`. In other words, in such a setting, we can create the vector span of `s` by looking at all vectors resulting from subtracting other points in `s` from a chosen point `p` in `s`, and then spanning over these vectors.
More concisely: The theorem asserts that the vector span of a set of points in an additive torsor space is equal to the span of the vectors obtained by subtracting each point in the set from a fixed point in the set.
|
vectorSpan_eq_span_vsub_set_right_ne
theorem vectorSpan_eq_span_vsub_set_right_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p : P},
p ∈ s → vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
The theorem `vectorSpan_eq_span_vsub_set_right_ne` states that, for any type `k` with a ring structure, a type `V` with an additive commutative group structure and a `k`-module structure, a type `P` with an additive torsor structure over `V`, a set `s` of elements of type `P`, and a point `p` of type `P` that is an element of the set `s`, the vector span of `s` is equal to the span of the set of pairwise subtractions of the elements of `s` from the point `p`, excluding the case where `p` is subtracted from itself.
In mathematical terms, if we denote by `s -ᵥ s` the set of all differences `s_i - s_j` where `s_i` and `s_j` are in `s`, and by `(fun x => x -ᵥ p) '' (s \ {p})` the set of all differences `s_i - p` where `s_i` is in `s` but not equal to `p`, then the theorem says that the `k`-submodule spanned by `s -ᵥ s` is the same as the `k`-submodule spanned by `(fun x => x -ᵥ p) '' (s \ {p})`.
More concisely: For any set `s` of elements in a `k`-module `V` with an additive commutative group structure, the vector span of `s` is equal to the span of the set of differences `s\_i - p` for all `s\_i` in `s` but not equal to a fixed `p` in `s`.
|
smul_vsub_vadd_mem_affineSpan_pair
theorem smul_vsub_vadd_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ affineSpan k {p₁, p₂}
The theorem `smul_vsub_vadd_mem_affineSpan_pair` states that for any ring `k`, any additive commutative group `V`, any `k`-module `V`, any add-torsor `V` over `P`, and any scalar `r` in `k` and points `p₁` and `p₂` in `P`, the result of adding the first point `p₁` to the scalar multiplication of `r` and the vector from `p₁` to `p₂` lies in the affine span of the set containing `p₁` and `p₂`. In mathematical terms, this corresponds to saying that for any scalar `r` and points `p₁` and `p₂`, the point `r(p₂ - p₁) + p₁` is in the smallest affine subspace that contains `p₁` and `p₂`.
More concisely: For any ring `k`, additive commutative group `V`, `k`-module `V`, add-torsor `V` over `P`, and scalars `r` in `k` and points `p₁, p₂` in `P`, the point `r(p₂ - p₁) + p₁` lies in the affine span of `{p₁, p₂}`.
|
AffineSubspace.vadd_mem_mk'
theorem AffineSubspace.vadd_mem_mk' :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {v : V} (p : P) {direction : Submodule k V},
v ∈ direction → v +ᵥ p ∈ AffineSubspace.mk' p direction
The theorem `AffineSubspace.vadd_mem_mk'` states that for any type `k` with ring structure, type `V` with additive commutative group structure, and type `P` as an affine torsor over `V`, given a vector `v` of type `V`, a point `p` of type `P`, and a direction which is a submodule of `V`, if `v` is in the direction, then the result of adding `v` to `p` (denoted by `v +ᵥ p`) is in the affine subspace constructed from point `p` and the direction. This theorem essentially ensures that an affine subspace includes all points that can be reached from a specific point by adding a vector from a certain direction.
More concisely: If `v` is in the submodule `direction` of a vector space `V`, then `v + p` is in the affine subspace `��ssub V p direction`.
|
AffineSubspace.mem_mk'_iff_vsub_mem
theorem AffineSubspace.mem_mk'_iff_vsub_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ : P} {direction : Submodule k V},
p₂ ∈ AffineSubspace.mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction
The theorem `AffineSubspace.mem_mk'_iff_vsub_mem` states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, given two points `p₁` and `p₂` of type `P`, and a direction which is a submodule of `V` over `k`, the point `p₂` lies in the affine subspace constructed from the point `p₁` and the direction if and only if the vector formed by the difference `p₂ -ᵥ p₁` is in the given direction.
More concisely: For any ring `k`, additive commutative group `V`, module `V` over `k`, additive torsor `P` over `V`, points `p₁, p₂` in `P`, and submodule `d` of `V` over `k`, the point `p₂` lies in the affine subspace spanned by `p₁` and `d` if and only if `p₂ - p₁` is in `d`.
|
vectorSpan_eq_span_vsub_finset_right_ne
theorem vectorSpan_eq_span_vsub_finset_right_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] [inst_5 : DecidableEq V] {s : Finset P} {p : P},
p ∈ s → vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun x => x -ᵥ p) (s.erase p))
This theorem states that, for a given type `k` and its associated structures and properties (`Ring k`, `AddCommGroup V`, `Module k V`, `AddTorsor V P`), along with a given `Finset` of elements of type `P` and a specific point `p` of type `P` within that set, the `vectorSpan` of the original set is equal to the `Submodule.span` of the set obtained by subtracting the specific point `p` from every other point in the set (excluding the subtraction of `p` from itself). In other words, the vector span of a set of points is the submodule span of the set of all pairwise differences with a given point on the right, excluding the difference of the point with itself. This theorem thus provides a relationship between two different ways of constructing subspaces from a set of points.
More concisely: For a given type `k`, set `P` of points in the `AddTorsor` `V P`, and point `p` in `P`, the submodule `Submodule.span {x : P | x ≠ p} (x - p)` is equal to the vector space span of `{p} ∪ {x : P | x ≠ p}`.
|
AffineSubspace.coe_injective
theorem AffineSubspace.coe_injective :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P], Function.Injective SetLike.coe
The theorem `AffineSubspace.coe_injective` states that two affine subspaces are considered equal if and only if they contain the same points. This applies for any field `k`, any additive commutative group `V`, and any affine space `P` over that group with scalar multiplication by elements of `k`. The theorem relies on the property of the injectiveness of the `SetLike.coe` function, which means that distinct affine subspaces map to distinct sets of points, thereby ensuring that the same set of points can only come from one affine subspace.
More concisely: Two affine subspaces of an affine space over a field with the same set of points are equal.
|
AffineSubspace.coe_direction_eq_vsub_set_left
theorem AffineSubspace.coe_direction_eq_vsub_set_left :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ↑s.direction = (fun x => p -ᵥ x) '' ↑s
This theorem states that given a point `p` in an affine subspace `s`, the set of all vectors in the direction of this subspace (`s.direction`) is equivalent to the set of all vectors obtained by subtracting each point in the subspace from `p`. This holds for any ring `k`, additive commutative group `V`, module over `k` on `V`, and an additive torsor of `V` over a type `P`.
More concisely: Given an affine subspace `s` in an additive commutative group `V` over a ring `k`, the set of vectors in the direction of `s` is equivalent to the set of vectors obtained by subtracting any point `p` in `s` from other points in `s`.
|
vectorSpan_pair
theorem vectorSpan_pair :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p₁ p₂ : P), vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}
The theorem `vectorSpan_pair` states that for any ring `k`, additive commutative group `V`, module `k V`, and additive torsor `V P`, and for any two points `p₁` and `p₂` from set `P`, the vector span of set `{p₁, p₂}` is equal to the submodule span of the set containing the difference of `p₁` and `p₂`. This means that the smallest submodule that contains the differences of the points `p₁` and `p₂` is the same as the submodule generated by the single difference `p₁ -ᵥ p₂`.
More concisely: For any additive commutative group V, module over a ring k, and additive torsor P, the vector span of two points p₁ and p₂ in P equals the submodule span of {p₁ - p₂}.
|
AffineSubspace.vsub_mem_direction
theorem AffineSubspace.vsub_mem_direction :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p1 p2 : P}, p1 ∈ s → p2 ∈ s → p1 -ᵥ p2 ∈ s.direction
The theorem `AffineSubspace.vsub_mem_direction` states that for any ring `k`, any additively commutative group `V`, any module `V` over `k`, any torsor `P` over `V`, and any affine subspace `s` of `P` with respect to `k`, if `p1` and `p2` are any two points in the subspace `s`, then the subtracted vector `p1 -ᵥ p2` will always be a member of the direction of the subspace `s`. Here, the direction of an affine subspace is defined as the submodule spanned by the pairwise differences of points in the subspace.
More concisely: For any ring `k`, additively commutative group `V`, module `V` over `k`, torsor `P` over `V`, and affine subspace `s` of `P` with respect to `k`, if `p1` and `p2` are in `s`, then `p1 - p2` lies in the submodule spanned by the differences of points in `s`.
|
AffineSubspace.direction_le
theorem AffineSubspace.direction_le :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s1 s2 : AffineSubspace k P}, s1 ≤ s2 → s1.direction ≤ s2.direction
The theorem `AffineSubspace.direction_le` states that for any types `k`, `V`, and `P`, where `k` is a ring, `V` is an additive commutative group, `V` is a `k`-module, and `P` is an affine space over `V`, if we have two affine subspaces `s1` and `s2` of `P` such that `s1` is a subset of `s2` (denoted by `s1 ≤ s2`), then the direction of `s1` is also a subset of the direction of `s2`. In other words, if one affine subspace is contained within another, any vector that can be expressed as a difference of two points in the smaller subspace can also be expressed as a difference of two points in the larger subspace. The term "direction" of an affine subspace refers to the subspace of the vector space spanned by the differences of pairs of points in the affine subspace.
More concisely: If `s1` is a subset of `s2` in the affine spaces `P` over a `k`-module `V`, then the direction of `s1` is contained in the direction of `s2`.
|
affineSpan_le_toAffineSubspace_span
theorem affineSpan_le_toAffineSubspace_span :
∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : Set V},
affineSpan k s ≤ (Submodule.span k s).toAffineSubspace
The theorem `affineSpan_le_toAffineSubspace_span` states that for any set `s` of elements in a vector type `V` over a ring `k`, the affine span of `s` (which is the smallest affine subspace that contains `s`) is a subset of the affine subspace corresponding to the linear span of `s` (which is the smallest linear subspace that contains `s`). This is under the condition that the affine space is also a vector space, which is implied by the structures `Ring k`, `AddCommGroup V`, and `Module k V`.
More concisely: The affine span of a set in a vector space is contained in the affine subspace spanned by its linear span.
|
AffineSubspace.map_direction
theorem AffineSubspace.map_direction :
∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [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 : AffineSubspace k P₁),
(AffineSubspace.map f s).direction = Submodule.map f.linear s.direction
The theorem `AffineSubspace.map_direction` states that for any ring `k`, additively commutative group `V₁` and `V₂`, module `V₁` and `V₂` over `k`, affine torsors `P₁` over `V₁` and `P₂` over `V₂`, and an affine map `f` from `P₁` to `P₂`, when an affine subspace `s` of `P₁` is mapped to `P₂` using `f`, the direction of the resulting subspace is equal to the image of the direction of the original subspace `s` under the linear part of the affine map `f`. In other words, if you take an affine subspace, map it via an affine map, the direction of the new subspace is just the direction of the original subspace transformed by the linear part of the affine map.
More concisely: Given an affine map between affine torsors, the image of an affine subspace under the map has direction equal to the linear part of the map times the direction of the original subspace.
|
AffineSubspace.direction_inf_of_mem
theorem AffineSubspace.direction_inf_of_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p : P},
p ∈ s₁ → p ∈ s₂ → (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction
This theorem states that, given two affine subspaces `s₁` and `s₂` in a module over a ring `k` and with an associated affine space `P`, if they have a common point `p`, the direction of the intersection of these subspaces is equal to the intersection of their directions. This result holds for any ring `k`, any additive commutative group `V`, and any module `k V`, and any affine torsor `V P`.
More concisely: Given affine subspaces $s\_1$ and $s\_2$ in a module $V$ over a ring $k$ with associated affine space $P$, if they have a common point $p$, then their directions intersect to form the direction of their intersection.
|
AffineSubspace.nonempty_of_affineSpan_eq_top
theorem AffineSubspace.nonempty_of_affineSpan_eq_top :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s : Set P}, affineSpan k s = ⊤ → s.Nonempty
This theorem states that for any ring `k`, additive commutative group `V`, and set `P` with `V` acting on `P` as an additive torsor, if the affine span of a set `s` of points in `P` equals the entire space (`⊤`), then the set `s` is not empty. In other words, the smallest affine subspace that contains all points cannot be the entire space unless there is at least one point in the set.
More concisely: If a set `s` of points in an additive torsor `P` over an additive commutative group `V` with action by a ring `k` has the property that the affine span of `s` equals the entire space `V`, then `s` is non-empty.
|
AffineSubspace.mk'_nonempty
theorem AffineSubspace.mk'_nonempty :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P) (direction : Submodule k V), (↑(AffineSubspace.mk' p direction)).Nonempty
The theorem `AffineSubspace.mk'_nonempty` states that for any point `p` and any direction `direction`, the affine subspace that is constructed from this point and direction is nonempty. This applies in the context where `k` is a ring, `V` is a group under addition and `P` is an affine space over `V` with `k` as the underlying field. The term "nonempty" means that there is at least one point in the affine subspace.
More concisely: Given a ring `k`, a group `V` under addition, and an affine space `P` over `V` with underlying field `k`, for every point `p` in `P` and direction `direction` in `V`, the affine subspace spanned by `p` and `direction` is non-empty.
|
AffineMap.lineMap_mem_affineSpan_pair
theorem AffineMap.lineMap_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), (AffineMap.lineMap p₁ p₂) r ∈ affineSpan k {p₁, p₂}
The theorem `AffineMap.lineMap_mem_affineSpan_pair` states that, for any ring `k`, commutative group `V`, generic type `P`, and any points `p₁` and `p₂` of type `P`, the image of any scalar `r` of `k` under the affine map `lineMap` from `k` to `P` with `p₁` as the "start" point and `p₂` as the "end" point always lies within the affine span of the set `{p₁, p₂}`. In other words, any point that can be obtained by linearly interpolating between `p₁` and `p₂` is contained in the smallest affine subspace that contains both `p₁` and `p₂`.
More concisely: For any ring `k`, commutative group `V`, and points `p₁, p₂` in `V`, the image of any scalar `r` under the affine map `lineMap` from `k` to `V` with `p₁` as the starting point and `p₂` as the ending point lies in the affine span of `{p₁, p₂}`.
|
vectorSpan_pair_rev
theorem vectorSpan_pair_rev :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p₁ p₂ : P), vectorSpan k {p₁, p₂} = Submodule.span k {p₂ -ᵥ p₁}
The theorem `vectorSpan_pair_rev` states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, and for any two points `p₁` and `p₂` in `P`, the vector span (i.e. the submodule generated by the differences) of the set containing `p₁` and `p₂` is equal to the submodule spanned (i.e. the smallest submodule containing) by the set containing the difference `p₂ -ᵥ p₁`. In simpler terms, the space generated by the vectors pointing from `p₁` to `p₂` is the same as the space generated by the single vector pointing from `p₂` to `p₁`.
More concisely: For any additive torsor P over an additive commutative group V as a module over a ring k, the submodule generated by {p₁, p₂} in P equals the submodule generated by {p₂ - p₁} in P.
|
mem_affineSpan
theorem mem_affineSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p : P} {s : Set P}, p ∈ s → p ∈ affineSpan k s
The theorem `mem_affineSpan` states that for any point `p` within a set `s` of type `P`, and given the conditions that `k` is a Ring, `V` is an Additive Commutative Group, `V` is a Module over `k`, and `P` is an Additive Torsor over `V`, the point `p` also belongs to the affine span of the set `s`. In other terms, any point in a set is also in the smallest affine subspace (affine span) that contains all points of that set.
More concisely: Given a set `s` of points in an Additive Torsor `P` over a Ring `k`, such that `P` is an Additive Commutative Group and a Module over `k`, every point `p` in `s` lies in the affine span of `s`.
|
right_mem_affineSpan_pair
theorem right_mem_affineSpan_pair :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p₁ p₂ : P), p₂ ∈ affineSpan k {p₁, p₂}
The theorem `right_mem_affineSpan_pair` states that, for any field `k`, if `P` is a space of points with an associated vector space `V` (where `V` is a module over `k` and `P` is an affine space for `V`), and if `p₁` and `p₂` are any two points in `P`, then `p₂` is contained in the affine span of the set `{p₁, p₂}`. In other words, the second of two points always lies within the smallest affine subspace containing both of these points.
More concisely: For any affine space $P$ over a field $k$ and any two points $p\_1, p\_2 \in P$, $p\_2$ lies in the affine span of $\{p\_1, p\_2\}$.
|
vectorSpan_image_eq_span_vsub_set_left_ne
theorem vectorSpan_image_eq_span_vsub_set_left_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) {s : Set ι} {i : ι},
i ∈ s → vectorSpan k (p '' s) = Submodule.span k ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))
The theorem `vectorSpan_image_eq_span_vsub_set_left_ne` states that for any ring `k`, additive commutative group `V`, module `k V`, and additive torsor `V P`, along with a function `p` that maps an index set `ι` to a point set `P`, a subset `s` of the index set `ι`, and an element `i` of the index set `ι` that is in the subset `s`, the `vectorSpan` of the image of the function `p` over the subset `s` is equal to the submodule spanned by the set of all pairwise differences obtained by subtracting each image of the function `p` over the subset `s`, excluding the element `i`, from the image of `i`. In mathematical terms, this can be expressed as the vector span of $p(s)$ is equal to the span of the set of all $(p(i) - x)$ for all $x \in p(s \ {i})$.
More concisely: For any additive torsor V over a commutative ring k, and a function p from an index set ι to V, the vector span of the images of p over a subset s of ι equals the submodule spanned by the differences between the image of i in s and the images of all other elements in s.
|
AffineSubspace.direction_top
theorem AffineSubspace.direction_top :
∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P], ⊤.direction = ⊤
The theorem `AffineSubspace.direction_top` states that for any ring `k`, additive commutative group `V`, and the torsor `P` over `V`, the direction of the top (`⊤`) affine subspace is the entire module as a submodule. In other words, the set of all pairwise differences of points in the top affine subspace, also known as its direction, covers the whole vector space `V`.
More concisely: For any additive commutative group `V` with a ring structure `k`, and a torsor `P` over `V`, the direction of the top affine subspace `P` is the entire module `V` as a submodule of `k≃V`.
|
AffineSubspace.exists_of_lt
theorem AffineSubspace.exists_of_lt :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s1 s2 : AffineSubspace k P}, s1 < s2 → ∃ p ∈ s2, p ∉ s1
This theorem states that if one affine subspace is strictly contained in another (denoted by `s1 < s2`), then there exists at least one point that belongs exclusively to the larger subspace (`s2`), but not to the smaller one (`s1`). The function takes as input the field `k`, the vector space `V`, the affine space `P`, and two affine subspaces `s1` and `s2`. The context requires `k` to be a ring, `V` to be an additive commutative group, and `V` to be a module over `k`. Additionally, an affine torsor structure over `V` and `P` is required.
More concisely: If `s1` is a proper affine subspace of `s2` in an affine space `P` over a field `k`, then there exists a point in `s2` not in `s1`.
|
AffineSubspace.mem_affineSpan_insert_iff
theorem AffineSubspace.mem_affineSpan_insert_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p1 : P},
p1 ∈ s → ∀ (p2 p : P), p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p2 -ᵥ p1) +ᵥ p0
This theorem states that for a given point `p1` in an affine subspace `s`, and another point `p2`, a point `p` belongs to the affine span of the subspace `s` with `p2` included if and only if `p` can be represented as a scalar multiplication of the vector difference `p2 -ᵥ p1` added to a point `p0` in subspace `s`. The scalar multiplier `r` and the point `p0` in `s` are not fixed and can be any real number and any point in `s` respectively. This is essentially giving us the condition required for a point `p` to lie in the specific affine span.
More concisely: A point p belongs to the affine span of a subspace s with point p2 included if and only if there exist a scalar r and a point p0 in s such that p = p0 + r *(p2 - p1), where p1 is a given point in s.
|
affineSpan_insert_affineSpan
theorem affineSpan_insert_affineSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P) (ps : Set P),
affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)
This theorem states that in the context of a ring `k`, an additive commutative group `V`, and an additive torsor `V P`, for any point `p` and any set of points `ps`, taking the affine span of `ps`, then inserting `p`, and taking the affine span again, is the same as first inserting `p` into `ps`, and then taking the affine span. Essentially, the order of inserting a point and taking the affine span does not affect the final result. This property is important for the manipulation and understanding of geometric and vector spaces in mathematics.
More concisely: In the context of a ring `k`, an additive commutative group `V`, and an additive torsor `V/P`, the affine span of `P ∪ {p}` is equal to the affine span of `P` followed by the affine span of `{p}`.
|
affineSpan_singleton_union_vadd_eq_top_of_span_eq_top
theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set V} (p : P),
Submodule.span k (Set.range Subtype.val) = ⊤ → affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s) = ⊤
This theorem states that for a given set of vectors `s` that span a vector space `V`, and a given point `p` in an affine space `P` over `V`, if the span of the set of vectors derived from the underlying elements of `s` is the entire space `V`, then the affine span of the set containing `p` and the set of vectors in `s` after each has been added to `p`, is the entire affine space `P`. The operators involved are `Submodule.span`, which gives the smallest subspace containing a set, `Set.range`, which gives the image of a function, `Subtype.val` which gives the underlying element of a subtype, and `affineSpan`, which gives the smallest affine subspace containing a set. This theorem can be crucial in studies involving affine spaces and their relation with corresponding vector spaces.
More concisely: If the span of a set of vectors `s` in a vector space `V` equals `V`, then the affine span of `p` and the set of `p` plus each vector in `s` equals the entire affine space `P` over `V`.
|
AffineSubspace.self_mem_mk'
theorem AffineSubspace.self_mem_mk' :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P) (direction : Submodule k V), p ∈ AffineSubspace.mk' p direction
This theorem states that for any point `p` and any direction given by a submodule of a vector space `V` over a ring `k`, the affine subspace constructed from the point `p` and this direction always contains the point `p`. This applies in the context where `k` is a ring, `V` is a commutative additive group, `V` is a module over `k`, and `V` is an additive torsor for the point type `P`.
More concisely: Given a point `p` and a submodule `d` of a vector space `V` over a ring `k`, the affine subspace of `V` determined by `p` and `d` contains `p`.
|
AffineSubspace.mem_direction_iff_eq_vsub_right
theorem AffineSubspace.mem_direction_iff_eq_vsub_right :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P},
p ∈ s → ∀ (v : V), v ∈ s.direction ↔ ∃ p2 ∈ s, v = p2 -ᵥ p
This theorem states that for any given point belonging to an affine subspace, a vector is in the direction of this subspace if and only if this vector can be represented as the result of subtracting the given point from another point in the subspace. The theorem is applicable in the context of a ring, an additive commutative group, and a module over the ring. Furthermore, the underlying space is an additive torsor, a mathematical structure that generalizes vector spaces and affine spaces.
More concisely: A vector is in the direction of an affine subspace if and only if it is the difference of two points in the subspace.
|
AffineSubspace.mem_affineSpan_singleton
theorem AffineSubspace.mem_affineSpan_singleton :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {p₁ p₂ : P}, p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂
This theorem states that a point is in the affine span of a single point if and only if the two points are equal. In a mathematical context, an affine span is the smallest affine subspace that contains a particular set of points. Therefore, the affine span of a single point is just that point itself. Hence, in the context of a ring `k`, an additive commutative group `V`, a module `k V`, and an additive torsor `V P`, for any two points `p₁` and `p₂` of `P`, `p₁` is in the affine span of `{p₂}` only when `p₁` and `p₂` are the same point.
More concisely: A point is in the affine span of a single point if and only if that point is equal to the given point.
|
AffineSubspace.ext_of_direction_eq
theorem AffineSubspace.ext_of_direction_eq :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s1 s2 : AffineSubspace k P},
s1.direction = s2.direction → (↑s1 ∩ ↑s2).Nonempty → s1 = s2
The theorem `AffineSubspace.ext_of_direction_eq` states that for any ring `k`, additive commutative group `V`, and add-torsor `V P`, if we have two affine subspaces `s1` and `s2` of `k P`, and the direction of `s1` is equal to the direction of `s2`, then if the intersection of `s1` and `s2` is non-empty, `s1` and `s2` must be the same affine subspace. In simple terms, two affine subspaces are equal if they point in the same direction and they share at least one common point.
More concisely: If two affine subspaces of a ring with additive commutative group have equal directions and non-empty intersection, then they are equal.
|
vectorSpan_insert_eq_vectorSpan
theorem vectorSpan_insert_eq_vectorSpan :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p : P} {ps : Set P},
p ∈ affineSpan k ps → vectorSpan k (insert p ps) = vectorSpan k ps
This theorem states that for any point `p` and any set `ps` of points, if `p` is within the affine span of `ps`, then the vector span of the set formed by inserting `p` into `ps` is the same as the original vector span of `ps`. Here, the affine span of a set of points is defined as the smallest affine subspace containing those points, while the vector span of a set of points is defined as the submodule spanning the differences of that set of points. The theorem is abstract over any type `k` forming a ring, any type `V` forming an additive commutative group and any type `P` that forms an affine torsor over `V` with scalar multiplication from `k`.
More concisely: If a point is in the affine hull of a set, then adding that point to the set does not change the vector span.
|
AffineSubspace.spanPoints_subset_coe_of_subset_coe
theorem AffineSubspace.spanPoints_subset_coe_of_subset_coe :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {s1 : AffineSubspace k P}, s ⊆ ↑s1 → spanPoints k s ⊆ ↑s1
The theorem `AffineSubspace.spanPoints_subset_coe_of_subset_coe` states that given a ring `k`, an additive commutative group `V`, a module `V` over the ring `k`, a torsor `P` for the group `V`, a set of points `s` in `P`, and an affine subspace `s1` of `P` over `k`, if the set `s` is a subset of the underlying set of `s1` (denoted `↑s1`), then the affine span of `s` (the set of all points which can be expressed as a vector in the vector span of `s`, shifted by a point in `s`) is also a subset of the underlying set of `s1`. In other words, if an affine subspace contains a set of points, it also contains all points in the affine span of that set.
More concisely: If `s` is a subset of an affine subspace `s1` of a module `V` over a ring `k`, then the affine span of `s` is contained in the underlying set of `s1`.
|
affineSpan_le
theorem affineSpan_le :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s : Set P} {Q : AffineSubspace k P}, affineSpan k s ≤ Q ↔ s ⊆ ↑Q
This theorem states that for all types `k`, `V`, and `P` in which `k` is a ring, `V` is an additive commutative group, and `V` is a `k`-module, and for all `s` which is a set of type `P` and `Q` which is an affine subspace of `P` over the ring `k`, the affine span of `s` is a subset of `Q` if and only if `s` is a subset of the carrier of `Q`. This theorem is about the relationship between the affine span of a set of points and a given affine subspace, and it provides a condition under which the set of points is contained within the affine subspace.
More concisely: For a ring `k`, an additive commutative group `V` that is a `k`-module, a set `s` of type `P` in `V`, and an affine subspace `Q` of `P` over `k`, the affine span of `s` is contained in `Q` if and only if `s` is a subset of the carrier of `Q`.
|
vectorSpan_range_eq_span_range_vsub_right_ne
theorem vectorSpan_range_eq_span_range_vsub_right_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i₀ : ι),
vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p ↑i -ᵥ p i₀)
The theorem `vectorSpan_range_eq_span_range_vsub_right_ne` states that for a given indexed family of points `p : ι → P` in an additive torsor `P` over an additive commutative group `V` that's a module over a ring `k`, and a selected index `i₀ : ι`, the `vectorSpan` of the range of `p` (which is the submodule spanned by the differences of all pairs of points in the range of `p`) is equal to the submodule spanned by all vectors obtained by subtracting the point corresponding to `i₀` from each point in the range of `p`, excluding the zero vector obtained by subtracting the point from itself.
More concisely: The theorem asserts that the submodule spanned by differences of points in an indexed family, excluding the difference of a fixed index and itself, is equal to the vector span of that family in an additive torsor over a commutative ring.
|
AffineSubspace.direction_inf
theorem AffineSubspace.direction_inf :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (s1 s2 : AffineSubspace k P), (s1 ⊓ s2).direction ≤ s1.direction ⊓ s2.direction
The theorem `AffineSubspace.direction_inf` says that for any ring `k`, an additive commutative group `V`, a module of `k` over `V`, an additive torsor `S` of `V` over `P`, and any two affine subspaces `s1` and `s2` of `k` over `P`, the direction (vector subspace) of the intersection of `s1` and `s2` is a subspace of the intersection of the directions of `s1` and `s2`. In other words, the vector subspace defined by the intersection of two affine subspaces is contained within the intersection of the vector subspaces defined by each affine subspace individually.
More concisely: The theorem asserts that the direction vector subspace of the intersection of two affine subspaces is contained within the intersection of their respective direction vector subspaces.
|
AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty
theorem AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s1 s2 : AffineSubspace k P},
(↑s1).Nonempty → (↑s2).Nonempty → ↑s1 ∩ ↑s2 = ∅ → s1.direction ⊔ s2.direction < (s1 ⊔ s2).direction
The theorem `AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty` states that for any two nonempty affine subspaces `s1` and `s2` in a module over a ring, if the intersection of `s1` and `s2` is empty, then the supremum (sup) of the directions of `s1` and `s2` is less than the direction of the supremum of `s1` and `s2`. In other words, the combined direction of two non-intersecting subspaces is always less than the direction of the subspace formed by their union.
More concisely: For any two nonempty affine subspaces in a module over a ring, if their intersection is empty then the direction of their union is strictly less than the directions of each subspace.
|
AffineSubspace.direction_sup
theorem AffineSubspace.direction_sup :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s1 s2 : AffineSubspace k P} {p1 p2 : P},
p1 ∈ s1 → p2 ∈ s2 → (s1 ⊔ s2).direction = s1.direction ⊔ s2.direction ⊔ Submodule.span k {p2 -ᵥ p1}
This theorem states that for any field `k`, any additive commutative group `V`, any module `V` over `k`, any add-torsor `P` over `V`, any two affine subspaces `s1` and `s2` of `P`, and for any two points `p1` and `p2` in `s1` and `s2` respectively, the direction of the sup (supremum or least upper bound) of `s1` and `s2` is equal to the sup of the directions of `s1` and `s2` and the span in `k` of the singleton set containing the difference `p2 -ᵥ p1`. Essentially, it describes how the direction of the combination of two affine subspaces is determined by the directions of the individual subspaces and the difference between one point in each subspace.
More concisely: Given a field `k`, an additive commutative group `V`, an `k`-module `V`, an add-torsor `P` over `V`, two affine subspaces `s1` and `s2` of `P`, and points `p1 ∈ s1` and `p2 ∈ s2`, the direction of the sup of `s1` and `s2` is equal to the sup of their directions and the span of `p2 - p1` in `k`.
|
AffineSubspace.mem_direction_iff_eq_vsub_left
theorem AffineSubspace.mem_direction_iff_eq_vsub_left :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P},
p ∈ s → ∀ (v : V), v ∈ s.direction ↔ ∃ p2 ∈ s, v = p -ᵥ p2
This theorem states that for any given point within an affine subspace, a vector is considered to be in the direction of this subspace if and only if it can be obtained by subtracting the given point from another point within the same subspace. This holds for subspaces within any module over a ring, where the module operations comply with the rules of an additive abelian group and the ring operations obey the rules of a field.
More concisely: Given a point and any two points in an affine subspace of a module over a ring with additive and multiative identities and field properties, the vector obtained by subtracting the first point from the second lies in the subspace's direction if and only if it is the direction vector itself.
|
affineSpan_pair_le_of_left_mem
theorem affineSpan_pair_le_of_left_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P},
p₁ ∈ affineSpan k {p₂, p₃} → affineSpan k {p₁, p₃} ≤ affineSpan k {p₂, p₃}
This theorem states that for any ring `k`, additive commutative group `V`, and point type `P` equipped with the module structure over `k` and an additive torsor structure, and for any three points `p₁`, `p₂`, and `p₃`, if `p₁` is in the affine span of the set `{p₂, p₃}`, then the affine span of the set `{p₁, p₃}` is contained within the affine span of the set `{p₂, p₃}`. In other words, one line can be contained in another line that differs only in the first point, if the first point of the first line is contained in the second line.
More concisely: Given a ring `k`, an additive commutative group `V` with a module structure over `k`, an additive torsor structure, and three points `p₁`, `p₂`, `p₃` in `V` such that `p₁` is in the affine span of `{p₂, p₃}`, then `p₁` is in the affine span of `{p₂, p₃}` implies that the affine span of `{p₁, p₃}` is contained in the affine span of `{p₂, p₃}`.
|
affineSpan_eq_bot
theorem affineSpan_eq_bot :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P}, affineSpan k s = ⊥ ↔ s = ∅
This theorem states that, for any ring `k`, any additive commutative group `V`, any module over `k` on `V`, any torsor `P` for `V`, and any set `s` of points in `P`, the affine span of `s` is the bottom element (i.e., the smallest affine subspace) if and only if `s` is the empty set. In other words, the smallest subspace that contains a set of points is the bottom element precisely when that set of points is empty.
More concisely: For any ring `k`, any additive commutative group `V`, any `k`-module `M` on `V`, and any set `s` of points in any torsor `P` of `M` over `V`, the affine span of `s` is the zero subspace if and only if `s` is empty.
|
AffineSubspace.preimage_coe_affineSpan_singleton
theorem AffineSubspace.preimage_coe_affineSpan_singleton :
∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] (x : P), Subtype.val ⁻¹' {x} = Set.univ
This theorem, `AffineSubspace.preimage_coe_affineSpan_singleton`, states that for any type `k` with a ring structure, a type `V` with an additive commutative group structure and a `k`-module structure, a type `P` that forms an additive torsor over `V`, and an element `x` of type `P`, the preimage under the function `Subtype.val` of the singleton set containing `x` is equal to the universal set. In simple terms, this theorem asserts that for all elements in our space, when we map them using `Subtype.val`, every element of our space will map to a singleton set `{x}`, implying that the entire space is covered by this preimage operation.
More concisely: For any additive torsor P over a k-module V with a ring K, and any x in P, the preimage under Subtype.val of the singleton {x} equals the entire space V.
|