Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

vectorSpan definition

(s : Set P) : Submodule k V

Full source

/-- The submodule spanning the differences of a (possibly empty) set of points. -/
def vectorSpan (s : Set P) : Submodule k V :=
  Submodule.span k (s -ᵥ s)

Vector span of a set of points in an affine space

Informal description

The `vectorSpan` of a set $s$ of points in an affine space over a module $V$ is the submodule of $V$ spanned by the differences of points in $s$. It is defined as the span of the set $\{p - q \mid p, q \in s\}$ under the module structure of $V$.

vectorSpan_def theorem

(s : Set P) : vectorSpan k s = Submodule.span k (s -ᵥ s)

Full source

/-- The definition of `vectorSpan`, for rewriting. -/
theorem vectorSpan_def (s : Set P) : vectorSpan k s = Submodule.span k (s -ᵥ s) :=
  rfl

Vector Span as Linear Span of Point Differences

Informal description

For any set $s$ of points in an affine space over a module $V$, the vector span of $s$ is equal to the linear span of the set of vectors $\{p - q \mid p, q \in s\}$ in $V$.

vectorSpan_mono theorem

{s₁ s₂ : Set P} (h : s₁ ⊆ s₂) : vectorSpan k s₁ ≤ vectorSpan k s₂

Full source

/-- `vectorSpan` is monotone. -/
theorem vectorSpan_mono {s₁ s₂ : Set P} (h : s₁ ⊆ s₂) : vectorSpan k s₁ ≤ vectorSpan k s₂ :=
  Submodule.span_mono (vsub_self_mono h)

Monotonicity of Vector Span: $s_1 \subseteq s_2 \Rightarrow \operatorname{vectorSpan}_k s_1 \leq \operatorname{vectorSpan}_k s_2$

Informal description

For any two sets $s_1$ and $s_2$ of points in an affine space over a module $V$, if $s_1 \subseteq s_2$, then the vector span of $s_1$ is contained in the vector span of $s_2$, i.e., $\operatorname{vectorSpan}_k s_1 \leq \operatorname{vectorSpan}_k s_2$.

vectorSpan_empty theorem

: vectorSpan k (∅ : Set P) = (⊥ : Submodule k V)

Full source

/-- The `vectorSpan` of the empty set is `⊥`. -/
@[simp]
theorem vectorSpan_empty : vectorSpan k (∅ : Set P) = (⊥ : Submodule k V) := by
  rw [vectorSpan_def, vsub_empty, Submodule.span_empty]

Vector Span of Empty Set is Trivial Submodule

Informal description

The vector span of the empty set in an affine space over a module $V$ is the trivial submodule $\bot$ of $V$.

vectorSpan_singleton theorem

(p : P) : vectorSpan k ({ p } : Set P) = ⊥

Full source

/-- The `vectorSpan` of a single point is `⊥`. -/
@[simp]
theorem vectorSpan_singleton (p : P) : vectorSpan k ({p} : Set P) = ⊥ := by simp [vectorSpan_def]

Vector Span of Singleton is Trivial Submodule

Informal description

For any point $p$ in an affine space over a module $V$, the vector span of the singleton set $\{p\}$ is the trivial submodule $\bot$ of $V$.

vsub_set_subset_vectorSpan theorem

(s : Set P) : s -ᵥ s ⊆ ↑(vectorSpan k s)

Full source

/-- The `s -ᵥ s` lies within the `vectorSpan k s`. -/
theorem vsub_set_subset_vectorSpan (s : Set P) : s -ᵥ ss -ᵥ s ⊆ ↑(vectorSpan k s) :=
  Submodule.subset_span

Difference Vectors Belong to Vector Span

Informal description

For any set $s$ of points in an affine space over a module $V$, the set of pairwise difference vectors $\{p - q \mid p, q \in s\}$ is contained in the vector span of $s$ (i.e., the submodule of $V$ generated by these differences).

vsub_mem_vectorSpan theorem

{s : Set P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : p₁ -ᵥ p₂ ∈ vectorSpan k s

Full source

/-- Each pairwise difference is in the `vectorSpan`. -/
theorem vsub_mem_vectorSpan {s : Set P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
    p₁ -ᵥ p₂p₁ -ᵥ p₂ ∈ vectorSpan k s :=
  vsub_set_subset_vectorSpan k s (vsub_mem_vsub hp₁ hp₂)

Difference Vector of Points in Set Belongs to Vector Span

Informal description

For any set $s$ of points in an affine space over a module $V$, and for any two points $p_1, p_2 \in s$, the difference vector $p_1 - p_2$ lies in the vector span of $s$.

spanPoints definition

(s : Set P) : Set P

Full source

/-- The points in the affine span of a (possibly empty) set of points. Use `affineSpan` instead to
get an `AffineSubspace k P`. -/
def spanPoints (s : Set P) : Set P :=
  { p | ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, p = v +ᵥ p₁ }

Points in the affine span of a set

Informal description

Given a set $s$ of points in an affine space over a module $V$, the set $\text{spanPoints}\ k\ s$ consists of all points $p$ such that there exists a point $p_1 \in s$ and a vector $v$ in the vector span of $s$ (i.e., the submodule of $V$ spanned by differences of points in $s$) with $p = v + p_1$.

mem_spanPoints theorem

(p : P) (s : Set P) : p ∈ s → p ∈ spanPoints k s

Full source

/-- A point in a set is in its affine span. -/
theorem mem_spanPoints (p : P) (s : Set P) : p ∈ s → p ∈ spanPoints k s
  | hp => ⟨p, hp, 0, Submodule.zero_mem _, (zero_vadd V p).symm⟩

Point in Set is in its Affine Span

Informal description

For any point $p$ in a set $s$ of points in an affine space over a module $V$, $p$ is contained in the affine span of $s$, i.e., $p \in \text{spanPoints}_k s$.

subset_spanPoints theorem

(s : Set P) : s ⊆ spanPoints k s

Full source

/-- A set is contained in its `spanPoints`. -/
theorem subset_spanPoints (s : Set P) : s ⊆ spanPoints k s := fun p => mem_spanPoints k p s

Set is Contained in its Affine Span

Informal description

For any set $s$ of points in an affine space over a module $V$, the set $s$ is contained in its affine span, i.e., $s \subseteq \text{spanPoints}_k s$.

spanPoints_nonempty theorem

(s : Set P) : (spanPoints k s).Nonempty ↔ s.Nonempty

Full source

/-- The `spanPoints` of a set is nonempty if and only if that set is. -/
@[simp]
theorem spanPoints_nonempty (s : Set P) : (spanPoints k s).Nonempty ↔ s.Nonempty := by
  constructor
  · contrapose
    rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]
    intro h
    simp [h, spanPoints]
  · exact fun h => h.mono (subset_spanPoints _ _)

Nonemptiness of Affine Span Equivalence

Informal description

For any set $s$ of points in an affine space over a module $V$, the affine span $\text{spanPoints}_k s$ is nonempty if and only if the set $s$ itself is nonempty.

vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan theorem

{s : Set P} {p : P} {v : V} (hp : p ∈ spanPoints k s) (hv : v ∈ vectorSpan k s) : v +ᵥ p ∈ spanPoints k s

Full source

/-- Adding a point in the affine span and a vector in the spanning submodule produces a point in the
affine span. -/
theorem vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan {s : Set P} {p : P} {v : V}
    (hp : p ∈ spanPoints k s) (hv : v ∈ vectorSpan k s) : v +ᵥ pv +ᵥ p ∈ spanPoints k s := by
  rcases hp with ⟨p₂, ⟨hp₂, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
  rw [hv₂p, vadd_vadd]
  exact ⟨p₂, hp₂, v + v₂, (vectorSpan k s).add_mem hv hv₂, rfl⟩

Affine Span is Closed Under Translation by Vector Span Elements

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a set of points in $P$. For any point $p$ in the affine span of $s$ and any vector $v$ in the vector span of $s$, the point obtained by adding $v$ to $p$ (denoted $v + p$) is also in the affine span of $s$.

vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints theorem

 {s : Set P} {p₁ p₂ : P} (hp₁ : p₁ ∈ spanPoints k s) (hp₂ : p₂ ∈ spanPoints k s) : p₁ -ᵥ p₂ ∈ vectorSpan k s

Full source

/-- Subtracting two points in the affine span produces a vector in the spanning submodule. -/
theorem vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints {s : Set P} {p₁ p₂ : P}
    (hp₁ : p₁ ∈ spanPoints k s) (hp₂ : p₂ ∈ spanPoints k s) : p₁ -ᵥ p₂p₁ -ᵥ p₂ ∈ vectorSpan k s := by
  rcases hp₁ with ⟨p₁a, ⟨hp₁a, ⟨v₁, ⟨hv₁, hv₁p⟩⟩⟩⟩
  rcases hp₂ with ⟨p₂a, ⟨hp₂a, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
  rw [hv₁p, hv₂p, vsub_vadd_eq_vsub_sub (v₁ +ᵥ p₁a), vadd_vsub_assoc, add_comm, add_sub_assoc]
  have hv₁v₂ : v₁ - v₂ ∈ vectorSpan k s := (vectorSpan k s).sub_mem hv₁ hv₂
  refine (vectorSpan k s).add_mem ?_ hv₁v₂
  exact vsub_mem_vectorSpan k hp₁a hp₂a

Difference of Points in Affine Span Belongs to Vector Span

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, and for any two points $p_1, p_2 \in \text{spanPoints}\ k\ s$, the difference vector $p_1 - p_2$ lies in the vector span of $s$.

AffineSubspace structure

(k : Type*) {V : Type*} (P : Type*) [Ring k] [AddCommGroup V] [Module k V] [AffineSpace V P]

Full source

/-- An `AffineSubspace k P` is a subset of an `AffineSpace V P` that, if not empty, has an affine
space structure induced by a corresponding subspace of the `Module k V`. -/
structure AffineSubspace (k : Type*) {V : Type*} (P : Type*) [Ring k] [AddCommGroup V]
  [Module k V] [AffineSpace V P] where
  /-- The affine subspace seen as a subset. -/
  carrier : Set P
  smul_vsub_vadd_mem :
    ∀ (c : k) {p₁ p₂ p₃ : P},
      p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂ : V) +ᵥ p₃c • (p₁ -ᵥ p₂ : V) +ᵥ p₃ ∈ carrier

Affine Subspace

Informal description

An affine subspace of an affine space $P$ over a module $V$ with scalar ring $k$ is a subset of $P$ that, if nonempty, inherits an affine space structure from a corresponding subspace of $V$. More formally, given a ring $k$, an additive commutative group $V$ with a $k$-module structure, and an affine space $P$ over $V$, an affine subspace is a subset of $P$ that is closed under affine combinations (i.e., for any two points in the subset, the entire line through them is contained in the subset). The direction of an affine subspace is the subspace of $V$ spanned by the differences of points in the affine subspace. The affine span of a set of points is the smallest affine subspace containing those points, and its direction is the vector span of the pairwise differences of the points.

Submodule.toAffineSubspace definition

(p : Submodule k V) : AffineSubspace k V

Full source

/-- Reinterpret `p : Submodule k V` as an `AffineSubspace k V`. -/
def toAffineSubspace (p : Submodule k V) : AffineSubspace k V where
  carrier := p
  smul_vsub_vadd_mem _ _ _ _ h₁ h₂ h₃ := p.add_mem (p.smul_mem _ (p.sub_mem h₁ h₂)) h₃

Submodule as affine subspace

Informal description

Given a submodule $p$ of a module $V$ over a ring $k$, the function `Submodule.toAffineSubspace` reinterprets $p$ as an affine subspace of $V$ by taking the carrier set to be $p$ itself and ensuring closure under the affine combination operation: for any $c \in k$ and $v_1, v_2, v_3 \in p$, the combination $c \cdot (v_1 - v_2) + v_3$ must also lie in $p$.

AffineSubspace.instSetLike instance

: SetLike (AffineSubspace k P) P

Full source

instance : SetLike (AffineSubspace k P) P where
  coe := carrier
  coe_injective' p q _ := by cases p; cases q; congr

Set-like Structure on Affine Subspaces

Informal description

The type of affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$ can be endowed with a set-like structure, where each affine subspace is treated as a subset of $P$.

AffineSubspace.mem_coe theorem

(p : P) (s : AffineSubspace k P) : p ∈ (s : Set P) ↔ p ∈ s

Full source

/-- A point is in an affine subspace coerced to a set if and only if it is in that affine
subspace. -/
theorem mem_coe (p : P) (s : AffineSubspace k P) : p ∈ (s : Set P)p ∈ (s : Set P) ↔ p ∈ s := by simp

Membership in Affine Subspace Coercion

Informal description

For any point $p$ in an affine space $P$ and any affine subspace $s$ of $P$, the point $p$ belongs to the set underlying $s$ if and only if $p$ belongs to $s$ as an affine subspace. In other words, $p \in (s : \text{Set } P) \leftrightarrow p \in s$.

AffineSubspace.direction definition

(s : AffineSubspace k P) : Submodule k V

Full source

/-- 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.) -/
def direction (s : AffineSubspace k P) : Submodule k V :=
  vectorSpan k (s : Set P)

Direction of an affine subspace

Informal description

The direction of an affine subspace $ s $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $ is the submodule of $ V $ spanned by the pairwise differences of points in $ s $. More precisely, it is the set of all vectors $ v \in V $ such that there exist points $ p, q \in s $ with $ v = p - q $. This submodule is closed under addition and scalar multiplication, and contains the zero vector (since $ p - p = 0 $ for any $ p \in s $). In the case where $ s $ is empty, the direction is the zero submodule.

AffineSubspace.direction_eq_vectorSpan theorem

(s : AffineSubspace k P) : s.direction = vectorSpan k (s : Set P)

Full source

/-- The direction equals the `vectorSpan`. -/
theorem direction_eq_vectorSpan (s : AffineSubspace k P) : s.direction = vectorSpan k (s : Set P) :=
  rfl

Direction of Affine Subspace Equals Vector Span of Its Points

Informal description

For any affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, the direction of $s$ is equal to the vector span of the underlying set of points of $s$. That is, $\text{direction}(s) = \text{vectorSpan}_k (s \text{ as a set})$.

AffineSubspace.directionOfNonempty definition

{s : AffineSubspace k P} (h : (s : Set P).Nonempty) : Submodule k V

Full source

/-- 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. -/
def directionOfNonempty {s : AffineSubspace k P} (h : (s : Set P).Nonempty) : Submodule k V where
  carrier := (s : Set P) -ᵥ s
  zero_mem' := by
    obtain ⟨p, hp⟩ := h
    exact vsub_self p ▸ vsub_mem_vsub hp hp
  add_mem' := by
    rintro _ _ ⟨p₁, hp₁, p₂, hp₂, rfl⟩ ⟨p₃, hp₃, p₄, hp₄, rfl⟩
    rw [← vadd_vsub_assoc]
    refine vsub_mem_vsub ?_ hp₄
    convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp₃
    rw [one_smul]
  smul_mem' := by
    rintro c _ ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    rw [← vadd_vsub (c • (p₁ -ᵥ p₂)) p₂]
    refine vsub_mem_vsub ?_ hp₂
    exact s.smul_vsub_vadd_mem c hp₁ hp₂ hp₂

Direction of a nonempty affine subspace

Informal description

Given a nonempty affine subspace $ s $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, the direction of $ s $ is the submodule of $ V $ consisting of all vectors $ p - q $ where $ p, q \in s $. More precisely, the direction is defined as the set of all vectors $ v \in V $ such that there exist points $ p, q \in s $ with $ v = p - q $. This submodule is closed under addition and scalar multiplication, and contains the zero vector (since $ p - p = 0 $ for any $ p \in s $).

AffineSubspace.directionOfNonempty_eq_direction theorem

{s : AffineSubspace k P} (h : (s : Set P).Nonempty) : directionOfNonempty h = s.direction

Full source

/-- `direction_of_nonempty` gives the same submodule as `direction`. -/
theorem directionOfNonempty_eq_direction {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    directionOfNonempty h = s.direction := by
  refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)
  rw [← SetLike.coe_subset_coe, directionOfNonempty, direction, Submodule.coe_set_mk,
    AddSubmonoid.coe_set_mk]
  exact vsub_set_subset_vectorSpan k _

Equality of Nonempty Affine Subspace Directions: $\text{directionOfNonempty}(h) = \text{direction}(s)$

Informal description

For any nonempty affine subspace $ s $ of an affine space $ P $ over a module $ V $ with scalar ring $ k $, the direction of $ s $ defined via the `directionOfNonempty` construction is equal to the standard direction of $ s $. That is, $\text{directionOfNonempty}(h) = \text{direction}(s)$, where $ h $ is a proof that $ s $ is nonempty.

AffineSubspace.coe_direction_eq_vsub_set theorem

{s : AffineSubspace k P} (h : (s : Set P).Nonempty) : (s.direction : Set V) = (s : Set P) -ᵥ s

Full source

/-- The set of vectors in the direction of a nonempty affine subspace is given by `vsub_set`. -/
theorem coe_direction_eq_vsub_set {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    (s.direction : Set V) = (s : Set P) -ᵥ s :=
  directionOfNonempty_eq_direction h ▸ rfl

Direction of Nonempty Affine Subspace as Difference Set

Informal description

For any nonempty affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, the set of vectors in the direction of $s$ (viewed as a subset of $V$) is equal to the set of all vectors obtained as differences of points in $s$. That is, \[ \text{direction}(s) = \{p - q \mid p, q \in s\}. \]

AffineSubspace.mem_direction_iff_eq_vsub theorem

 {s : AffineSubspace k P} (h : (s : Set P).Nonempty) (v : V) : v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

Full source

/-- 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. -/
theorem mem_direction_iff_eq_vsub {s : AffineSubspace k P} (h : (s : Set P).Nonempty) (v : V) :
    v ∈ s.directionv ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂ := by
  rw [← SetLike.mem_coe, coe_direction_eq_vsub_set h, Set.mem_vsub]
  simp only [SetLike.mem_coe, eq_comm]

Characterization of Direction Vectors in Nonempty Affine Subspace

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a nonempty affine subspace of $P$. For any vector $v \in V$, $v$ lies in the direction of $s$ if and only if there exist points $p_1, p_2 \in s$ such that $v = p_1 - p_2$.

AffineSubspace.vadd_mem_of_mem_direction theorem

{s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction) {p : P} (hp : p ∈ s) : v +ᵥ p ∈ s

Full source

/-- Adding a vector in the direction to a point in the subspace produces a point in the
subspace. -/
theorem vadd_mem_of_mem_direction {s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction) {p : P}
    (hp : p ∈ s) : v +ᵥ pv +ᵥ p ∈ s := by
  rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv
  rcases hv with ⟨p₁, hp₁, p₂, hp₂, hv⟩
  rw [hv]
  convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp
  rw [one_smul]

Addition of Direction Vector Preserves Affine Subspace Membership

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any vector $v \in V$ in the direction of $s$ and any point $p \in s$, the point obtained by adding $v$ to $p$ (denoted $v + p$) is also in $s$.

AffineSubspace.vsub_mem_direction theorem

{s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : p₁ -ᵥ p₂ ∈ s.direction

Full source

/-- Subtracting two points in the subspace produces a vector in the direction. -/
theorem vsub_mem_direction {s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
    p₁ -ᵥ p₂p₁ -ᵥ p₂ ∈ s.direction :=
  vsub_mem_vectorSpan k hp₁ hp₂

Difference Vector of Points in Affine Subspace Lies in Direction

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any two points $p_1, p_2 \in s$, the difference vector $p_1 - p_2$ lies in the direction of $s$.

AffineSubspace.vadd_mem_iff_mem_direction theorem

{s : AffineSubspace k P} (v : V) {p : P} (hp : p ∈ s) : v +ᵥ p ∈ s ↔ v ∈ s.direction

Full source

/-- 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. -/
theorem vadd_mem_iff_mem_direction {s : AffineSubspace k P} (v : V) {p : P} (hp : p ∈ s) :
    v +ᵥ pv +ᵥ p ∈ sv +ᵥ p ∈ s ↔ v ∈ s.direction :=
  ⟨fun h => by simpa using vsub_mem_direction h hp, fun h => vadd_mem_of_mem_direction h hp⟩

Characterization of Affine Subspace Membership via Direction Vectors

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any vector $v \in V$ and any point $p \in s$, the point $v + p$ lies in $s$ if and only if $v$ is in the direction of $s$.

AffineSubspace.vadd_mem_iff_mem_of_mem_direction theorem

{s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction) {p : P} : v +ᵥ p ∈ s ↔ p ∈ s

Full source

/-- 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. -/
theorem vadd_mem_iff_mem_of_mem_direction {s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction)
    {p : P} : v +ᵥ pv +ᵥ p ∈ sv +ᵥ p ∈ s ↔ p ∈ s := by
  refine ⟨fun h => ?_, fun h => vadd_mem_of_mem_direction hv h⟩
  convert vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h
  simp

Affine Subspace Membership Criterion via Direction Vector Addition

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any vector $v$ in the direction of $s$ and any point $p \in P$, the point $v + p$ is in $s$ if and only if $p$ is in $s$.

AffineSubspace.coe_direction_eq_vsub_set_right theorem

{s : AffineSubspace k P} {p : P} (hp : p ∈ s) : (s.direction : Set V) = (· -ᵥ p) '' s

Full source

/-- 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. -/
theorem coe_direction_eq_vsub_set_right {s : AffineSubspace k P} {p : P} (hp : p ∈ s) :
    (s.direction : Set V) = (· -ᵥ p) '' s := by
  rw [coe_direction_eq_vsub_set ⟨p, hp⟩]
  refine le_antisymm ?_ ?_
  · rintro v ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    exact ⟨(p₁ -ᵥ p₂) +ᵥ p,
      vadd_mem_of_mem_direction (vsub_mem_direction hp₁ hp₂) hp, vadd_vsub _ _⟩
  · rintro v ⟨p₂, hp₂, rfl⟩
    exact ⟨p₂, hp₂, p, hp, rfl⟩

Direction of Affine Subspace as Right Difference Set

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any point $p \in s$, the set of vectors in the direction of $s$ (viewed as a subset of $V$) is equal to the image of $s$ under the function that subtracts $p$ from each point in $s$. That is, \[ \text{direction}(s) = \{q - p \mid q \in s\}. \]

AffineSubspace.coe_direction_eq_vsub_set_left theorem

{s : AffineSubspace k P} {p : P} (hp : p ∈ s) : (s.direction : Set V) = (p -ᵥ ·) '' s

Full source

/-- 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. -/
theorem coe_direction_eq_vsub_set_left {s : AffineSubspace k P} {p : P} (hp : p ∈ s) :
    (s.direction : Set V) = (p -ᵥ ·) '' s := by
  ext v
  rw [SetLike.mem_coe, ← Submodule.neg_mem_iff, ← SetLike.mem_coe,
    coe_direction_eq_vsub_set_right hp, Set.mem_image, Set.mem_image]
  conv_lhs =>
    congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]

Direction of Affine Subspace as Left Difference Set

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any point $p \in s$, the set of vectors in the direction of $s$ (viewed as a subset of $V$) is equal to the image of $s$ under the function that subtracts each point in $s$ from $p$. That is, \[ \text{direction}(s) = \{p - q \mid q \in s\}. \]

AffineSubspace.mem_direction_iff_eq_vsub_right theorem

{s : AffineSubspace k P} {p : P} (hp : p ∈ s) (v : V) : v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Full source

/-- 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. -/
theorem mem_direction_iff_eq_vsub_right {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (v : V) :
    v ∈ s.directionv ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p := by
  rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_right hp]
  exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

Characterization of Direction Vectors via Right Subtraction in Affine Subspace

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any point $p \in s$ and any vector $v \in V$, the vector $v$ belongs to the direction of $s$ if and only if there exists a point $p_2 \in s$ such that $v = p_2 - p$.

AffineSubspace.mem_direction_iff_eq_vsub_left theorem

{s : AffineSubspace k P} {p : P} (hp : p ∈ s) (v : V) : v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Full source

/-- 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. -/
theorem mem_direction_iff_eq_vsub_left {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (v : V) :
    v ∈ s.directionv ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂ := by
  rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]
  exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

Characterization of Direction Vectors via Left Subtraction in Affine Subspace

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any point $p \in s$ and any vector $v \in V$, the vector $v$ belongs to the direction of $s$ if and only if there exists a point $p_2 \in s$ such that $v = p - p_2$.

AffineSubspace.coe_injective theorem

: Function.Injective ((↑) : AffineSubspace k P → Set P)

Full source

/-- Two affine subspaces are equal if they have the same points. -/
theorem coe_injective : Function.Injective ((↑) : AffineSubspace k P → Set P) :=
  SetLike.coe_injective

Injectivity of Affine Subspace to Set Coercion

Informal description

The canonical map from affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$ to subsets of $P$ is injective. That is, if two affine subspaces have the same underlying set of points, then they are equal.

AffineSubspace.ext theorem

{p q : AffineSubspace k P} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q

Full source

@[ext (iff := false)]
theorem ext {p q : AffineSubspace k P} (h : ∀ x, x ∈ px ∈ p ↔ x ∈ q) : p = q :=
  SetLike.ext h

Extensionality of Affine Subspaces

Informal description

For any two affine subspaces $p$ and $q$ of an affine space $P$ over a module $V$ with scalar ring $k$, if for every point $x \in P$ we have $x \in p$ if and only if $x \in q$, then $p = q$.

AffineSubspace.ext_iff theorem

(s₁ s₂ : AffineSubspace k P) : s₁ = s₂ ↔ (s₁ : Set P) = s₂

Full source

protected theorem ext_iff (s₁ s₂ : AffineSubspace k P) : s₁ = s₂ ↔ (s₁ : Set P) = s₂ :=
  SetLike.ext'_iff

Equality of Affine Subspaces via Carrier Set Equality

Informal description

For any two affine subspaces $s₁$ and $s₂$ of an affine space $P$ over a module $V$ with scalar ring $k$, the subspaces are equal if and only if their underlying sets of points in $P$ are equal. That is, $s₁ = s₂ \leftrightarrow (s₁ : \text{Set } P) = s₂$.

AffineSubspace.ext_of_direction_eq theorem

 {s₁ s₂ : AffineSubspace k P} (hd : s₁.direction = s₂.direction) (hn : ((s₁ : Set P) ∩ s₂).Nonempty) : s₁ = s₂

Full source

/-- Two affine subspaces with the same direction and nonempty intersection are equal. -/
theorem ext_of_direction_eq {s₁ s₂ : AffineSubspace k P} (hd : s₁.direction = s₂.direction)
    (hn : ((s₁ : Set P) ∩ s₂).Nonempty) : s₁ = s₂ := by
  ext p
  have hq1 := Set.mem_of_mem_inter_left hn.some_mem
  have hq2 := Set.mem_of_mem_inter_right hn.some_mem
  constructor
  · intro hp
    rw [← vsub_vadd p hn.some]
    refine vadd_mem_of_mem_direction ?_ hq2
    rw [← hd]
    exact vsub_mem_direction hp hq1
  · intro hp
    rw [← vsub_vadd p hn.some]
    refine vadd_mem_of_mem_direction ?_ hq1
    rw [hd]
    exact vsub_mem_direction hp hq2

Equality of Affine Subspaces with Common Direction and Nonempty Intersection

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s_1$ and $s_2$ be two affine subspaces of $P$. If $s_1$ and $s_2$ have the same direction (i.e., $s_1.\text{direction} = s_2.\text{direction}$) and their intersection is nonempty (i.e., $(s_1 \cap s_2).\text{Nonempty}$), then $s_1 = s_2$.

AffineSubspace.mk' definition

(p : P) (direction : Submodule k V) : AffineSubspace k P

Full source

/-- Construct an affine subspace from a point and a direction. -/
def mk' (p : P) (direction : Submodule k V) : AffineSubspace k P where
  carrier := { q | q -ᵥ p ∈ direction }
  smul_vsub_vadd_mem c p₁ p₂ p₃ hp₁ hp₂ hp₃ := by
    simpa [vadd_vsub_assoc] using
      direction.add_mem (direction.smul_mem c (direction.sub_mem hp₁ hp₂)) hp₃

Affine subspace from point and direction

Informal description

Given a point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, and a submodule $direction$ of $V$, the function constructs an affine subspace of $P$ consisting of all points $q$ such that the vector difference $q - p$ lies in $direction$.

AffineSubspace.mem_mk' theorem

(p q : P) (direction : Submodule k V) : q ∈ mk' p direction ↔ q -ᵥ p ∈ direction

Full source

@[simp]
theorem mem_mk' (p q : P) (direction : Submodule k V) : q ∈ mk' p directionq ∈ mk' p direction ↔ q -ᵥ p ∈ direction :=
  Iff.rfl

Membership Criterion for Affine Subspace Generated by Point and Direction

Informal description

Given an affine space $P$ over a module $V$ with scalar ring $k$, a point $p \in P$, and a submodule $direction$ of $V$, a point $q \in P$ belongs to the affine subspace generated by $p$ and $direction$ if and only if the vector difference $q - p$ lies in $direction$. In other words, for any points $p, q \in P$ and submodule $direction \subseteq V$, we have: $$ q \in \text{affineSubspace}(p, \text{direction}) \iff q - p \in \text{direction}. $$

AffineSubspace.self_mem_mk' theorem

(p : P) (direction : Submodule k V) : p ∈ mk' p direction

Full source

/-- An affine subspace constructed from a point and a direction contains that point. -/
theorem self_mem_mk' (p : P) (direction : Submodule k V) : p ∈ mk' p direction := by
  simp

Point Belongs to Affine Subspace Constructed from Itself and Direction

Informal description

Given a point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, and a submodule $direction$ of $V$, the point $p$ belongs to the affine subspace constructed from $p$ and $direction$.

AffineSubspace.vadd_mem_mk' theorem

{v : V} (p : P) {direction : Submodule k V} (hv : v ∈ direction) : v +ᵥ p ∈ mk' p direction

Full source

/-- An affine subspace constructed from a point and a direction contains the result of adding a
vector in that direction to that point. -/
theorem vadd_mem_mk' {v : V} (p : P) {direction : Submodule k V} (hv : v ∈ direction) :
    v +ᵥ pv +ᵥ p ∈ mk' p direction := by
  simpa

Point-Vector Addition in Affine Subspace Construction

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $p \in P$ be a point. For any submodule $\text{direction}$ of $V$ and any vector $v \in \text{direction}$, the point obtained by adding $v$ to $p$ (denoted $v + p$) lies in the affine subspace constructed from $p$ and $\text{direction}$.

AffineSubspace.mk'_nonempty theorem

(p : P) (direction : Submodule k V) : (mk' p direction : Set P).Nonempty

Full source

/-- An affine subspace constructed from a point and a direction is nonempty. -/
theorem mk'_nonempty (p : P) (direction : Submodule k V) : (mk' p direction : Set P).Nonempty :=
  ⟨p, self_mem_mk' p direction⟩

Nonemptiness of Affine Subspace Constructed from Point and Direction

Informal description

Given a point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, and a submodule $\text{direction}$ of $V$, the affine subspace constructed from $p$ and $\text{direction}$ is nonempty. Specifically, the set of points in this affine subspace is nonempty.

AffineSubspace.direction_mk' theorem

(p : P) (direction : Submodule k V) : (mk' p direction).direction = direction

Full source

/-- The direction of an affine subspace constructed from a point and a direction. -/
@[simp]
theorem direction_mk' (p : P) (direction : Submodule k V) :
    (mk' p direction).direction = direction := by
  ext v
  rw [mem_direction_iff_eq_vsub (mk'_nonempty _ _)]
  constructor
  · rintro ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    simpa using direction.sub_mem hp₁ hp₂
  · exact fun hv => ⟨v +ᵥ p, vadd_mem_mk' _ hv, p, self_mem_mk' _ _, (vadd_vsub _ _).symm⟩

Direction of Affine Subspace Constructed from Point and Direction Matches Given Direction

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$. Given a point $p \in P$ and a submodule $\text{direction}$ of $V$, the direction of the affine subspace constructed from $p$ and $\text{direction}$ is equal to $\text{direction}$ itself. In other words, if $s$ is the affine subspace defined as all points $q$ such that $q - p \in \text{direction}$, then the direction of $s$ is exactly $\text{direction}$.

AffineSubspace.mem_mk'_iff_vsub_mem theorem

{p₁ p₂ : P} {direction : Submodule k V} : p₂ ∈ mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction

Full source

/-- A point lies in an affine subspace constructed from another point and a direction if and only
if their difference is in that direction. -/
theorem mem_mk'_iff_vsub_mem {p₁ p₂ : P} {direction : Submodule k V} :
    p₂ ∈ mk' p₁ directionp₂ ∈ mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← direction_mk' p₁ direction]
    exact vsub_mem_direction h (self_mem_mk' _ _)
  · rw [← vsub_vadd p₂ p₁]
    exact vadd_mem_mk' p₁ h

Membership in Affine Subspace via Difference Vector

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $p_1, p_2 \in P$ be points. Given a submodule $\text{direction}$ of $V$, the point $p_2$ lies in the affine subspace constructed from $p_1$ and $\text{direction}$ if and only if the difference vector $p_2 - p_1$ lies in $\text{direction}$.

AffineSubspace.mk'_eq theorem

{s : AffineSubspace k P} {p : P} (hp : p ∈ s) : mk' p s.direction = s

Full source

/-- Constructing an affine subspace from a point in a subspace and that subspace's direction
yields the original subspace. -/
@[simp]
theorem mk'_eq {s : AffineSubspace k P} {p : P} (hp : p ∈ s) : mk' p s.direction = s :=
  ext_of_direction_eq (direction_mk' p s.direction) ⟨p, Set.mem_inter (self_mem_mk' _ _) hp⟩

Reconstruction of Affine Subspace from Point and Direction

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be an affine subspace of $P$. For any point $p \in s$, the affine subspace constructed from $p$ and the direction of $s$ is equal to $s$ itself. In other words, if $s$ is nonempty, then $s$ can be reconstructed from any of its points and its direction.

AffineSubspace.spanPoints_subset_coe_of_subset_coe theorem

{s : Set P} {s₁ : AffineSubspace k P} (h : s ⊆ s₁) : spanPoints k s ⊆ s₁

Full source

/-- If an affine subspace contains a set of points, it contains the `spanPoints` of that set. -/
theorem spanPoints_subset_coe_of_subset_coe {s : Set P} {s₁ : AffineSubspace k P} (h : s ⊆ s₁) :
    spanPointsspanPoints k s ⊆ s₁ := by
  rintro p ⟨p₁, hp₁, v, hv, hp⟩
  rw [hp]
  have hp₁s₁ : p₁ ∈ (s₁ : Set P) := Set.mem_of_mem_of_subset hp₁ h
  refine vadd_mem_of_mem_direction ?_ hp₁s₁
  have hs : vectorSpan k s ≤ s₁.direction := vectorSpan_mono k h
  rw [SetLike.le_def] at hs
  rw [← SetLike.mem_coe]
  exact Set.mem_of_mem_of_subset hv hs

Affine Span is Smallest Containing Subspace: $s \subseteq s_1 \Rightarrow \operatorname{spanPoints}_k s \subseteq s_1$

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a subset of $P$. For any affine subspace $s_1$ of $P$ containing $s$, the affine span of $s$ (denoted $\operatorname{spanPoints}_k s$) is contained in $s_1$. In other words, if $s \subseteq s_1$, then $\operatorname{spanPoints}_k s \subseteq s_1$.

Submodule.mem_toAffineSubspace theorem

{p : Submodule k V} {x : V} : x ∈ p.toAffineSubspace ↔ x ∈ p

Full source

@[simp]
theorem mem_toAffineSubspace {p : Submodule k V} {x : V} :
    x ∈ p.toAffineSubspacex ∈ p.toAffineSubspace ↔ x ∈ p :=
  Iff.rfl

Membership in Affine Subspace of Submodule

Informal description

For any submodule $p$ of a module $V$ over a ring $k$ and any vector $x \in V$, the vector $x$ belongs to the affine subspace corresponding to $p$ if and only if $x$ belongs to $p$ itself.

Submodule.toAffineSubspace_direction theorem

(s : Submodule k V) : s.toAffineSubspace.direction = s

Full source

@[simp]
theorem toAffineSubspace_direction (s : Submodule k V) : s.toAffineSubspace.direction = s := by
  ext x; simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]

Direction of Affine Subspace from Submodule Equals Submodule

Informal description

For any submodule $s$ of a module $V$ over a ring $k$, the direction of the affine subspace corresponding to $s$ is equal to $s$ itself. In other words, the submodule spanned by the pairwise differences of points in $s$ (viewed as an affine subspace) is exactly $s$.

affineSpan definition

(s : Set P) : AffineSubspace k P

Full source

/-- 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.) -/
def affineSpan (s : Set P) : AffineSubspace k P where
  carrier := spanPoints k s
  smul_vsub_vadd_mem c _ _ _ hp₁ hp₂ hp₃ :=
    vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan k hp₃
      ((vectorSpan k s).smul_mem c
        (vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints k hp₁ hp₂))

Affine span of a set of points

Informal description

Given a set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of $s$ is the smallest affine subspace of $P$ containing all points in $s$. More precisely, it consists of all points $p \in P$ such that there exists a point $p_1 \in s$ and a vector $v$ in the vector span of $s$ (the submodule of $V$ generated by differences of points in $s$) with $p = v + p_1$.

coe_affineSpan theorem

(s : Set P) : (affineSpan k s : Set P) = spanPoints k s

Full source

/-- The affine span, converted to a set, is `spanPoints`. -/
@[simp]
theorem coe_affineSpan (s : Set P) : (affineSpan k s : Set P) = spanPoints k s :=
  rfl

Affine Span as spanPoints Set Equality

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the set of points in the affine span of $s$ is equal to the set $\text{spanPoints}\ k\ s$, which consists of all points $p \in P$ such that there exists a point $p_1 \in s$ and a vector $v$ in the vector span of $s$ with $p = v + p_1$.

mem_affineSpan_iff_exists theorem

{p : P} {s : Set P} : p ∈ affineSpan k s ↔ ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, p = v +ᵥ p₁

Full source

/-- The condition for a point to be in the affine span, in terms of `vectorSpan`. -/
lemma mem_affineSpan_iff_exists {p : P} {s : Set P} : p ∈ affineSpan k sp ∈ affineSpan k s ↔
    ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, p = v +ᵥ p₁ :=
  Iff.rfl

Characterization of Points in Affine Span via Vector Span

Informal description

A point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$ belongs to the affine span of a set $s \subseteq P$ if and only if there exists a point $p_1 \in s$ and a vector $v$ in the vector span of $s$ such that $p = v + p_1$.

subset_affineSpan theorem

(s : Set P) : s ⊆ affineSpan k s

Full source

/-- A set is contained in its affine span. -/
theorem subset_affineSpan (s : Set P) : s ⊆ affineSpan k s :=
  subset_spanPoints k s

Set is Contained in its Affine Span

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the set $s$ is contained in its affine span, i.e., $s \subseteq \text{affineSpan}_k s$.

direction_affineSpan theorem

(s : Set P) : (affineSpan k s).direction = vectorSpan k s

Full source

/-- The direction of the affine span is the `vectorSpan`. -/
theorem direction_affineSpan (s : Set P) : (affineSpan k s).direction = vectorSpan k s := by
  apply le_antisymm
  · refine Submodule.span_le.2 ?_
    rintro v ⟨p₁, ⟨p₂, hp₂, v₁, hv₁, hp₁⟩, p₃, ⟨p₄, hp₄, v₂, hv₂, hp₃⟩, rfl⟩
    simp only [SetLike.mem_coe]
    rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]
    exact
      (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂
  · exact vectorSpan_mono k (subset_spanPoints k s)

Direction of Affine Span Equals Vector Span

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the direction of the affine span of $s$ is equal to the vector span of $s$. That is, $$ \text{direction}(\text{affineSpan}_k s) = \text{vectorSpan}_k s $$

mem_affineSpan theorem

{p : P} {s : Set P} (hp : p ∈ s) : p ∈ affineSpan k s

Full source

/-- A point in a set is in its affine span. -/
theorem mem_affineSpan {p : P} {s : Set P} (hp : p ∈ s) : p ∈ affineSpan k s :=
  mem_spanPoints k p s hp

Point in Set Belongs to its Affine Span

Informal description

For any point $p$ in a set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, $p$ is contained in the affine span of $s$, i.e., $p \in \text{affineSpan}_k s$.

vectorSpan_add_self theorem

(s : Set V) : (vectorSpan k s : Set V) + s = affineSpan k s

Full source

@[simp]
lemma vectorSpan_add_self (s : Set V) : (vectorSpan k s : Set V) + s = affineSpan k s := by
  ext
  simp [mem_add, spanPoints]
  aesop

Affine Span as Vector Span Plus Set in Module

Informal description

For any set $s$ of vectors in a module $V$ over a ring $k$, the sum of the vector span of $s$ and $s$ itself equals the affine span of $s$. That is, $\mathrm{vectorSpan}_k(s) + s = \mathrm{affineSpan}_k(s)$, where the addition denotes the Minkowski sum of sets.

vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan theorem

{s : Set P} {p : P} {v : V} (hp : p ∈ affineSpan k s) (hv : v ∈ vectorSpan k s) : v +ᵥ p ∈ affineSpan k s

Full source

/-- Adding a point in the affine span and a vector in the spanning submodule produces a point in the
affine span. -/
theorem vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan {s : Set P} {p : P} {v : V}
    (hp : p ∈ affineSpan k s) (hv : v ∈ vectorSpan k s) : v +ᵥ pv +ᵥ p ∈ affineSpan k s :=
  vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan k hp hv

Affine span is closed under translation by vectors in its direction

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a set of points in $P$. For any point $p$ in the affine span of $s$ and any vector $v$ in the vector span of $s$, the point $v + p$ (obtained by translating $p$ by $v$) is also in the affine span of $s$.

vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan theorem

 {s : Set P} {p₁ p₂ : P} (hp₁ : p₁ ∈ affineSpan k s) (hp₂ : p₂ ∈ affineSpan k s) : p₁ -ᵥ p₂ ∈ vectorSpan k s

Full source

/-- Subtracting two points in the affine span produces a vector in the spanning submodule. -/
theorem vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan {s : Set P} {p₁ p₂ : P}
    (hp₁ : p₁ ∈ affineSpan k s) (hp₂ : p₂ ∈ affineSpan k s) : p₁ -ᵥ p₂p₁ -ᵥ p₂ ∈ vectorSpan k s :=
  vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints k hp₁ hp₂

Difference of Points in Affine Span Belongs to Vector Span

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, and for any two points $p_1, p_2$ in the affine span of $s$, the difference vector $p_1 - p_2$ lies in the vector span of $s$.

affineSpan_le_of_subset_coe theorem

{s : Set P} {s₁ : AffineSubspace k P} (h : s ⊆ s₁) : affineSpan k s ≤ s₁

Full source

/-- If an affine subspace contains a set of points, it contains the affine span of that set. -/
theorem affineSpan_le_of_subset_coe {s : Set P} {s₁ : AffineSubspace k P} (h : s ⊆ s₁) :
    affineSpan k s ≤ s₁ :=
  AffineSubspace.spanPoints_subset_coe_of_subset_coe h

Affine span is the smallest containing subspace: $s \subseteq s_1 \Rightarrow \operatorname{affineSpan}_k s \leq s_1$

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a subset of $P$. For any affine subspace $s_1$ of $P$ containing $s$, the affine span of $s$ is contained in $s_1$.

AffineSubspace.instCompleteLattice instance

: CompleteLattice (AffineSubspace k P)

Full source

instance : CompleteLattice (AffineSubspace k P) :=
  {
    PartialOrder.lift ((↑) : AffineSubspace k P → Set P)
      coe_injective with
    sup := fun s₁ s₂ => affineSpan k (s₁ ∪ s₂)
    le_sup_left := fun _ _ =>
      Set.Subset.trans Set.subset_union_left (subset_spanPoints k _)
    le_sup_right := fun _ _ =>
      Set.Subset.trans Set.subset_union_right (subset_spanPoints k _)
    sup_le := fun _ _ _ hs₁ hs₂ => spanPoints_subset_coe_of_subset_coe (Set.union_subset hs₁ hs₂)
    inf := fun s₁ s₂ =>
      mk (s₁ ∩ s₂) fun c _ _ _ hp₁ hp₂ hp₃ =>
        ⟨s₁.smul_vsub_vadd_mem c hp₁.1 hp₂.1 hp₃.1, s₂.smul_vsub_vadd_mem c hp₁.2 hp₂.2 hp₃.2⟩
    inf_le_left := fun _ _ => Set.inter_subset_left
    inf_le_right := fun _ _ => Set.inter_subset_right
    le_sInf := fun S s₁ hs₁ => by
      apply Set.subset_sInter
      rintro t ⟨s, _hs, rfl⟩
      exact Set.subset_iInter (hs₁ s)
    top :=
      { carrier := Set.univ
        smul_vsub_vadd_mem := fun _ _ _ _ _ _ _ => Set.mem_univ _ }
    le_top := fun _ _ _ => Set.mem_univ _
    bot :=
      { carrier := ∅
        smul_vsub_vadd_mem := fun _ _ _ _ => False.elim }
    bot_le := fun _ _ => False.elim
    sSup := fun s => affineSpan k (⋃ s' ∈ s, (s' : Set P))
    sInf := fun s =>
      mk (⋂ s' ∈ s, (s' : Set P)) fun c p₁ p₂ p₃ hp₁ hp₂ hp₃ =>
        Set.mem_iInter₂.2 fun s₂ hs₂ => by
          rw [Set.mem_iInter₂] at *
          exact s₂.smul_vsub_vadd_mem c (hp₁ s₂ hs₂) (hp₂ s₂ hs₂) (hp₃ s₂ hs₂)
    le_sSup := fun _ _ h => Set.Subset.trans (Set.subset_biUnion_of_mem h) (subset_spanPoints k _)
    sSup_le := fun _ _ h => spanPoints_subset_coe_of_subset_coe (Set.iUnion₂_subset h)
    sInf_le := fun _ _ => Set.biInter_subset_of_mem
    le_inf := fun _ _ _ => Set.subset_inter }

Complete Lattice Structure on Affine Subspaces

Informal description

The collection of affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$ forms a complete lattice, where the partial order is given by inclusion of subsets, the infimum is the intersection of subspaces, and the supremum is the affine span of the union of subspaces.

AffineSubspace.instInhabited instance

: Inhabited (AffineSubspace k P)

Full source

instance : Inhabited (AffineSubspace k P) :=
  ⟨⊤⟩

Nonempty Collection of Affine Subspaces

Informal description

For any ring $k$, additive commutative group $V$ with a $k$-module structure, and affine space $P$ over $V$, the collection of affine subspaces of $P$ is nonempty.

AffineSubspace.le_def theorem

(s₁ s₂ : AffineSubspace k P) : s₁ ≤ s₂ ↔ (s₁ : Set P) ⊆ s₂

Full source

/-- The `≤` order on subspaces is the same as that on the corresponding sets. -/
theorem le_def (s₁ s₂ : AffineSubspace k P) : s₁ ≤ s₂ ↔ (s₁ : Set P) ⊆ s₂ :=
  Iff.rfl

Partial Order on Affine Subspaces Corresponds to Subset Inclusion

Informal description

For any two affine subspaces $s₁$ and $s₂$ of an affine space $P$ over a module $V$ with scalar ring $k$, the partial order relation $s₁ \leq s₂$ holds if and only if the underlying set of $s₁$ is a subset of the underlying set of $s₂$.

AffineSubspace.le_def' theorem

(s₁ s₂ : AffineSubspace k P) : s₁ ≤ s₂ ↔ ∀ p ∈ s₁, p ∈ s₂

Full source

/-- One subspace is less than or equal to another if and only if all its points are in the second
subspace. -/
theorem le_def' (s₁ s₂ : AffineSubspace k P) : s₁ ≤ s₂ ↔ ∀ p ∈ s₁, p ∈ s₂ :=
  Iff.rfl

Containment of Affine Subspaces via Point Membership

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, the subspace $s_1$ is contained in $s_2$ if and only if every point in $s_1$ is also in $s_2$. In other words, $s_1 \leq s_2 \iff \forall p \in s_1, p \in s_2$.

AffineSubspace.lt_def theorem

(s₁ s₂ : AffineSubspace k P) : s₁ < s₂ ↔ (s₁ : Set P) ⊂ s₂

Full source

/-- The `<` order on subspaces is the same as that on the corresponding sets. -/
theorem lt_def (s₁ s₂ : AffineSubspace k P) : s₁ < s₂ ↔ (s₁ : Set P) ⊂ s₂ :=
  Iff.rfl

Strict Order on Affine Subspaces Corresponds to Strict Set Inclusion

Informal description

For any two affine subspaces $s₁$ and $s₂$ of an affine space $P$ over a module $V$ with scalar ring $k$, the strict order relation $s₁ < s₂$ holds if and only if the underlying set of $s₁$ is a strict subset of the underlying set of $s₂$.

AffineSubspace.not_le_iff_exists theorem

(s₁ s₂ : AffineSubspace k P) : ¬s₁ ≤ s₂ ↔ ∃ p ∈ s₁, p ∉ s₂

Full source

/-- One subspace is not less than or equal to another if and only if it has a point not in the
second subspace. -/
theorem not_le_iff_exists (s₁ s₂ : AffineSubspace k P) : ¬s₁ ≤ s₂¬s₁ ≤ s₂ ↔ ∃ p ∈ s₁, p ∉ s₂ :=
  Set.not_subset

Characterization of Non-Inclusion of Affine Subspaces

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, the statement that $s_1$ is not contained in $s_2$ is equivalent to the existence of a point $p \in s_1$ such that $p \notin s_2$. In other words, $\neg (s_1 \leq s_2) \leftrightarrow \exists p \in s_1, p \notin s_2$.

AffineSubspace.exists_of_lt theorem

{s₁ s₂ : AffineSubspace k P} (h : s₁ < s₂) : ∃ p ∈ s₂, p ∉ s₁

Full source

/-- If a subspace is less than another, there is a point only in the second. -/
theorem exists_of_lt {s₁ s₂ : AffineSubspace k P} (h : s₁ < s₂) : ∃ p ∈ s₂, p ∉ s₁ :=
  Set.exists_of_ssubset h

Existence of Point in Strictly Larger Affine Subspace

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, if $s_1$ is strictly contained in $s_2$ (i.e., $s_1 < s_2$), then there exists a point $p \in s_2$ that is not in $s_1$.

AffineSubspace.lt_iff_le_and_exists theorem

(s₁ s₂ : AffineSubspace k P) : s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

Full source

/-- 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. -/
theorem lt_iff_le_and_exists (s₁ s₂ : AffineSubspace k P) :
    s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁ := by
  rw [lt_iff_le_not_le, not_le_iff_exists]

Characterization of Strict Inclusion for Affine Subspaces

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, the strict inclusion $s_1 < s_2$ holds if and only if $s_1$ is contained in $s_2$ (i.e., $s_1 \leq s_2$) and there exists a point $p \in s_2$ that is not in $s_1$.

AffineSubspace.affineSpan_eq_sInf theorem

(s : Set P) : affineSpan k s = sInf {s' : AffineSubspace k P | s ⊆ s'}

Full source

/-- The affine span is the `sInf` of subspaces containing the given points. -/
theorem affineSpan_eq_sInf (s : Set P) :
    affineSpan k s = sInf { s' : AffineSubspace k P | s ⊆ s' } :=
  le_antisymm (affineSpan_le_of_subset_coe <| Set.subset_iInter₂ fun _ => id)
    (sInf_le (subset_spanPoints k _))

Affine Span as Infimum of Containing Subspaces

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of $s$ is equal to the infimum of all affine subspaces of $P$ that contain $s$. In other words, $\operatorname{affineSpan}_k s = \bigwedge \{s' \mid s \subseteq s'\}$, where the infimum is taken over all affine subspaces $s'$ containing $s$.

AffineSubspace.gi definition

: GaloisInsertion (affineSpan k) ((↑) : AffineSubspace k P → Set P)

Full source

/-- The Galois insertion formed by `affineSpan` and coercion back to a set. -/
protected def gi : GaloisInsertion (affineSpan k) ((↑) : AffineSubspace k P → Set P) where
  choice s _ := affineSpan k s
  gc s₁ _s₂ :=
    ⟨fun h => Set.Subset.trans (subset_spanPoints k s₁) h, affineSpan_le_of_subset_coe⟩
  le_l_u _ := subset_spanPoints k _
  choice_eq _ _ := rfl

Galois insertion between affine span and coercion to sets

Informal description

The Galois insertion between the `affineSpan` function and the coercion from affine subspaces to sets. Specifically, for any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of $s$ is the smallest affine subspace containing $s$, and the coercion maps an affine subspace back to its underlying set of points. This forms a Galois insertion, meaning that for any set $s$ and affine subspace $S$, we have: \[ \text{affineSpan}\ k\ s \leq S \iff s \subseteq S \] where the order on affine subspaces is given by inclusion.

AffineSubspace.span_empty theorem

: affineSpan k (∅ : Set P) = ⊥

Full source

/-- The span of the empty set is `⊥`. -/
@[simp]
theorem span_empty : affineSpan k (∅ : Set P) = ⊥ :=
  (AffineSubspace.gi k V P).gc.l_bot

Affine Span of Empty Set is Bottom Subspace

Informal description

The affine span of the empty set in an affine space $P$ over a module $V$ with scalar ring $k$ is equal to the bottom element $\bot$ of the complete lattice of affine subspaces of $P$.

AffineSubspace.span_univ theorem

: affineSpan k (Set.univ : Set P) = ⊤

Full source

/-- The span of `univ` is `⊤`. -/
@[simp]
theorem span_univ : affineSpan k (Set.univ : Set P) = ⊤ :=
  eq_top_iff.2 <| subset_affineSpan k _

Affine Span of Universal Set is Entire Space

Informal description

The affine span of the universal set in an affine space $P$ over a module $V$ with scalar ring $k$ is equal to the entire affine space, i.e., $\text{affineSpan}_k (\text{univ}) = \top$.

affineSpan_le theorem

{s : Set P} {Q : AffineSubspace k P} : affineSpan k s ≤ Q ↔ s ⊆ (Q : Set P)

Full source

theorem _root_.affineSpan_le {s : Set P} {Q : AffineSubspace k P} :
    affineSpanaffineSpan k s ≤ Q ↔ s ⊆ (Q : Set P) :=
  (AffineSubspace.gi k V P).gc _ _

Affine Span Containment Criterion: $\text{affineSpan}(s) \leq Q \leftrightarrow s \subseteq Q$

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, and for any affine subspace $Q$ of $P$, the affine span of $s$ is contained in $Q$ if and only if $s$ is a subset of $Q$ (when viewed as a set of points).

AffineSubspace.span_union theorem

(s t : Set P) : affineSpan k (s ∪ t) = affineSpan k s ⊔ affineSpan k t

Full source

/-- The span of a union of sets is the sup of their spans. -/
theorem span_union (s t : Set P) : affineSpan k (s ∪ t) = affineSpanaffineSpan k s ⊔ affineSpan k t :=
  (AffineSubspace.gi k V P).gc.l_sup

Affine Span of Union Equals Supremum of Affine Spans

Informal description

For any two sets $s$ and $t$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of their union $s \cup t$ is equal to the supremum (in the lattice of affine subspaces) of the affine spans of $s$ and $t$ individually. In other words: \[ \text{affineSpan}_k(s \cup t) = \text{affineSpan}_k(s) \sqcup \text{affineSpan}_k(t) \] where $\sqcup$ denotes the join operation in the lattice of affine subspaces.

AffineSubspace.span_iUnion theorem

{ι : Type*} (s : ι → Set P) : affineSpan k (⋃ i, s i) = ⨆ i, affineSpan k (s i)

Full source

/-- The span of a union of an indexed family of sets is the sup of their spans. -/
theorem span_iUnion {ι : Type*} (s : ι → Set P) :
    affineSpan k (⋃ i, s i) = ⨆ i, affineSpan k (s i) :=
  (AffineSubspace.gi k V P).gc.l_iSup

Affine Span of Union Equals Supremum of Affine Spans

Informal description

For any indexed family of sets $(s_i)_{i \in \iota}$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of the union $\bigcup_i s_i$ is equal to the supremum of the affine spans of the individual sets $s_i$. In other words: \[ \text{affineSpan}_k \left( \bigcup_{i \in \iota} s_i \right) = \bigsqcup_{i \in \iota} \text{affineSpan}_k (s_i) \]

AffineSubspace.top_coe theorem

: ((⊤ : AffineSubspace k P) : Set P) = Set.univ

Full source

/-- `⊤`, coerced to a set, is the whole set of points. -/
@[simp]
theorem top_coe : ((⊤ : AffineSubspace k P) : Set P) = Set.univ :=
  rfl

Top Affine Subspace Equals Universal Set

Informal description

The set of points in the top affine subspace (i.e., the entire affine space $P$) is equal to the universal set of all points in $P$.

AffineSubspace.mem_top theorem

(p : P) : p ∈ (⊤ : AffineSubspace k P)

Full source

/-- All points are in `⊤`. -/
@[simp]
theorem mem_top (p : P) : p ∈ (⊤ : AffineSubspace k P) :=
  Set.mem_univ p

Every Point Belongs to the Top Affine Subspace

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, $p$ belongs to the top affine subspace $\top$ of $P$.

AffineSubspace.mk'_top theorem

(p : P) : mk' p (⊤ : Submodule k V) = ⊤

Full source

@[simp] lemma mk'_top (p : P) : mk' p (⊤ : Submodule k V) = ⊤ := by
  ext x
  simp [mem_mk'_iff_vsub_mem]

Affine Subspace Construction with Full Direction Yields Entire Space

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, the affine subspace constructed from $p$ with the full submodule $\top$ of $V$ as its direction is equal to the top affine subspace $\top$ (which is the entire space $P$).

AffineSubspace.direction_top theorem

: (⊤ : AffineSubspace k P).direction = ⊤

Full source

/-- The direction of `⊤` is the whole module as a submodule. -/
@[simp]
theorem direction_top : (⊤ : AffineSubspace k P).direction = ⊤ := by
  obtain ⟨p⟩ := S.nonempty
  ext v
  refine ⟨imp_intro Submodule.mem_top, fun _hv => ?_⟩
  have hpv : ((v +ᵥ p) -ᵥ p : V) ∈ (⊤ : AffineSubspace k P).direction :=
    vsub_mem_direction (mem_top k V _) (mem_top k V _)
  rwa [vadd_vsub] at hpv

Direction of Top Affine Subspace is Entire Module

Informal description

The direction of the top affine subspace $\top$ of an affine space $P$ over a module $V$ with scalar ring $k$ is equal to the entire module $V$ (i.e., the top submodule $\top$ of $V$).

AffineSubspace.bot_coe theorem

: ((⊥ : AffineSubspace k P) : Set P) = ∅

Full source

/-- `⊥`, coerced to a set, is the empty set. -/
@[simp]
theorem bot_coe : ((⊥ : AffineSubspace k P) : Set P) = ∅ :=
  rfl

Bottom Affine Subspace is the Empty Set

Informal description

The bottom element of the complete lattice of affine subspaces of $P$ over $V$ with scalar ring $k$, when coerced to a set, is equal to the empty set. In other words, $\bot = \emptyset$ as subsets of $P$.

AffineSubspace.bot_ne_top theorem

: (⊥ : AffineSubspace k P) ≠ ⊤

Full source

theorem bot_ne_top : (⊥ : AffineSubspace k P) ≠ ⊤ := by
  intro contra
  rw [AffineSubspace.ext_iff, bot_coe, top_coe] at contra
  exact Set.empty_ne_univ contra

Non-triviality of Affine Subspace Lattice: $\bot \neq \top$

Informal description

The bottom affine subspace (the empty set) is not equal to the top affine subspace (the entire affine space $P$) in the lattice of affine subspaces of $P$ over $V$ with scalar ring $k$.

AffineSubspace.instNontrivial instance

: Nontrivial (AffineSubspace k P)

Full source

instance : Nontrivial (AffineSubspace k P) :=
  ⟨⟨⊥, ⊤, bot_ne_top k V P⟩⟩

Nontriviality of the Affine Subspace Lattice

Informal description

The lattice of affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$ is nontrivial, meaning it contains at least two distinct elements.

AffineSubspace.nonempty_of_affineSpan_eq_top theorem

{s : Set P} (h : affineSpan k s = ⊤) : s.Nonempty

Full source

theorem nonempty_of_affineSpan_eq_top {s : Set P} (h : affineSpan k s = ⊤) : s.Nonempty := by
  rw [Set.nonempty_iff_ne_empty]
  rintro rfl
  rw [AffineSubspace.span_empty] at h
  exact bot_ne_top k V P h

Nonempty Set Condition for Affine Span to Equal Entire Space

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, if the affine span of $s$ equals the entire space $P$, then $s$ is nonempty.

AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top theorem

{s : Set P} (h : affineSpan k s = ⊤) : vectorSpan k s = ⊤

Full source

/-- If the affine span of a set is `⊤`, then the vector span of the same set is the `⊤`. -/
theorem vectorSpan_eq_top_of_affineSpan_eq_top {s : Set P} (h : affineSpan k s = ⊤) :
    vectorSpan k s = ⊤ := by rw [← direction_affineSpan, h, direction_top]

Vector Span is Entire Module When Affine Span is Entire Space

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, if the affine span of $s$ is equal to the entire space $P$ (i.e., $\text{affineSpan}_k s = \top$), then the vector span of $s$ is equal to the entire module $V$ (i.e., $\text{vectorSpan}_k s = \top$).

AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty theorem

{s : Set P} (hs : s.Nonempty) : affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Full source

/-- For a nonempty set, the affine span is `⊤` iff its vector span is `⊤`. -/
theorem affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty {s : Set P} (hs : s.Nonempty) :
    affineSpanaffineSpan k s = ⊤ ↔ vectorSpan k s = ⊤ := by
  refine ⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, ?_⟩
  intro h
  suffices Nonempty (affineSpan k s) by
    obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
    rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
  obtain ⟨x, hx⟩ := hs
  exact ⟨⟨x, mem_affineSpan k hx⟩⟩

Affine Span Equals Entire Space iff Vector Span Equals Entire Module for Nonempty Sets

Informal description

For a nonempty set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of $s$ equals the entire space $P$ if and only if the vector span of $s$ equals the entire module $V$. In other words, $$ \text{affineSpan}_k s = \top \leftrightarrow \text{vectorSpan}_k s = \top $$

AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial theorem

{s : Set P} [Nontrivial P] : affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Full source

/-- For a non-trivial space, the affine span of a set is `⊤` iff its vector span is `⊤`. -/
theorem affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial {s : Set P} [Nontrivial P] :
    affineSpanaffineSpan k s = ⊤ ↔ vectorSpan k s = ⊤ := by
  rcases s.eq_empty_or_nonempty with hs | hs
  · simp [hs, subsingleton_iff_bot_eq_top, AddTorsor.subsingleton_iff V P, not_subsingleton]
  · rw [affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty k V P hs]

Affine Span Equals Space iff Vector Span Equals Module in Nontrivial Affine Space

Informal description

For a nontrivial affine space $P$ over a module $V$ with scalar ring $k$, and for any set $s$ of points in $P$, the affine span of $s$ equals the entire space $P$ if and only if the vector span of $s$ equals the entire module $V$. In other words, $$\text{affineSpan}_k(s) = P \leftrightarrow \text{vectorSpan}_k(s) = V.$$

AffineSubspace.card_pos_of_affineSpan_eq_top theorem

{ι : Type*} [Fintype ι] {p : ι → P} (h : affineSpan k (range p) = ⊤) : 0 < Fintype.card ι

Full source

theorem card_pos_of_affineSpan_eq_top {ι : Type*} [Fintype ι] {p : ι → P}
    (h : affineSpan k (range p) = ⊤) : 0 < Fintype.card ι := by
  obtain ⟨-, ⟨i, -⟩⟩ := nonempty_of_affineSpan_eq_top k V P h
  exact Fintype.card_pos_iff.mpr ⟨i⟩

Nonempty Index Set for Affine Span Covering Entire Space

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $\{p_i\}_{i \in \iota}$ be a finite family of points in $P$ indexed by a finite type $\iota$. If the affine span of the range of $p$ equals the entire space $P$, then the cardinality of $\iota$ is positive, i.e., $\text{card}(\iota) > 0$.

AffineSubspace.instNonemptySubtypeMemTop instance

: Nonempty (⊤ : AffineSubspace k P)

Full source

instance : Nonempty (⊤ : AffineSubspace k P) := inferInstanceAs (Nonempty (⊤ : Set P))

Nonemptiness of the Top Affine Subspace

Informal description

The top element in the lattice of affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$ is nonempty. In other words, the entire affine space $P$ itself, considered as an affine subspace, contains at least one point.

AffineSubspace.not_mem_bot theorem

(p : P) : p ∉ (⊥ : AffineSubspace k P)

Full source

/-- No points are in `⊥`. -/
theorem not_mem_bot (p : P) : p ∉ (⊥ : AffineSubspace k P) :=
  Set.not_mem_empty p

No Points in the Empty Affine Subspace

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, $p$ does not belong to the bottom affine subspace $\bot$ (the empty affine subspace).

AffineSubspace.isEmpty_bot instance

: IsEmpty (⊥ : AffineSubspace k P)

Full source

instance isEmpty_bot : IsEmpty (⊥ : AffineSubspace k P) :=
  Subtype.isEmpty_of_false fun _ ↦ not_mem_bot _ _ _

The Empty Affine Subspace is Empty

Informal description

The empty affine subspace $\bot$ of an affine space $P$ over a module $V$ with scalar ring $k$ has no points.

AffineSubspace.direction_bot theorem

: (⊥ : AffineSubspace k P).direction = ⊥

Full source

/-- The direction of `⊥` is the submodule `⊥`. -/
@[simp]
theorem direction_bot : (⊥ : AffineSubspace k P).direction = ⊥ := by
  rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]

Direction of Empty Affine Subspace is Trivial Submodule

Informal description

The direction of the empty affine subspace $\bot$ of an affine space $P$ over a module $V$ with scalar ring $k$ is the trivial submodule $\bot$ of $V$.

AffineSubspace.coe_eq_bot_iff theorem

(Q : AffineSubspace k P) : (Q : Set P) = ∅ ↔ Q = ⊥

Full source

@[simp]
theorem coe_eq_bot_iff (Q : AffineSubspace k P) : (Q : Set P) = ∅ ↔ Q = ⊥ :=
  coe_injective.eq_iff' (bot_coe _ _ _)

Characterization of Empty Affine Subspace as Bottom Element

Informal description

For any affine subspace $Q$ of an affine space $P$ over a module $V$ with scalar ring $k$, the underlying set of points of $Q$ is empty if and only if $Q$ is the bottom element of the complete lattice of affine subspaces (i.e., the empty affine subspace). In symbols: $(Q : \text{Set } P) = \emptyset \leftrightarrow Q = \bot$.

AffineSubspace.coe_eq_univ_iff theorem

(Q : AffineSubspace k P) : (Q : Set P) = univ ↔ Q = ⊤

Full source

@[simp]
theorem coe_eq_univ_iff (Q : AffineSubspace k P) : (Q : Set P) = univ ↔ Q = ⊤ :=
  coe_injective.eq_iff' (top_coe _ _ _)

Characterization of Universal Affine Subspace as Top Element

Informal description

For any affine subspace $Q$ of an affine space $P$ over a module $V$ with scalar ring $k$, the set of points in $Q$ is equal to the universal set of all points in $P$ if and only if $Q$ is the top affine subspace (i.e., $Q$ is equal to the entire affine space $P$).

AffineSubspace.nonempty_iff_ne_bot theorem

(Q : AffineSubspace k P) : (Q : Set P).Nonempty ↔ Q ≠ ⊥

Full source

theorem nonempty_iff_ne_bot (Q : AffineSubspace k P) : (Q : Set P).Nonempty ↔ Q ≠ ⊥ := by
  rw [nonempty_iff_ne_empty]
  exact not_congr Q.coe_eq_bot_iff

Nonempty Affine Subspace Characterization: $Q \neq \bot$

Informal description

For any affine subspace $Q$ of an affine space $P$ over a module $V$ with scalar ring $k$, the set of points in $Q$ is nonempty if and only if $Q$ is not the bottom element (empty affine subspace) of the complete lattice of affine subspaces. In symbols: $(Q : \text{Set } P) \neq \emptyset \leftrightarrow Q \neq \bot$.

AffineSubspace.direction_eq_top_iff_of_nonempty theorem

{s : AffineSubspace k P} (h : (s : Set P).Nonempty) : s.direction = ⊤ ↔ s = ⊤

Full source

/-- A nonempty affine subspace is `⊤` if and only if its direction is `⊤`. -/
@[simp]
theorem direction_eq_top_iff_of_nonempty {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    s.direction = ⊤ ↔ s = ⊤ := by
  constructor
  · intro hd
    rw [← direction_top k V P] at hd
    refine ext_of_direction_eq hd ?_
    simp [h]
  · rintro rfl
    simp

Characterization of Top Affine Subspace via Direction: Nonempty Case

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a nonempty affine subspace of $P$. Then the direction of $s$ is equal to the entire module $V$ if and only if $s$ is the entire affine space $P$. In symbols: $\text{direction}(s) = \top \leftrightarrow s = \top$.

AffineSubspace.inf_coe theorem

(s₁ s₂ : AffineSubspace k P) : (s₁ ⊓ s₂ : Set P) = (s₁ : Set P) ∩ s₂

Full source

/-- The inf of two affine subspaces, coerced to a set, is the intersection of the two sets of
points. -/
@[simp]
theorem inf_coe (s₁ s₂ : AffineSubspace k P) : (s₁ ⊓ s₂ : Set P) = (s₁ : Set P) ∩ s₂ :=
  rfl

Intersection of Affine Subspaces as Infimum

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, the set of points in their infimum $s_1 \sqcap s_2$ is equal to the intersection of the sets of points in $s_1$ and $s_2$. In other words, $(s_1 \sqcap s_2) = s_1 \cap s_2$ as subsets of $P$.

AffineSubspace.mem_inf_iff theorem

(p : P) (s₁ s₂ : AffineSubspace k P) : p ∈ s₁ ⊓ s₂ ↔ p ∈ s₁ ∧ p ∈ s₂

Full source

/-- A point is in the inf of two affine subspaces if and only if it is in both of them. -/
theorem mem_inf_iff (p : P) (s₁ s₂ : AffineSubspace k P) : p ∈ s₁ ⊓ s₂p ∈ s₁ ⊓ s₂ ↔ p ∈ s₁ ∧ p ∈ s₂ :=
  Iff.rfl

Membership in Infimum of Affine Subspaces is Intersection of Memberships

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, and for any two affine subspaces $s_1$ and $s_2$ of $P$, the point $p$ belongs to the infimum $s_1 \sqcap s_2$ if and only if $p$ belongs to both $s_1$ and $s_2$.

AffineSubspace.direction_inf theorem

(s₁ s₂ : AffineSubspace k P) : (s₁ ⊓ s₂).direction ≤ s₁.direction ⊓ s₂.direction

Full source

/-- The direction of the inf of two affine subspaces is less than or equal to the inf of their
directions. -/
theorem direction_inf (s₁ s₂ : AffineSubspace k P) :
    (s₁ ⊓ s₂).direction ≤ s₁.direction ⊓ s₂.direction := by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact
    le_inf (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_left) hp)
      (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_right) hp)

Direction of Infimum of Affine Subspaces is Contained in Infimum of Directions

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, the direction of their infimum $s_1 \sqcap s_2$ is a submodule of the infimum of their directions. In other words, the subspace spanned by the pairwise differences of points in $s_1 \sqcap s_2$ is contained in the intersection of the subspaces spanned by the pairwise differences of points in $s_1$ and $s_2$.

AffineSubspace.direction_inf_of_mem theorem

 {s₁ s₂ : AffineSubspace k P} {p : P} (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) : (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

Full source

/-- If two affine subspaces have a point in common, the direction of their inf equals the inf of
their directions. -/
theorem direction_inf_of_mem {s₁ s₂ : AffineSubspace k P} {p : P} (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) :
    (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction := by
  ext v
  rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
    vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]

Direction of Intersection of Affine Subspaces with Common Point

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s_1$ and $s_2$ be affine subspaces of $P$. If there exists a point $p \in P$ that belongs to both $s_1$ and $s_2$, then the direction of their intersection $s_1 \sqcap s_2$ equals the intersection of their directions, i.e., \[ \text{direction}(s_1 \sqcap s_2) = \text{direction}(s_1) \sqcap \text{direction}(s_2). \]

AffineSubspace.direction_inf_of_mem_inf theorem

 {s₁ s₂ : AffineSubspace k P} {p : P} (h : p ∈ s₁ ⊓ s₂) : (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

Full source

/-- If two affine subspaces have a point in their inf, the direction of their inf equals the inf of
their directions. -/
theorem direction_inf_of_mem_inf {s₁ s₂ : AffineSubspace k P} {p : P} (h : p ∈ s₁ ⊓ s₂) :
    (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction :=
  direction_inf_of_mem ((mem_inf_iff p s₁ s₂).1 h).1 ((mem_inf_iff p s₁ s₂).1 h).2

Direction of Intersection of Affine Subspaces with Common Point Equals Intersection of Directions

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s_1$ and $s_2$ be affine subspaces of $P$. If there exists a point $p \in P$ that belongs to both $s_1$ and $s_2$, then the direction of their intersection $s_1 \cap s_2$ equals the intersection of their directions, i.e., \[ \text{direction}(s_1 \cap s_2) = \text{direction}(s_1) \cap \text{direction}(s_2). \]

AffineSubspace.direction_le theorem

{s₁ s₂ : AffineSubspace k P} (h : s₁ ≤ s₂) : s₁.direction ≤ s₂.direction

Full source

/-- If one affine subspace is less than or equal to another, the same applies to their
directions. -/
theorem direction_le {s₁ s₂ : AffineSubspace k P} (h : s₁ ≤ s₂) : s₁.direction ≤ s₂.direction := by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact vectorSpan_mono k h

Direction Submodule Inclusion under Affine Subspace Containment

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, if $s_1$ is contained in $s_2$ (i.e., $s_1 \leq s_2$), then the direction of $s_1$ is a submodule of the direction of $s_2$, i.e., $s_1.\text{direction} \leq s_2.\text{direction}$.

AffineSubspace.sup_direction_le theorem

(s₁ s₂ : AffineSubspace k P) : s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction

Full source

/-- The sup of the directions of two affine subspaces is less than or equal to the direction of
their sup. -/
theorem sup_direction_le (s₁ s₂ : AffineSubspace k P) :
    s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction := by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact
    sup_le
      (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_left : s₁ ≤ s₁ ⊔ s₂)) hp)
      (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_right : s₂ ≤ s₁ ⊔ s₂)) hp)

Supremum of Directions is Contained in Direction of Supremum for Affine Subspaces

Informal description

For any two affine subspaces $s_1$ and $s_2$ of an affine space $P$ over a module $V$ with scalar ring $k$, the supremum of their direction submodules is contained in the direction of their affine span. In other words, the submodule $s_1.\text{direction} \sqcup s_2.\text{direction}$ is a submodule of $(s_1 \sqcup s_2).\text{direction}$. Here, the direction of an affine subspace is the submodule spanned by the pairwise differences of its points, and the affine span is the smallest affine subspace containing both $s_1$ and $s_2$.

AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty theorem

 {s₁ s₂ : AffineSubspace k P} (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty) (he : (s₁ ∩ s₂ : Set P) = ∅) :
  s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Full source

/-- The sup of the directions of two nonempty affine subspaces with empty intersection is less than
the direction of their sup. -/
theorem sup_direction_lt_of_nonempty_of_inter_empty {s₁ s₂ : AffineSubspace k P}
    (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty) (he : (s₁ ∩ s₂ : Set P) = ∅) :
    s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction := by
  obtain ⟨p₁, hp₁⟩ := h1
  obtain ⟨p₂, hp₂⟩ := h2
  rw [SetLike.lt_iff_le_and_exists]
  use sup_direction_le s₁ s₂, p₂ -ᵥ p₁,
    vsub_mem_direction ((le_sup_right : s₂ ≤ s₁ ⊔ s₂) hp₂) ((le_sup_left : s₁ ≤ s₁ ⊔ s₂) hp₁)
  intro h
  rw [Submodule.mem_sup] at h
  rcases h with ⟨v₁, hv₁, v₂, hv₂, hv₁v₂⟩
  rw [← sub_eq_zero, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm v₁, add_assoc, ←
    vadd_vsub_assoc, ← neg_neg v₂, add_comm, ← sub_eq_add_neg, ← vsub_vadd_eq_vsub_sub,
    vsub_eq_zero_iff_eq] at hv₁v₂
  refine Set.Nonempty.ne_empty ?_ he
  use v₁ +ᵥ p₁, vadd_mem_of_mem_direction hv₁ hp₁
  rw [hv₁v₂]
  exact vadd_mem_of_mem_direction (Submodule.neg_mem _ hv₂) hp₂

Strict Supremum of Directions for Disjoint Nonempty Affine Subspaces

Informal description

Let $s_1$ and $s_2$ be nonempty affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$. If the intersection of $s_1$ and $s_2$ is empty, then the supremum of their direction submodules is strictly contained in the direction of their affine span, i.e., $s_1.\text{direction} \sqcup s_2.\text{direction} < (s_1 \sqcup s_2).\text{direction}$.

AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top theorem

 {s₁ s₂ : AffineSubspace k P} (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty)
  (hd : s₁.direction ⊔ s₂.direction = ⊤) : ((s₁ : Set P) ∩ s₂).Nonempty

Full source

/-- If the directions of two nonempty affine subspaces span the whole module, they have nonempty
intersection. -/
theorem inter_nonempty_of_nonempty_of_sup_direction_eq_top {s₁ s₂ : AffineSubspace k P}
    (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty)
    (hd : s₁.direction ⊔ s₂.direction = ⊤) : ((s₁ : Set P) ∩ s₂).Nonempty := by
  by_contra h
  rw [Set.not_nonempty_iff_eq_empty] at h
  have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 h
  rw [hd] at hlt
  exact not_top_lt hlt

Nonempty Intersection of Affine Subspaces with Spanning Directions

Informal description

Let $s_1$ and $s_2$ be nonempty affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$. If the sum of their direction submodules spans the entire module $V$ (i.e., $s_1.\text{direction} \sqcup s_2.\text{direction} = \top$), then their intersection is nonempty.

AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl theorem

 {s₁ s₂ : AffineSubspace k P} (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty)
  (hd : IsCompl s₁.direction s₂.direction) : ∃ p, (s₁ : Set P) ∩ s₂ = { p }

Full source

/-- If the directions of two nonempty affine subspaces are complements of each other, they intersect
in exactly one point. -/
theorem inter_eq_singleton_of_nonempty_of_isCompl {s₁ s₂ : AffineSubspace k P}
    (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty)
    (hd : IsCompl s₁.direction s₂.direction) : ∃ p, (s₁ : Set P) ∩ s₂ = {p} := by
  obtain ⟨p, hp⟩ := inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top
  use p
  ext q
  rw [Set.mem_singleton_iff]
  constructor
  · rintro ⟨hq1, hq2⟩
    have hqp : q -ᵥ pq -ᵥ p ∈ s₁.direction ⊓ s₂.direction :=
      ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩
    rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp
  · exact fun h => h.symm ▸ hp

Unique Intersection of Nonempty Affine Subspaces with Complementary Directions

Informal description

Let $s_1$ and $s_2$ be nonempty affine subspaces of an affine space $P$ over a module $V$ with scalar ring $k$. If their direction submodules are complements of each other (i.e., $s_1.\text{direction} \sqcap s_2.\text{direction} = \bot$ and $s_1.\text{direction} \sqcup s_2.\text{direction} = \top$), then their intersection consists of exactly one point, i.e., there exists a point $p \in P$ such that $s_1 \cap s_2 = \{p\}$.

AffineSubspace.affineSpan_coe theorem

(s : AffineSubspace k P) : affineSpan k (s : Set P) = s

Full source

/-- Coercing a subspace to a set then taking the affine span produces the original subspace. -/
@[simp]
theorem affineSpan_coe (s : AffineSubspace k P) : affineSpan k (s : Set P) = s := by
  refine le_antisymm ?_ (subset_affineSpan _ _)
  rintro p ⟨p₁, hp₁, v, hv, rfl⟩
  exact vadd_mem_of_mem_direction hv hp₁

Affine Span of Subspace Equals Itself

Informal description

For any affine subspace $s$ of an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of the set of points in $s$ is equal to $s$ itself, i.e., $\text{affineSpan}_k (s) = s$.

affineSpan_nonempty theorem

: (affineSpan k s : Set P).Nonempty ↔ s.Nonempty

Full source

/-- The affine span of a set is nonempty if and only if that set is. -/
theorem affineSpan_nonempty : (affineSpan k s : Set P).Nonempty ↔ s.Nonempty :=
  spanPoints_nonempty k s

Nonemptiness of Affine Span Equivalence

Informal description

For any set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span $\operatorname{affineSpan}_k(s)$ is nonempty if and only if $s$ is nonempty.

instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem instance

[Nonempty s] : Nonempty (affineSpan k s)

Full source

/-- The affine span of a nonempty set is nonempty. -/
instance [Nonempty s] : Nonempty (affineSpan k s) :=
  ((nonempty_coe_sort.1 ‹_›).affineSpan _).to_subtype

Nonemptiness of Affine Span for Nonempty Sets

Informal description

For any nonempty set $s$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, the affine span of $s$ is nonempty.

affineSpan_eq_bot theorem

: affineSpan k s = ⊥ ↔ s = ∅

Full source

/-- The affine span of a set is `⊥` if and only if that set is empty. -/
@[simp]
theorem affineSpan_eq_bot : affineSpanaffineSpan k s = ⊥ ↔ s = ∅ := by
  rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    nonempty_iff_ne_empty]

Empty Set Characterization for Affine Span: $\operatorname{affineSpan}_k(s) = \bot \leftrightarrow s = \emptyset$

Informal description

The affine span of a set $s$ in an affine space $P$ over a module $V$ with scalar ring $k$ is equal to the bottom element $\bot$ (the empty affine subspace) if and only if $s$ is the empty set. In symbols: $\operatorname{affineSpan}_k(s) = \bot \leftrightarrow s = \emptyset$.

bot_lt_affineSpan theorem

: ⊥ < affineSpan k s ↔ s.Nonempty

Full source

@[simp]
theorem bot_lt_affineSpan : ⊥⊥ < affineSpan k s ↔ s.Nonempty := by
  rw [bot_lt_iff_ne_bot, nonempty_iff_ne_empty]
  exact (affineSpan_eq_bot _).not

Nonempty Set Characterization via Affine Span: $\bot < \operatorname{affineSpan}_k(s) \leftrightarrow s \neq \emptyset$

Informal description

For any set $s$ of points in an affine space over a module with scalar ring $k$, the empty affine subspace $\bot$ is strictly contained in the affine span of $s$ if and only if $s$ is nonempty. In symbols: $\bot < \operatorname{affineSpan}_k(s) \leftrightarrow s \neq \emptyset$.

affineSpan_induction theorem

 {x : P} {s : Set P} {p : P → Prop} (h : x ∈ affineSpan k s) (mem : ∀ x : P, x ∈ s → p x)
  (smul_vsub_vadd : ∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)) : p x

Full source

/-- 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`. -/
@[elab_as_elim]
theorem affineSpan_induction {x : P} {s : Set P} {p : P → Prop} (h : x ∈ affineSpan k s)
    (mem : ∀ x : P, x ∈ s → p x)
    (smul_vsub_vadd : ∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)) : p x :=
  (affineSpan_le (Q := ⟨p, smul_vsub_vadd⟩)).mpr mem h

Induction Principle for Affine Span Membership

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a subset of $P$. For any point $x$ in the affine span of $s$, if a predicate $p$ holds for all points in $s$ and is preserved under affine combinations of the form $c \cdot (u - v) + w$ for any $c \in k$ and $u, v, w \in P$, then $p$ holds for $x$. More precisely, given: 1. $x \in \text{affineSpan}_k(s)$, 2. $\forall y \in s, p(y)$, 3. $\forall c \in k, \forall u, v, w \in P, p(u) \land p(v) \land p(w) \implies p(c \cdot (u - v) + w)$, then $p(x)$ holds.

affineSpan_induction' theorem

 {s : Set P} {p : ∀ x, x ∈ affineSpan k s → Prop} (mem : ∀ (y) (hys : y ∈ s), p y (subset_affineSpan k _ hys))
  (smul_vsub_vadd :
    ∀ (c : k) (u hu v hv w hw),
      p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) (AffineSubspace.smul_vsub_vadd_mem _ _ hu hv hw))
  {x : P} (h : x ∈ affineSpan k s) : p x h

Full source

/-- A dependent version of `affineSpan_induction`. -/
@[elab_as_elim]
theorem affineSpan_induction' {s : Set P} {p : ∀ x, x ∈ affineSpan k s → Prop}
    (mem : ∀ (y) (hys : y ∈ s), p y (subset_affineSpan k _ hys))
    (smul_vsub_vadd : ∀ (c : k) (u hu v hv w hw), p u hu → p v hv → p w hw →
      p (c • (u -ᵥ v) +ᵥ w) (AffineSubspace.smul_vsub_vadd_mem _ _ hu hv hw))
    {x : P} (h : x ∈ affineSpan k s) : p x h := by
  suffices ∃ (hx : x ∈ affineSpan k s), p x hx from this.elim fun hx hc ↦ hc
  -- TODO: `induction h using affineSpan_induction` gives the error:
  -- extra targets for '@affineSpan_induction'
  -- It seems that the `induction` tactic has decided to ignore the clause
  -- `using affineSpan_induction` and use `Exists.rec` instead.
  refine affineSpan_induction h ?mem ?smul_vsub_vadd
  · exact fun y hy ↦ ⟨subset_affineSpan _ _ hy, mem y hy⟩
  · exact fun c u v w hu hv hw ↦
      hu.elim fun hu' hu ↦ hv.elim fun hv' hv ↦ hw.elim fun hw' hw ↦
        ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw',
              smul_vsub_vadd _ _ _ _ _ _ _ hu hv hw⟩

Dependent Induction Principle for Affine Span Membership

Informal description

Let $P$ be an affine space over a module $V$ with scalar ring $k$, and let $s$ be a subset of $P$. Given a predicate $p$ on points in the affine span of $s$ such that: 1. For every point $y \in s$, $p(y)$ holds (with the proof that $y$ is in the affine span), 2. For any $c \in k$ and points $u, v, w$ in the affine span of $s$ (with proofs $hu, hv, hw$), if $p(u, hu)$, $p(v, hv)$, and $p(w, hw)$ hold, then $p(c \cdot (u - v) + w)$ holds (with the proof that this point is in the affine span), then for any point $x$ in the affine span of $s$, $p(x, h)$ holds (where $h$ is the proof that $x$ is in the affine span).

vsub_mem_vectorSpan_pair theorem

(p₁ p₂ : P) : p₁ -ᵥ p₂ ∈ vectorSpan k ({ p₁, p₂ } : Set P)

Full source

/-- The difference between two points lies in their `vectorSpan`. -/
theorem vsub_mem_vectorSpan_pair (p₁ p₂ : P) : p₁ -ᵥ p₂p₁ -ᵥ p₂ ∈ vectorSpan k ({p₁, p₂} : Set P) :=
  vsub_mem_vectorSpan _ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Difference Vector of Two Points Belongs to Their Vector Span

Informal description

For any two points $p_1$ and $p_2$ in an affine space over a module $V$, the difference vector $p_1 - p_2$ lies in the vector span of the set $\{p_1, p_2\}$.

vsub_rev_mem_vectorSpan_pair theorem

(p₁ p₂ : P) : p₂ -ᵥ p₁ ∈ vectorSpan k ({ p₁, p₂ } : Set P)

Full source

/-- The difference between two points (reversed) lies in their `vectorSpan`. -/
theorem vsub_rev_mem_vectorSpan_pair (p₁ p₂ : P) : p₂ -ᵥ p₁p₂ -ᵥ p₁ ∈ vectorSpan k ({p₁, p₂} : Set P) :=
  vsub_mem_vectorSpan _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)) (Set.mem_insert _ _)

Reversed Difference Vector in Vector Span of Two Points

Informal description

For any two points $p_1$ and $p_2$ in an affine space over a module $V$, the reversed difference vector $p_2 - p_1$ lies in the vector span of the set $\{p_1, p_2\}$.

smul_vsub_mem_vectorSpan_pair theorem

(r : k) (p₁ p₂ : P) : r • (p₁ -ᵥ p₂) ∈ vectorSpan k ({ p₁, p₂ } : Set P)

Full source

/-- A multiple of the difference between two points lies in their `vectorSpan`. -/
theorem smul_vsub_mem_vectorSpan_pair (r : k) (p₁ p₂ : P) :
    r • (p₁ -ᵥ p₂) ∈ vectorSpan k ({p₁, p₂} : Set P) :=
  Submodule.smul_mem _ _ (vsub_mem_vectorSpan_pair k p₁ p₂)

Scaled Difference Vector in Vector Span of Two Points

Informal description

For any scalar $r$ in a ring $k$ and any two points $p_1$ and $p_2$ in an affine space over a module $V$, the scaled difference vector $r \cdot (p_1 - p_2)$ lies in the vector span of the set $\{p_1, p_2\}$.

smul_vsub_rev_mem_vectorSpan_pair theorem

(r : k) (p₁ p₂ : P) : r • (p₂ -ᵥ p₁) ∈ vectorSpan k ({ p₁, p₂ } : Set P)

Full source

/-- A multiple of the difference between two points (reversed) lies in their `vectorSpan`. -/
theorem smul_vsub_rev_mem_vectorSpan_pair (r : k) (p₁ p₂ : P) :
    r • (p₂ -ᵥ p₁) ∈ vectorSpan k ({p₁, p₂} : Set P) :=
  Submodule.smul_mem _ _ (vsub_rev_mem_vectorSpan_pair k p₁ p₂)

Scaled Reversed Difference Vector in Vector Span of Two Points

Informal description

For any scalar $r$ in a ring $k$ and any two points $p_1$ and $p_2$ in an affine space over a module $V$, the scaled reversed difference vector $r \cdot (p_2 - p_1)$ lies in the vector span of the set $\{p_1, p_2\}$.

termLine[_,_,_] definition

: Lean.ParserDescr✝

Full source

/-- The line between two points, as an affine subspace. -/
notation "line[" k ", " p₁ ", " p₂ "]" =>
  affineSpan k (insert p₁ (@singleton _ _ Set.instSingletonSet p₂))

Affine line through two points

Informal description

For a ring $k$ and points $p₁, p₂$ in an affine space over $k$, the notation $\text{line}[k, p₁, p₂]$ represents the affine subspace generated by the set $\{p₁, p₂\}$, which is the line passing through these two points.

left_mem_affineSpan_pair theorem

(p₁ p₂ : P) : p₁ ∈ line[k, p₁, p₂]

Full source

/-- The first of two points lies in their affine span. -/
theorem left_mem_affineSpan_pair (p₁ p₂ : P) : p₁ ∈ line[k, p₁, p₂] :=
  mem_affineSpan _ (Set.mem_insert _ _)

First Point in Affine Span of Pair

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, the first point $p_1$ lies in the affine span of the pair $\{p_1, p_2\}$, denoted $\text{affineSpan}_k \{p_1, p_2\}$.

right_mem_affineSpan_pair theorem

(p₁ p₂ : P) : p₂ ∈ line[k, p₁, p₂]

Full source

/-- The second of two points lies in their affine span. -/
theorem right_mem_affineSpan_pair (p₁ p₂ : P) : p₂ ∈ line[k, p₁, p₂] :=
  mem_affineSpan _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Second Point in Affine Span of Pair

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, the second point $p_2$ lies in the affine span of the pair $\{p_1, p_2\}$, i.e., $p_2 \in \text{affineSpan}_k \{p_1, p_2\}$.

affineSpan_pair_le_of_mem_of_mem theorem

{p₁ p₂ : P} {s : AffineSubspace k P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : line[k, p₁, p₂] ≤ s

Full source

/-- The span of two points that lie in an affine subspace is contained in that subspace. -/
theorem affineSpan_pair_le_of_mem_of_mem {p₁ p₂ : P} {s : AffineSubspace k P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) : line[k, p₁, p₂] ≤ s := by
  rw [affineSpan_le, Set.insert_subset_iff, Set.singleton_subset_iff]
  exact ⟨hp₁, hp₂⟩

Affine Span of Pair Contained in Affine Subspace: $\text{affineSpan}_k\{p_1, p_2\} \leq s$ if $p_1, p_2 \in s$

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a module $V$ with scalar ring $k$, if both $p_1$ and $p_2$ belong to an affine subspace $s$ of $P$, then the affine span of the pair $\{p_1, p_2\}$ is contained in $s$.

affineSpan_pair_le_of_left_mem theorem

{p₁ p₂ p₃ : P} (h : p₁ ∈ line[k, p₂, p₃]) : line[k, p₁, p₃] ≤ line[k, p₂, p₃]

Full source

/-- 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. -/
theorem affineSpan_pair_le_of_left_mem {p₁ p₂ p₃ : P} (h : p₁ ∈ line[k, p₂, p₃]) :
    line[k, p₁, p₃] ≤ line[k, p₂, p₃] :=
  affineSpan_pair_le_of_mem_of_mem h (right_mem_affineSpan_pair _ _ _)

Inclusion of Affine Spans: $\text{affineSpan}_k\{p_1, p_3\} \subseteq \text{affineSpan}_k\{p_2, p_3\}$ when $p_1 \in \text{affineSpan}_k\{p_2, p_3\}$

Informal description

For any three points $p_1, p_2, p_3$ in an affine space $P$ over a module $V$ with scalar ring $k$, if $p_1$ lies in the affine span of $\{p_2, p_3\}$, then the affine span of $\{p_1, p_3\}$ is contained in the affine span of $\{p_2, p_3\}$.

affineSpan_pair_le_of_right_mem theorem

{p₁ p₂ p₃ : P} (h : p₁ ∈ line[k, p₂, p₃]) : line[k, p₂, p₁] ≤ line[k, p₂, p₃]

Full source

/-- 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. -/
theorem affineSpan_pair_le_of_right_mem {p₁ p₂ p₃ : P} (h : p₁ ∈ line[k, p₂, p₃]) :
    line[k, p₂, p₁] ≤ line[k, p₂, p₃] :=
  affineSpan_pair_le_of_mem_of_mem (left_mem_affineSpan_pair _ _ _) h

Inclusion of Affine Spans: $\text{affineSpan}_k\{p_2, p_1\} \subseteq \text{affineSpan}_k\{p_2, p_3\}$ when $p_1 \in \text{affineSpan}_k\{p_2, p_3\}$

Informal description

For any three points $p_1, p_2, p_3$ in an affine space $P$ over a module $V$ with scalar ring $k$, if $p_1$ lies in the affine span of $\{p_2, p_3\}$, then the affine span of $\{p_2, p_1\}$ is contained in the affine span of $\{p_2, p_3\}$.

affineSpan_mono theorem

{s₁ s₂ : Set P} (h : s₁ ⊆ s₂) : affineSpan k s₁ ≤ affineSpan k s₂

Full source

/-- `affineSpan` is monotone. -/
@[gcongr, mono]
theorem affineSpan_mono {s₁ s₂ : Set P} (h : s₁ ⊆ s₂) : affineSpan k s₁ ≤ affineSpan k s₂ :=
  affineSpan_le_of_subset_coe (Set.Subset.trans h (subset_affineSpan k _))

Monotonicity of Affine Span: $s_1 \subseteq s_2 \Rightarrow \text{affineSpan}_k s_1 \leq \text{affineSpan}_k s_2$

Informal description

For any two sets $s_1$ and $s_2$ of points in an affine space $P$ over a module $V$ with scalar ring $k$, if $s_1 \subseteq s_2$, then the affine span of $s_1$ is contained in the affine span of $s_2$, i.e., $\text{affineSpan}_k s_1 \leq \text{affineSpan}_k s_2$.

affineSpan_insert_affineSpan theorem

(p : P) (ps : Set P) : affineSpan k (insert p (affineSpan k ps : Set P)) = affineSpan k (insert p ps)

Full source

/-- 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. -/
theorem affineSpan_insert_affineSpan (p : P) (ps : Set P) :
    affineSpan k (insert p (affineSpan k ps : Set P)) = affineSpan k (insert p ps) := by
  rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]

Affine Span Insertion Invariance: $\text{affineSpan}_k(\{p\} \cup \text{affineSpan}_k(ps)) = \text{affineSpan}_k(\{p\} \cup ps)$

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, and any set of points $ps \subseteq P$, the affine span of the set obtained by inserting $p$ into the affine span of $ps$ is equal to the affine span of the set obtained by inserting $p$ directly into $ps$. In other words: \[ \text{affineSpan}_k(\{p\} \cup \text{affineSpan}_k(ps)) = \text{affineSpan}_k(\{p\} \cup ps) \]

affineSpan_insert_eq_affineSpan theorem

{p : P} {ps : Set P} (h : p ∈ affineSpan k ps) : affineSpan k (insert p ps) = affineSpan k ps

Full source

/-- If a point is in the affine span of a set, adding it to that set does not change the affine
span. -/
theorem affineSpan_insert_eq_affineSpan {p : P} {ps : Set P} (h : p ∈ affineSpan k ps) :
    affineSpan k (insert p ps) = affineSpan k ps := by
  rw [← mem_coe] at h
  rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]

Affine Span Unchanged by Inserting Dependent Point

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, and any set of points $ps \subseteq P$, if $p$ belongs to the affine span of $ps$, then the affine span of the set obtained by inserting $p$ into $ps$ is equal to the affine span of $ps$. In other words: \[ p \in \text{affineSpan}_k(ps) \implies \text{affineSpan}_k(\{p\} \cup ps) = \text{affineSpan}_k(ps) \]

vectorSpan_insert_eq_vectorSpan theorem

{p : P} {ps : Set P} (h : p ∈ affineSpan k ps) : vectorSpan k (insert p ps) = vectorSpan k ps

Full source

/-- If a point is in the affine span of a set, adding it to that set does not change the vector
span. -/
theorem vectorSpan_insert_eq_vectorSpan {p : P} {ps : Set P} (h : p ∈ affineSpan k ps) :
    vectorSpan k (insert p ps) = vectorSpan k ps := by
  simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]

Vector Span Unchanged by Inserting Affinely Dependent Point

Informal description

For any point $p$ in an affine space $P$ over a module $V$ with scalar ring $k$, and any set of points $ps \subseteq P$, if $p$ belongs to the affine span of $ps$, then the vector span of the set obtained by inserting $p$ into $ps$ is equal to the vector span of $ps$. In other words: \[ p \in \text{affineSpan}_k(ps) \implies \text{vectorSpan}_k(\{p\} \cup ps) = \text{vectorSpan}_k(ps) \]

affineSpan_le_toAffineSubspace_span theorem

{s : Set V} : affineSpan k s ≤ (Submodule.span k s).toAffineSubspace

Full source

/-- When the affine space is also a vector space, the affine span is contained within the linear
span. -/
lemma affineSpan_le_toAffineSubspace_span {s : Set V} :
    affineSpan k s ≤ (Submodule.span k s).toAffineSubspace := by
  intro x hx
  simp only [SetLike.mem_coe, Submodule.mem_toAffineSubspace]
  induction hx using affineSpan_induction' with
  | mem x hx => exact Submodule.subset_span hx
  | smul_vsub_vadd c u _ v _ w _ hu hv hw =>
    simp only [vsub_eq_sub, vadd_eq_add]
    apply Submodule.add_mem _ _ hw
    exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)

Affine Span is Contained in Linear Span's Affine Subspace

Informal description

For any subset $s$ of a vector space $V$ over a ring $k$, the affine span of $s$ is contained in the affine subspace obtained by interpreting the linear span of $s$ as an affine subspace. In other words, $\operatorname{affineSpan}_k s \leq (\operatorname{span}_k s).\text{toAffineSubspace}$.

affineSpan_subset_span theorem

{s : Set V} : (affineSpan k s : Set V) ⊆ Submodule.span k s

Full source

lemma affineSpan_subset_span {s : Set V} :
    (affineSpan k s : Set V) ⊆  Submodule.span k s :=
  affineSpan_le_toAffineSubspace_span

Affine Span is Subset of Linear Span

Informal description

For any subset $s$ of a vector space $V$ over a ring $k$, the affine span of $s$ (considered as a subset of $V$) is contained in the linear span of $s$. In other words, $\operatorname{affineSpan}_k s \subseteq \operatorname{span}_k s$.

affineSpan_insert_zero theorem

(s : Set V) : (affineSpan k (insert 0 s) : Set V) = Submodule.span k s

Full source

lemma affineSpan_insert_zero (s : Set V) :
    (affineSpan k (insert 0 s) : Set V) = Submodule.span k s := by
  rw [← Submodule.span_insert_zero]
  refine affineSpan_subset_span.antisymm ?_
  rw [← vectorSpan_add_self, vectorSpan_def]
  refine Subset.trans ?_ <| subset_add_left _ <| mem_insert ..
  gcongr
  exact subset_sub_left <| mem_insert ..

Affine Span of Zero-Inserted Set Equals Linear Span: $\operatorname{affineSpan}_k (\{0\} \cup s) = \operatorname{span}_k s$

Informal description

For any subset $s$ of a vector space $V$ over a ring $k$, the affine span of the set obtained by inserting the zero vector into $s$ is equal to the linear span of $s$ as subsets of $V$. That is, $$\operatorname{affineSpan}_k (\{0\} \cup s) = \operatorname{span}_k s.$$

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Main definitions

Implementation notes

References