mathlib3 documentation

linear_algebra.affine_space.affine_subspace

Affine spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines affine subspaces (over modules) and the affine span of a set of points.

Main definitions #

Implementation notes #

out_param is used in the definiton of add_torsor V P to make V an implicit argument (deduced from P) in most cases; include V is needed in many cases for V, and type classes using it, to be added as implicit arguments to individual lemmas. As for modules, k is an explicit argument rather than implied by P or V.

This file only provides purely algebraic definitions and results. Those depending on analysis or topology are defined elsewhere; see analysis.normed_space.add_torsor and topology.algebra.affine.

References #

source
def vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
submodule k V

The submodule spanning the differences of a (possibly empty) set of points.

Equations
Instances for ↥vector_span
source
theorem vector_span_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
vector_span k s = submodule.span k (s -ᵥ s)

The definition of vector_span, for rewriting.

source
theorem vector_span_mono (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : set P} (h : s₁ ⊆ s₂) :
vector_span k s₁ ≤ vector_span k s₂

vector_span is monotone.

source
@[simp]
theorem vector_span_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [add_torsor V P] :
vector_span k ∅ = ⊥

The vector_span of the empty set is ⊥.

source
@[simp]
theorem vector_span_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) :
vector_span k {p} = ⊥

The vector_span of a single point is ⊥.

source
theorem vsub_set_subset_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
s -ᵥ s ⊆ ↑(vector_span k s)

The s -ᵥ s lies within the vector_span k s.

source
theorem vsub_mem_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p1 p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) :
p1 -ᵥ p2 ∈ vector_span k s

Each pairwise difference is in the vector_span.

source
def span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
set P

The points in the affine span of a (possibly empty) set of points. Use affine_span instead to get an affine_subspace k P.

Equations
source
theorem mem_span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) (s : set P) :
p ∈ s → p ∈ span_points k s

A point in a set is in its affine span.

source
theorem subset_span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
s ⊆ span_points k s

A set is contained in its span_points.

source
@[simp]
theorem span_points_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
(span_points k s).nonempty ↔ s.nonempty

The span_points of a set is nonempty if and only if that set is.

source
theorem vadd_mem_span_points_of_mem_span_points_of_mem_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : P} {v : V} (hp : p ∈ span_points k s) (hv : v ∈ vector_span k s) :
v +ᵥ p ∈ span_points k s

Adding a point in the affine span and a vector in the spanning submodule produces a point in the affine span.

source
theorem vsub_mem_vector_span_of_mem_span_points_of_mem_span_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p1 p2 : P} (hp1 : p1 ∈ span_points k s) (hp2 : p2 ∈ span_points k s) :
p1 -ᵥ p2 ∈ vector_span k s

Subtracting two points in the affine span produces a vector in the spanning submodule.

source
structure affine_subspace (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [add_torsor V P] :
Type u_3

An affine_subspace k P is a subset of an affine_space V P that, if not empty, has an affine space structure induced by a corresponding subspace of the module k V.

Instances for affine_subspace
source
def submodule.to_affine_subspace {k : Type u_1} {V : Type u_2} [ring k] [add_comm_group V] [module k V] (p : submodule k V) :
affine_subspace k V

Reinterpret p : submodule k V as an affine_subspace k V.

Equations
source
@[protected, instance]
def affine_subspace.set_like (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [add_torsor V P] :
set_like (affine_subspace k P) P
Equations
source
@[simp]
theorem affine_subspace.mem_coe (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) (s : affine_subspace k P) :
p ∈ ↑s ↔ p ∈ s

A point is in an affine subspace coerced to a set if and only if it is in that affine subspace.

source
def affine_subspace.direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) :
submodule k V

The direction of an affine subspace is the submodule spanned by the pairwise differences of points. (Except in the case of an empty affine subspace, where the direction is the zero submodule, every vector in the direction is the difference of two points in the affine subspace.)

Equations
Instances for ↥affine_subspace.direction
source
theorem affine_subspace.direction_eq_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) :
s.direction = vector_span k ↑s

The direction equals the vector_span.

source
def affine_subspace.direction_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} (h : ↑s.nonempty) :
submodule k V

Alternative definition of the direction when the affine subspace is nonempty. This is defined so that the order on submodules (as used in the definition of submodule.span) can be used in the proof of coe_direction_eq_vsub_set, and is not intended to be used beyond that proof.

Equations
source
theorem affine_subspace.direction_of_nonempty_eq_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} (h : ↑s.nonempty) :
affine_subspace.direction_of_nonempty h = s.direction

direction_of_nonempty gives the same submodule as direction.

source
theorem affine_subspace.coe_direction_eq_vsub_set {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} (h : ↑s.nonempty) :
↑(s.direction) = ↑s -ᵥ ↑s

The set of vectors in the direction of a nonempty affine subspace is given by vsub_set.

source
theorem affine_subspace.mem_direction_iff_eq_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} (h : ↑s.nonempty) (v : V) :
v ∈ s.direction ↔ ∃ (p1 : P) (H : p1 ∈ s) (p2 : P) (H : p2 ∈ s), v = p1 -ᵥ p2

A vector is in the direction of a nonempty affine subspace if and only if it is the subtraction of two vectors in the subspace.

source
theorem affine_subspace.vadd_mem_of_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {v : V} (hv : v ∈ s.direction) {p : P} (hp : p ∈ s) :
v +ᵥ p ∈ s

Adding a vector in the direction to a point in the subspace produces a point in the subspace.

source
theorem affine_subspace.vsub_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p1 p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) :
p1 -ᵥ p2 ∈ s.direction

Subtracting two points in the subspace produces a vector in the direction.

source
theorem affine_subspace.vadd_mem_iff_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} (v : V) {p : P} (hp : p ∈ s) :
v +ᵥ p ∈ s ↔ v ∈ s.direction

Adding a vector to a point in a subspace produces a point in the subspace if and only if the vector is in the direction.

source
theorem affine_subspace.vadd_mem_iff_mem_of_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {v : V} (hv : v ∈ s.direction) {p : P} :
v +ᵥ p ∈ s ↔ p ∈ s

Adding a vector in the direction to a point produces a point in the subspace if and only if the original point is in the subspace.

source
theorem affine_subspace.coe_direction_eq_vsub_set_right {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p : P} (hp : p ∈ s) :
↑(s.direction) = (λ (_x : P), _x -ᵥ p) '' ↑s

Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the right.

source
theorem affine_subspace.coe_direction_eq_vsub_set_left {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p : P} (hp : p ∈ s) :
↑(s.direction) = has_vsub.vsub p '' ↑s

Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the left.

source
theorem affine_subspace.mem_direction_iff_eq_vsub_right {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p : P} (hp : p ∈ s) (v : V) :
v ∈ s.direction ↔ ∃ (p2 : P) (H : p2 ∈ s), v = p2 -ᵥ p

Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the right.

source
theorem affine_subspace.mem_direction_iff_eq_vsub_left {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p : P} (hp : p ∈ s) (v : V) :
v ∈ s.direction ↔ ∃ (p2 : P) (H : p2 ∈ s), v = p -ᵥ p2

Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the left.

source
theorem affine_subspace.vsub_right_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p : P} (hp : p ∈ s) (p2 : P) :
p2 -ᵥ p ∈ s.direction ↔ p2 ∈ s

Given a point in an affine subspace, a result of subtracting that point on the right is in the direction if and only if the other point is in the subspace.

source
theorem affine_subspace.vsub_left_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p : P} (hp : p ∈ s) (p2 : P) :
p -ᵥ p2 ∈ s.direction ↔ p2 ∈ s

Given a point in an affine subspace, a result of subtracting that point on the left is in the direction if and only if the other point is in the subspace.

source
theorem affine_subspace.coe_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] :
function.injective coe

Two affine subspaces are equal if they have the same points.

source
@[ext]
theorem affine_subspace.ext {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p q : affine_subspace k P} (h : ∀ (x : P), x ∈ p ↔ x ∈ q) :
p = q
source
@[simp]
theorem affine_subspace.ext_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s₁ s₂ : affine_subspace k P) :
↑s₁ = ↑s₂ ↔ s₁ = s₂
source
theorem affine_subspace.ext_of_direction_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s1 s2 : affine_subspace k P} (hd : s1.direction = s2.direction) (hn : (↑s1 ∩ ↑s2).nonempty) :
s1 = s2

Two affine subspaces with the same direction and nonempty intersection are equal.

source
@[reducible]
def affine_subspace.to_add_torsor {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] :
add_torsor ↥(s.direction) ↥s

This is not an instance because it loops with add_torsor.nonempty.

Equations
source
@[simp, norm_cast]
theorem affine_subspace.coe_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] (a b : ↥s) :
↑(a -ᵥ b) = ↑a -ᵥ ↑b
source
@[simp, norm_cast]
theorem affine_subspace.coe_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] (a : ↥(s.direction)) (b : ↥s) :
↑(a +ᵥ b) = ↑a +ᵥ ↑b
source
@[protected]
def affine_subspace.subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] :
↥s →ᵃ[k] P

Embedding of an affine subspace to the ambient space, as an affine map.

Equations
source
@[simp]
theorem affine_subspace.subtype_linear {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] :
s.subtype.linear = s.direction.subtype
source
theorem affine_subspace.subtype_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] (p : ↥s) :
⇑(s.subtype) p = ↑p
source
@[simp]
theorem affine_subspace.coe_subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] :
⇑(s.subtype) = coe
source
theorem affine_subspace.injective_subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [nonempty ↥s] :
function.injective ⇑(s.subtype)
source
theorem affine_subspace.eq_iff_direction_eq_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : affine_subspace k P} {p : P} (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) :
s₁ = s₂ ↔ s₁.direction = s₂.direction

Two affine subspaces with nonempty intersection are equal if and only if their directions are equal.

source
def affine_subspace.mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) (direction : submodule k V) :
affine_subspace k P

Construct an affine subspace from a point and a direction.

Equations
source
theorem affine_subspace.self_mem_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) (direction : submodule k V) :
p ∈ affine_subspace.mk' p direction

An affine subspace constructed from a point and a direction contains that point.

source
theorem affine_subspace.vadd_mem_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {v : V} (p : P) {direction : submodule k V} (hv : v ∈ direction) :
v +ᵥ p ∈ affine_subspace.mk' p direction

An affine subspace constructed from a point and a direction contains the result of adding a vector in that direction to that point.

source
theorem affine_subspace.mk'_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) (direction : submodule k V) :
↑(affine_subspace.mk' p direction).nonempty

An affine subspace constructed from a point and a direction is nonempty.

source
@[simp]
theorem affine_subspace.direction_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) (direction : submodule k V) :
(affine_subspace.mk' p direction).direction = direction

The direction of an affine subspace constructed from a point and a direction.

source
theorem affine_subspace.mem_mk'_iff_vsub_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ : P} {direction : submodule k V} :
p₂ ∈ affine_subspace.mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction

A point lies in an affine subspace constructed from another point and a direction if and only if their difference is in that direction.

source
@[simp]
theorem affine_subspace.mk'_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p : P} (hp : p ∈ s) :
affine_subspace.mk' p s.direction = s

Constructing an affine subspace from a point in a subspace and that subspace's direction yields the original subspace.

source
theorem affine_subspace.span_points_subset_coe_of_subset_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {s1 : affine_subspace k P} (h : s ⊆ ↑s1) :
span_points k s ⊆ ↑s1

If an affine subspace contains a set of points, it contains the span_points of that set.

source
theorem affine_map.line_map_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {Q : affine_subspace k P} {p₀ p₁ : P} (c : k) (h₀ : p₀ ∈ Q) (h₁ : p₁ ∈ Q) :
⇑(affine_map.line_map p₀ p₁) c ∈ Q
source
def affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
affine_subspace k P

The affine span of a set of points is the smallest affine subspace containing those points. (Actually defined here in terms of spans in modules.)

Equations
Instances for ↥affine_span
source
@[simp]
theorem coe_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
↑(affine_span k s) = span_points k s

The affine span, converted to a set, is span_points.

source
theorem subset_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
s ⊆ ↑(affine_span k s)

A set is contained in its affine span.

source
theorem direction_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
(affine_span k s).direction = vector_span k s

The direction of the affine span is the vector_span.

source
theorem mem_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : P} {s : set P} (hp : p ∈ s) :
p ∈ affine_span k s

A point in a set is in its affine span.

source
@[protected, instance]
def affine_subspace.complete_lattice {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
complete_lattice (affine_subspace k P)
Equations
source
@[protected, instance]
def affine_subspace.inhabited {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
inhabited (affine_subspace k P)
Equations
source
theorem affine_subspace.le_def {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
s1 ≤ s2 ↔ ↑s1 ⊆ ↑s2

The ≤ order on subspaces is the same as that on the corresponding sets.

source
theorem affine_subspace.le_def' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
s1 ≤ s2 ↔ ∀ (p : P), p ∈ s1 → p ∈ s2

One subspace is less than or equal to another if and only if all its points are in the second subspace.

source
theorem affine_subspace.lt_def {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
s1 < s2 ↔ ↑s1 ⊂ ↑s2

The < order on subspaces is the same as that on the corresponding sets.

source
theorem affine_subspace.not_le_iff_exists {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
¬s1 ≤ s2 ↔ ∃ (p : P) (H : p ∈ s1), p ∉ s2

One subspace is not less than or equal to another if and only if it has a point not in the second subspace.

source
theorem affine_subspace.exists_of_lt {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s1 s2 : affine_subspace k P} (h : s1 < s2) :
∃ (p : P) (H : p ∈ s2), p ∉ s1

If a subspace is less than another, there is a point only in the second.

source
theorem affine_subspace.lt_iff_le_and_exists {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
s1 < s2 ↔ s1 ≤ s2 ∧ ∃ (p : P) (H : p ∈ s2), p ∉ s1

A subspace is less than another if and only if it is less than or equal to the second subspace and there is a point only in the second.

source
theorem affine_subspace.eq_of_direction_eq_of_nonempty_of_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s₁ s₂ : affine_subspace k P} (hd : s₁.direction = s₂.direction) (hn : ↑s₁.nonempty) (hle : s₁ ≤ s₂) :
s₁ = s₂

If an affine subspace is nonempty and contained in another with the same direction, they are equal.

source
theorem affine_subspace.affine_span_eq_Inf (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s : set P) :
affine_span k s = has_Inf.Inf {s' : affine_subspace k P | s ⊆ ↑s'}

The affine span is the Inf of subspaces containing the given points.

source
@[protected]
def affine_subspace.gi (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
galois_insertion (affine_span k) coe

The Galois insertion formed by affine_span and coercion back to a set.

Equations
source
@[simp]
theorem affine_subspace.span_empty (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
affine_span k ∅ = ⊥

The span of the empty set is ⊥.

source
@[simp]
theorem affine_subspace.span_univ (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
affine_span k set.univ = ⊤

The span of univ is ⊤.

source
theorem affine_span_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : set P} {Q : affine_subspace k P} :
affine_span k s ≤ Q ↔ s ⊆ ↑Q
source
@[simp]
theorem affine_subspace.coe_affine_span_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (p : P) :
↑(affine_span k {p}) = {p}

The affine span of a single point, coerced to a set, contains just that point.

source
@[simp]
theorem affine_subspace.mem_affine_span_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {p₁ p₂ : P} :
p₁ ∈ affine_span k {p₂} ↔ p₁ = p₂

A point is in the affine span of a single point if and only if they are equal.

source
@[simp]
theorem affine_subspace.preimage_coe_affine_span_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (x : P) :
coe ⁻¹' {x} = set.univ
source
theorem affine_subspace.span_union (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s t : set P) :
affine_span k (s ∪ t) = affine_span k s ⊔ affine_span k t

The span of a union of sets is the sup of their spans.

source
theorem affine_subspace.span_Union (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {ι : Type u_4} (s : ι → set P) :
affine_span k (⋃ (i : ι), s i) = ⨆ (i : ι), affine_span k (s i)

The span of a union of an indexed family of sets is the sup of their spans.

source
@[simp]
theorem affine_subspace.top_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
↑⊤ = set.univ

⊤, coerced to a set, is the whole set of points.

source
theorem affine_subspace.mem_top (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (p : P) :
p ∈ ⊤

All points are in ⊤.

source
@[simp]
theorem affine_subspace.direction_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
⊤.direction = ⊤

The direction of ⊤ is the whole module as a submodule.

source
@[simp]
theorem affine_subspace.bot_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
↑⊥ = ∅

⊥, coerced to a set, is the empty set.

source
theorem affine_subspace.bot_ne_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
⊥ ≠ ⊤
source
@[protected, instance]
def affine_subspace.nontrivial (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
nontrivial (affine_subspace k P)
source
theorem affine_subspace.nonempty_of_affine_span_eq_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : set P} (h : affine_span k s = ⊤) :
s.nonempty
source
theorem affine_subspace.vector_span_eq_top_of_affine_span_eq_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : set P} (h : affine_span k s = ⊤) :
vector_span k s = ⊤

If the affine span of a set is ⊤, then the vector span of the same set is the ⊤.

source
theorem affine_subspace.affine_span_eq_top_iff_vector_span_eq_top_of_nonempty (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : set P} (hs : s.nonempty) :
affine_span k s = ⊤ ↔ vector_span k s = ⊤

For a nonempty set, the affine span is ⊤ iff its vector span is ⊤.

source
theorem affine_subspace.affine_span_eq_top_iff_vector_span_eq_top_of_nontrivial (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : set P} [nontrivial P] :
affine_span k s = ⊤ ↔ vector_span k s = ⊤

For a non-trivial space, the affine span of a set is ⊤ iff its vector span is ⊤.

source
theorem affine_subspace.card_pos_of_affine_span_eq_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {ι : Type u_4} [fintype ι] {p : ι → P} (h : affine_span k (set.range p) = ⊤) :
0 < fintype.card ι
source
theorem affine_subspace.not_mem_bot (k : Type u_1) (V : Type u_2) {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (p : P) :
p ∉ ⊥

No points are in ⊥.

source
@[simp]
theorem affine_subspace.direction_bot (k : Type u_1) (V : Type u_2) (P : Type u_3) [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] :
⊥.direction = ⊥

The direction of ⊥ is the submodule ⊥.

source
@[simp]
theorem affine_subspace.coe_eq_bot_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (Q : affine_subspace k P) :
↑Q = ∅ ↔ Q = ⊥
source
@[simp]
theorem affine_subspace.coe_eq_univ_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (Q : affine_subspace k P) :
↑Q = set.univ ↔ Q = ⊤
source
theorem affine_subspace.nonempty_iff_ne_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (Q : affine_subspace k P) :
↑Q.nonempty ↔ Q ≠ ⊥
source
theorem affine_subspace.eq_bot_or_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (Q : affine_subspace k P) :
Q = ⊥ ∨ ↑Q.nonempty
source
theorem affine_subspace.subsingleton_of_subsingleton_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : set P} (h₁ : s.subsingleton) (h₂ : affine_span k s = ⊤) :
subsingleton P
source
theorem affine_subspace.eq_univ_of_subsingleton_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : set P} (h₁ : s.subsingleton) (h₂ : affine_span k s = ⊤) :
s = set.univ
source
@[simp]
theorem affine_subspace.direction_eq_top_iff_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s : affine_subspace k P} (h : ↑s.nonempty) :
s.direction = ⊤ ↔ s = ⊤

A nonempty affine subspace is ⊤ if and only if its direction is ⊤.

source
@[simp]
theorem affine_subspace.inf_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
↑s1 ⊓ ↑s2 = ↑s1 ∩ ↑s2

The inf of two affine subspaces, coerced to a set, is the intersection of the two sets of points.

source
theorem affine_subspace.mem_inf_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (p : P) (s1 s2 : affine_subspace k P) :
p ∈ s1 ⊓ s2 ↔ p ∈ s1 ∧ p ∈ s2

A point is in the inf of two affine subspaces if and only if it is in both of them.

source
theorem affine_subspace.direction_inf {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
(s1 ⊓ s2).direction ≤ s1.direction ⊓ s2.direction

The direction of the inf of two affine subspaces is less than or equal to the inf of their directions.

source
theorem affine_subspace.direction_inf_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s₁ s₂ : affine_subspace k P} {p : P} (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) :
(s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

If two affine subspaces have a point in common, the direction of their inf equals the inf of their directions.

source
theorem affine_subspace.direction_inf_of_mem_inf {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s₁ s₂ : affine_subspace k P} {p : P} (h : p ∈ s₁ ⊓ s₂) :
(s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

If two affine subspaces have a point in their inf, the direction of their inf equals the inf of their directions.

source
theorem affine_subspace.direction_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s1 s2 : affine_subspace k P} (h : s1 ≤ s2) :
s1.direction ≤ s2.direction

If one affine subspace is less than or equal to another, the same applies to their directions.

source
theorem affine_subspace.direction_lt_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s1 s2 : affine_subspace k P} (h : s1 < s2) (hn : ↑s1.nonempty) :
s1.direction < s2.direction

If one nonempty affine subspace is less than another, the same applies to their directions

source
theorem affine_subspace.sup_direction_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s1 s2 : affine_subspace k P) :
s1.direction ⊔ s2.direction ≤ (s1 ⊔ s2).direction

The sup of the directions of two affine subspaces is less than or equal to the direction of their sup.

source
theorem affine_subspace.sup_direction_lt_of_nonempty_of_inter_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s1 s2 : affine_subspace k P} (h1 : ↑s1.nonempty) (h2 : ↑s2.nonempty) (he : ↑s1 ∩ ↑s2 = ∅) :
s1.direction ⊔ s2.direction < (s1 ⊔ s2).direction

The sup of the directions of two nonempty affine subspaces with empty intersection is less than the direction of their sup.

source
theorem affine_subspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s1 s2 : affine_subspace k P} (h1 : ↑s1.nonempty) (h2 : ↑s2.nonempty) (hd : s1.direction ⊔ s2.direction = ⊤) :
(↑s1 ∩ ↑s2).nonempty

If the directions of two nonempty affine subspaces span the whole module, they have nonempty intersection.

source
theorem affine_subspace.inter_eq_singleton_of_nonempty_of_is_compl {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] {s1 s2 : affine_subspace k P} (h1 : ↑s1.nonempty) (h2 : ↑s2.nonempty) (hd : is_compl s1.direction s2.direction) :
∃ (p : P), ↑s1 ∩ ↑s2 = {p}

If the directions of two nonempty affine subspaces are complements of each other, they intersect in exactly one point.

source
@[simp]
theorem affine_subspace.affine_span_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [S : add_torsor V P] (s : affine_subspace k P) :
affine_span k ↑s = s

Coercing a subspace to a set then taking the affine span produces the original subspace.

source
theorem vector_span_eq_span_vsub_set_left (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : P} (hp : p ∈ s) :
vector_span k s = submodule.span k (has_vsub.vsub p '' s)

The vector_span is the span of the pairwise subtractions with a given point on the left.

source
theorem vector_span_eq_span_vsub_set_right (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : P} (hp : p ∈ s) :
vector_span k s = submodule.span k ((λ (_x : P), _x -ᵥ p) '' s)

The vector_span is the span of the pairwise subtractions with a given point on the right.

source
theorem vector_span_eq_span_vsub_set_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : P} (hp : p ∈ s) :
vector_span k s = submodule.span k (has_vsub.vsub p '' (s \ {p}))

The vector_span is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

source
theorem vector_span_eq_span_vsub_set_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : P} (hp : p ∈ s) :
vector_span k s = submodule.span k ((λ (_x : P), _x -ᵥ p) '' (s \ {p}))

The vector_span is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

source
theorem vector_span_eq_span_vsub_finset_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] [decidable_eq P] [decidable_eq V] {s : finset P} {p : P} (hp : p ∈ s) :
vector_span k ↑s = submodule.span k ↑(finset.image (λ (_x : P), _x -ᵥ p) (s.erase p))

The vector_span is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

source
theorem vector_span_image_eq_span_vsub_set_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) {s : set ι} {i : ι} (hi : i ∈ s) :
vector_span k (p '' s) = submodule.span k (has_vsub.vsub (p i) '' (p '' (s \ {i})))

The vector_span of the image of a function is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

source
theorem vector_span_image_eq_span_vsub_set_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) {s : set ι} {i : ι} (hi : i ∈ s) :
vector_span k (p '' s) = submodule.span k ((λ (_x : P), _x -ᵥ p i) '' (p '' (s \ {i})))

The vector_span of the image of a function is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

source
theorem vector_span_range_eq_span_range_vsub_left (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) (i0 : ι) :
vector_span k (set.range p) = submodule.span k (set.range (λ (i : ι), p i0 -ᵥ p i))

The vector_span of an indexed family is the span of the pairwise subtractions with a given point on the left.

source
theorem vector_span_range_eq_span_range_vsub_right (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) (i0 : ι) :
vector_span k (set.range p) = submodule.span k (set.range (λ (i : ι), p i -ᵥ p i0))

The vector_span of an indexed family is the span of the pairwise subtractions with a given point on the right.

source
theorem vector_span_range_eq_span_range_vsub_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) (i₀ : ι) :
vector_span k (set.range p) = submodule.span k (set.range (λ (i : {x // x ≠ i₀}), p i₀ -ᵥ p ↑i))

The vector_span of an indexed family is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

source
theorem vector_span_range_eq_span_range_vsub_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) (i₀ : ι) :
vector_span k (set.range p) = submodule.span k (set.range (λ (i : {x // x ≠ i₀}), p ↑i -ᵥ p i₀))

The vector_span of an indexed family is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

source
theorem affine_span_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} :
↑(affine_span k s).nonempty ↔ s.nonempty

The affine span of a set is nonempty if and only if that set is.

source
theorem set.nonempty.affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} :
s.nonempty → ↑(affine_span k s).nonempty

Alias of the reverse direction of affine_span_nonempty.

source
@[protected, instance]
def affine_span.nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} [nonempty ↥s] :
nonempty ↥(affine_span k s)

The affine span of a nonempty set is nonempty.

source
@[simp]
theorem affine_span_eq_bot (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} :
affine_span k s = ⊥ ↔ s = ∅

The affine span of a set is ⊥ if and only if that set is empty.

source
@[simp]
theorem bot_lt_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} :
⊥ < affine_span k s ↔ s.nonempty
source
theorem affine_span_induction {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {x : P} {s : set P} {p : P → Prop} (h : x ∈ affine_span k s) (Hs : ∀ (x : P), x ∈ s → p x) (Hc : ∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)) :
p x

An induction principle for span membership. If p holds for all elements of s and is preserved under certain affine combinations, then p holds for all elements of the span of s.

source
theorem affine_span_induction' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : Π (x : P), x ∈ affine_span k s → Prop} (Hs : ∀ (y : P) (hys : y ∈ s), p y _) (Hc : ∀ (c : k) (u : P) (hu : u ∈ affine_span k s) (v : P) (hv : v ∈ affine_span k s) (w : P) (hw : w ∈ affine_span k s), p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) _) {x : P} (h : x ∈ affine_span k s) :
p x h

A dependent version of affine_span_induction.

source
@[simp]
theorem affine_span_coe_preimage_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (A : set P) [nonempty ↥A] :
affine_span k (coe ⁻¹' A) = ⊤

A set, considered as a subset of its spanned affine subspace, spans the whole subspace.

source
theorem affine_span_singleton_union_vadd_eq_top_of_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set V} (p : P) (h : submodule.span k (set.range coe) = ⊤) :
affine_span k ({p} ∪ (λ (v : V), v +ᵥ p) '' s) = ⊤

Suppose a set of vectors spans V. Then a point p, together with those vectors added to p, spans P.

source
theorem vector_span_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :
vector_span k {p₁, p₂} = submodule.span k {p₁ -ᵥ p₂}

The vector_span of two points is the span of their difference.

source
theorem vector_span_pair_rev (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :
vector_span k {p₁, p₂} = submodule.span k {p₂ -ᵥ p₁}

The vector_span of two points is the span of their difference (reversed).

source
theorem vsub_mem_vector_span_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :
p₁ -ᵥ p₂ ∈ vector_span k {p₁, p₂}

The difference between two points lies in their vector_span.

source
theorem vsub_rev_mem_vector_span_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :
p₂ -ᵥ p₁ ∈ vector_span k {p₁, p₂}

The difference between two points (reversed) lies in their vector_span.

source
theorem smul_vsub_mem_vector_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (r : k) (p₁ p₂ : P) :
r • (p₁ -ᵥ p₂) ∈ vector_span k {p₁, p₂}

A multiple of the difference between two points lies in their vector_span.

source
theorem smul_vsub_rev_mem_vector_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (r : k) (p₁ p₂ : P) :
r • (p₂ -ᵥ p₁) ∈ vector_span k {p₁, p₂}

A multiple of the difference between two points (reversed) lies in their vector_span.

source
theorem mem_vector_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ : P} {v : V} :
v ∈ vector_span k {p₁, p₂} ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v

A vector lies in the vector_span of two points if and only if it is a multiple of their difference.

source
theorem mem_vector_span_pair_rev {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ : P} {v : V} :
v ∈ vector_span k {p₁, p₂} ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v

A vector lies in the vector_span of two points if and only if it is a multiple of their difference (reversed).

source
theorem left_mem_affine_span_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :
p₁ ∈ affine_span k {p₁, p₂}

The first of two points lies in their affine span.

source
theorem right_mem_affine_span_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :
p₂ ∈ affine_span k {p₁, p₂}

The second of two points lies in their affine span.

source
theorem affine_map.line_map_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (r : k) (p₁ p₂ : P) :
⇑(affine_map.line_map p₁ p₂) r ∈ affine_span k {p₁, p₂}

A combination of two points expressed with line_map lies in their affine span.

source
theorem affine_map.line_map_rev_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (r : k) (p₁ p₂ : P) :
⇑(affine_map.line_map p₂ p₁) r ∈ affine_span k {p₁, p₂}

A combination of two points expressed with line_map (with the two points reversed) lies in their affine span.

source
theorem smul_vsub_vadd_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (r : k) (p₁ p₂ : P) :
r • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ affine_span k {p₁, p₂}

A multiple of the difference of two points added to the first point lies in their affine span.

source
theorem smul_vsub_rev_vadd_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (r : k) (p₁ p₂ : P) :
r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ affine_span k {p₁, p₂}

A multiple of the difference of two points added to the second point lies in their affine span.

source
theorem vadd_left_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ : P} {v : V} :
v +ᵥ p₁ ∈ affine_span k {p₁, p₂} ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v

A vector added to the first point lies in the affine span of two points if and only if it is a multiple of their difference.

source
theorem vadd_right_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ : P} {v : V} :
v +ᵥ p₂ ∈ affine_span k {p₁, p₂} ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v

A vector added to the second point lies in the affine span of two points if and only if it is a multiple of their difference.

source
theorem affine_span_pair_le_of_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ : P} {s : affine_subspace k P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
affine_span k {p₁, p₂} ≤ s

The span of two points that lie in an affine subspace is contained in that subspace.

source
theorem affine_span_pair_le_of_left_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ : P} (h : p₁ ∈ affine_span k {p₂, p₃}) :
affine_span k {p₁, p₃} ≤ affine_span k {p₂, p₃}

One line is contained in another differing in the first point if the first point of the first line is contained in the second line.

source
theorem affine_span_pair_le_of_right_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ : P} (h : p₁ ∈ affine_span k {p₂, p₃}) :
affine_span k {p₂, p₁} ≤ affine_span k {p₂, p₃}

One line is contained in another differing in the second point if the second point of the first line is contained in the second line.

source
theorem affine_span_mono (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : set P} (h : s₁ ⊆ s₂) :
affine_span k s₁ ≤ affine_span k s₂

affine_span is monotone.

source
theorem affine_span_insert_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) (ps : set P) :
affine_span k (has_insert.insert p ↑(affine_span k ps)) = affine_span k (has_insert.insert p ps)

Taking the affine span of a set, adding a point and taking the span again produces the same results as adding the point to the set and taking the span.

source
theorem affine_span_insert_eq_affine_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : P} {ps : set P} (h : p ∈ affine_span k ps) :
affine_span k (has_insert.insert p ps) = affine_span k ps

If a point is in the affine span of a set, adding it to that set does not change the affine span.

source
theorem vector_span_insert_eq_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : P} {ps : set P} (h : p ∈ affine_span k ps) :
vector_span k (has_insert.insert p ps) = vector_span k ps

If a point is in the affine span of a set, adding it to that set does not change the vector span.

source
theorem affine_subspace.direction_sup {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s1 s2 : affine_subspace k P} {p1 p2 : P} (hp1 : p1 ∈ s1) (hp2 : p2 ∈ s2) :
(s1 ⊔ s2).direction = s1.direction ⊔ s2.direction ⊔ submodule.span k {p2 -ᵥ p1}

The direction of the sup of two nonempty affine subspaces is the sup of the two directions and of any one difference between points in the two subspaces.

source
theorem affine_subspace.direction_affine_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p1 p2 : P} (hp1 : p1 ∈ s) :
(affine_span k (has_insert.insert p2 ↑s)).direction = submodule.span k {p2 -ᵥ p1} ⊔ s.direction

The direction of the span of the result of adding a point to a nonempty affine subspace is the sup of the direction of that subspace and of any one difference between that point and a point in the subspace.

source
theorem affine_subspace.mem_affine_span_insert_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p1 : P} (hp1 : p1 ∈ s) (p2 p : P) :
p ∈ affine_span k (has_insert.insert p2 ↑s) ↔ ∃ (r : k) (p0 : P) (hp0 : p0 ∈ s), p = r • (p2 -ᵥ p1) +ᵥ p0

Given a point p1 in an affine subspace s, and a point p2, a point p is in the span of s with p2 added if and only if it is a multiple of p2 -ᵥ p1 added to a point in s.

source
@[simp]
theorem affine_map.vector_span_image_eq_submodule_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : set P₁} :
submodule.map f.linear (vector_span k s) = vector_span k (⇑f '' s)
source
def affine_subspace.map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : affine_subspace k P₁) :
affine_subspace k P₂

The image of an affine subspace under an affine map as an affine subspace.

Equations
source
@[simp]
theorem affine_subspace.coe_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : affine_subspace k P₁) :
↑(affine_subspace.map f s) = ⇑f '' ↑s
source
@[simp]
theorem affine_subspace.mem_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₂} {s : affine_subspace k P₁} :
x ∈ affine_subspace.map f s ↔ ∃ (y : P₁) (H : y ∈ s), ⇑f y = x
source
theorem affine_subspace.mem_map_of_mem {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {x : P₁} {s : affine_subspace k P₁} (h : x ∈ s) :
⇑f x ∈ affine_subspace.map f s
source
theorem affine_subspace.mem_map_iff_mem_of_injective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : affine_subspace k P₁} (hf : function.injective ⇑f) :
⇑f x ∈ affine_subspace.map f s ↔ x ∈ s
source
@[simp]
theorem affine_subspace.map_bot {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) :
affine_subspace.map f ⊥ = ⊥
source
@[simp]
theorem affine_subspace.map_eq_bot_iff {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : affine_subspace k P₁} :
affine_subspace.map f s = ⊥ ↔ s = ⊥
source
@[simp]
theorem affine_subspace.map_id {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] (s : affine_subspace k P₁) :
affine_subspace.map (affine_map.id k P₁) s = s
source
theorem affine_subspace.map_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] [add_comm_group V₃] [module k V₃] [add_torsor V₃ P₃] (s : affine_subspace k P₁) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) :
affine_subspace.map g (affine_subspace.map f s) = affine_subspace.map (g.comp f) s
source
@[simp]
theorem affine_subspace.map_direction {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : affine_subspace k P₁) :
(affine_subspace.map f s).direction = submodule.map f.linear s.direction
source
theorem affine_subspace.map_span {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : set P₁) :
affine_subspace.map f (affine_span k s) = affine_span k (⇑f '' s)
source
@[simp]
theorem affine_map.map_top_of_surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (hf : function.surjective ⇑f) :
affine_subspace.map f ⊤ = ⊤
source
theorem affine_map.span_eq_top_of_surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : set P₁} (hf : function.surjective ⇑f) (h : affine_span k s = ⊤) :
affine_span k (⇑f '' s) = ⊤
source
theorem affine_equiv.span_eq_top_iff {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {s : set P₁} (e : P₁ ≃ᵃ[k] P₂) :
affine_span k s = ⊤ ↔ affine_span k (⇑e '' s) = ⊤
source
def affine_subspace.comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : affine_subspace k P₂) :
affine_subspace k P₁

The preimage of an affine subspace under an affine map as an affine subspace.

Equations
source
@[simp]
theorem affine_subspace.coe_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : affine_subspace k P₂) :
↑(affine_subspace.comap f s) = ⇑f ⁻¹' ↑s
source
@[simp]
theorem affine_subspace.mem_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : affine_subspace k P₂} :
x ∈ affine_subspace.comap f s ↔ ⇑f x ∈ s
source
theorem affine_subspace.comap_mono {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s t : affine_subspace k P₂} :
s ≤ t → affine_subspace.comap f s ≤ affine_subspace.comap f t
source
@[simp]
theorem affine_subspace.comap_top {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} :
affine_subspace.comap f ⊤ = ⊤
source
@[simp]
theorem affine_subspace.comap_id {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] (s : affine_subspace k P₁) :
affine_subspace.comap (affine_map.id k P₁) s = s
source
theorem affine_subspace.comap_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] [add_comm_group V₃] [module k V₃] [add_torsor V₃ P₃] (s : affine_subspace k P₃) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) :
affine_subspace.comap f (affine_subspace.comap g s) = affine_subspace.comap (g.comp f) s
source
theorem affine_subspace.map_le_iff_le_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s : affine_subspace k P₁} {t : affine_subspace k P₂} :
affine_subspace.map f s ≤ t ↔ s ≤ affine_subspace.comap f t
source
theorem affine_subspace.gc_map_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) :
galois_connection (affine_subspace.map f) (affine_subspace.comap f)
source
theorem affine_subspace.map_comap_le {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : affine_subspace k P₂) :
affine_subspace.map f (affine_subspace.comap f s) ≤ s
source
theorem affine_subspace.le_comap_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : affine_subspace k P₁) :
s ≤ affine_subspace.comap f (affine_subspace.map f s)
source
theorem affine_subspace.map_sup {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (s t : affine_subspace k P₁) (f : P₁ →ᵃ[k] P₂) :
affine_subspace.map f (s ⊔ t) = affine_subspace.map f s ⊔ affine_subspace.map f t
source
theorem affine_subspace.map_supr {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {ι : Sort u_6} (f : P₁ →ᵃ[k] P₂) (s : ι → affine_subspace k P₁) :
affine_subspace.map f (supr s) = ⨆ (i : ι), affine_subspace.map f (s i)
source
theorem affine_subspace.comap_inf {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (s t : affine_subspace k P₂) (f : P₁ →ᵃ[k] P₂) :
affine_subspace.comap f (s ⊓ t) = affine_subspace.comap f s ⊓ affine_subspace.comap f t
source
theorem affine_subspace.comap_supr {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {ι : Sort u_6} (f : P₁ →ᵃ[k] P₂) (s : ι → affine_subspace k P₂) :
affine_subspace.comap f (infi s) = ⨅ (i : ι), affine_subspace.comap f (s i)
source
@[simp]
theorem affine_subspace.comap_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : affine_subspace k P₁) :
affine_subspace.comap ↑(e.symm) s = affine_subspace.map ↑e s
source
@[simp]
theorem affine_subspace.map_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : affine_subspace k P₂) :
affine_subspace.map ↑(e.symm) s = affine_subspace.comap ↑e s
source
theorem affine_subspace.comap_span {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [ring k] [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : set P₂) :
affine_subspace.comap ↑f (affine_span k s) = affine_span k (⇑f ⁻¹' s)
source
def affine_subspace.parallel {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s₁ s₂ : affine_subspace k P) :
Prop

Two affine subspaces are parallel if one is related to the other by adding the same vector to all points.

Equations
source
@[symm]
theorem affine_subspace.parallel.symm {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : affine_subspace k P} (h : s₁.parallel s₂) :
s₂.parallel s₁
source
theorem affine_subspace.parallel_comm {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : affine_subspace k P} :
s₁.parallel s₂ ↔ s₂.parallel s₁
source
@[refl]
theorem affine_subspace.parallel.refl {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) :
s.parallel s
source
@[trans]
theorem affine_subspace.parallel.trans {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ s₃ : affine_subspace k P} (h₁₂ : s₁.parallel s₂) (h₂₃ : s₂.parallel s₃) :
s₁.parallel s₃
source
theorem affine_subspace.parallel.direction_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : affine_subspace k P} (h : s₁.parallel s₂) :
s₁.direction = s₂.direction
source
@[simp]
theorem affine_subspace.parallel_bot_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} :
s.parallel ⊥ ↔ s = ⊥
source
@[simp]
theorem affine_subspace.bot_parallel_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} :
⊥.parallel s ↔ s = ⊥
source
theorem affine_subspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : affine_subspace k P} :
s₁.parallel s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
source
theorem affine_subspace.parallel.vector_span_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : set P} (h : (affine_span k s₁).parallel (affine_span k s₂)) :
vector_span k s₁ = vector_span k s₂
source
theorem affine_subspace.affine_span_parallel_iff_vector_span_eq_and_eq_empty_iff_eq_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : set P} :
(affine_span k s₁).parallel (affine_span k s₂) ↔ vector_span k s₁ = vector_span k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)
source
theorem affine_subspace.affine_span_pair_parallel_iff_vector_span_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ p₄ : P} :
(affine_span k {p₁, p₂}).parallel (affine_span k {p₃, p₄}) ↔ vector_span k {p₁, p₂} = vector_span k {p₃, p₄}