linear_algebra.affine_space.finite_dimensional

source

theorem finite_dimensional_vector_span_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : s.finite) :

finite_dimensional k ↥(vector_span k s)

The vector_span of a finite set is finite-dimensional.

source

@[protected, instance]

def finite_dimensional_vector_span_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) :

finite_dimensional k ↥(vector_span k (set.range p))

The vector_span of a family indexed by a fintype is finite-dimensional.

source

@[protected, instance]

def finite_dimensional_vector_span_image_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) (s : set ι) :

finite_dimensional k ↥(vector_span k (p '' s))

The vector_span of a subset of a family indexed by a fintype is finite-dimensional.

source

theorem finite_dimensional_direction_affine_span_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : s.finite) :

finite_dimensional k ↥((affine_span k s).direction)

The direction of the affine span of a finite set is finite-dimensional.

source

@[protected, instance]

def finite_dimensional_direction_affine_span_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) :

finite_dimensional k ↥((affine_span k (set.range p)).direction)

The direction of the affine span of a family indexed by a fintype is finite-dimensional.

source

@[protected, instance]

def finite_dimensional_direction_affine_span_image_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) (s : set ι) :

finite_dimensional k ↥((affine_span k (p '' s)).direction)

The direction of the affine span of a subset of a family indexed by a fintype is finite-dimensional.

source

noncomputable def fintype_of_fin_dim_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] {p : ι → P} (hi : affine_independent k p) :

fintype ι

An affine-independent family of points in a finite-dimensional affine space is finite.

Equations

fintype_of_fin_dim_affine_independent k hi = dite (is_empty ι) (λ (hι : is_empty ι), fintype.of_is_empty) (λ (hι : ¬is_empty ι), let q : ι := _.some, _inst : is_noetherian k V := _ in fintype_of_fintype_ne q (fintype.of_finite {x // x ≠ q}))

source

theorem finite_of_fin_dim_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] {s : set P} (hi : affine_independent k coe) :

s.finite

An affine-independent subset of a finite-dimensional affine space is finite.

source

theorem affine_independent.finrank_vector_span_image_finset {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : ι → P} (hi : affine_independent k p) {s : finset ι} {n : ℕ} (hc : s.card = n + 1) :

finite_dimensional.finrank k ↥(vector_span k ↑(finset.image p s)) = n

The vector_span of a finite subset of an affinely independent family has dimension one less than its cardinality.

source

theorem affine_independent.finrank_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] {p : ι → P} (hi : affine_independent k p) {n : ℕ} (hc : fintype.card ι = n + 1) :

finite_dimensional.finrank k ↥(vector_span k (set.range p)) = n

The vector_span of a finite affinely independent family has dimension one less than its cardinality.

source

theorem affine_independent.vector_span_eq_top_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] [fintype ι] {p : ι → P} (hi : affine_independent k p) (hc : fintype.card ι = finite_dimensional.finrank k V + 1) :

vector_span k (set.range p) = ⊤

The vector_span of a finite affinely independent family whose cardinality is one more than that of the finite-dimensional space is ⊤.

source

theorem finrank_vector_span_image_finset_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : ι → P) (s : finset ι) {n : ℕ} (hc : s.card = n + 1) :

finite_dimensional.finrank k ↥(vector_span k ↑(finset.image p s)) ≤ n

The vector_span of n + 1 points in an indexed family has dimension at most n.

source

theorem finrank_vector_span_range_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 1) :

finite_dimensional.finrank k ↥(vector_span k (set.range p)) ≤ n

The vector_span of an indexed family of n + 1 points has dimension at most n.

source

theorem affine_independent_iff_finrank_vector_span_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 1) :

affine_independent k p ↔ finite_dimensional.finrank k ↥(vector_span k (set.range p)) = n

n + 1 points are affinely independent if and only if their vector_span has dimension n.

source

theorem affine_independent_iff_le_finrank_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 1) :

affine_independent k p ↔ n ≤ finite_dimensional.finrank k ↥(vector_span k (set.range p))

n + 1 points are affinely independent if and only if their vector_span has dimension at least n.

source

theorem affine_independent_iff_not_finrank_vector_span_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 2) :

affine_independent k p ↔ ¬finite_dimensional.finrank k ↥(vector_span k (set.range p)) ≤ n

n + 2 points are affinely independent if and only if their vector_span does not have dimension at most n.

source

theorem finrank_vector_span_le_iff_not_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 2) :

finite_dimensional.finrank k ↥(vector_span k (set.range p)) ≤ n ↔ ¬affine_independent k p

n + 2 points have a vector_span with dimension at most n if and only if they are not affinely independent.

source

theorem affine_independent.vector_span_image_finset_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sm : submodule k V} [finite_dimensional k ↥sm] (hle : vector_span k ↑(finset.image p s) ≤ sm) (hc : s.card = finite_dimensional.finrank k ↥sm + 1) :

vector_span k ↑(finset.image p s) = sm

If the vector_span of a finite subset of an affinely independent family lies in a submodule with dimension one less than its cardinality, it equals that submodule.

source

theorem affine_independent.vector_span_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] {p : ι → P} (hi : affine_independent k p) {sm : submodule k V} [finite_dimensional k ↥sm] (hle : vector_span k (set.range p) ≤ sm) (hc : fintype.card ι = finite_dimensional.finrank k ↥sm + 1) :

vector_span k (set.range p) = sm

If the vector_span of a finite affinely independent family lies in a submodule with dimension one less than its cardinality, it equals that submodule.

source

theorem affine_independent.affine_span_image_finset_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sp : affine_subspace k P} [finite_dimensional k ↥(sp.direction)] (hle : affine_span k ↑(finset.image p s) ≤ sp) (hc : s.card = finite_dimensional.finrank k ↥(sp.direction) + 1) :

affine_span k ↑(finset.image p s) = sp

If the affine_span of a finite subset of an affinely independent family lies in an affine subspace whose direction has dimension one less than its cardinality, it equals that subspace.

source

theorem affine_independent.affine_span_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] {p : ι → P} (hi : affine_independent k p) {sp : affine_subspace k P} [finite_dimensional k ↥(sp.direction)] (hle : affine_span k (set.range p) ≤ sp) (hc : fintype.card ι = finite_dimensional.finrank k ↥(sp.direction) + 1) :

affine_span k (set.range p) = sp

If the affine_span of a finite affinely independent family lies in an affine subspace whose direction has dimension one less than its cardinality, it equals that subspace.

source

theorem affine_independent.affine_span_eq_top_iff_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] [fintype ι] {p : ι → P} (hi : affine_independent k p) :

affine_span k (set.range p) = ⊤ ↔ fintype.card ι = finite_dimensional.finrank k V + 1

The affine_span of a finite affinely independent family is ⊤ iff the family's cardinality is one more than that of the finite-dimensional space.

source

theorem finite_dimensional_vector_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [finite_dimensional k ↥(s.direction)] (p : P) :

finite_dimensional k ↥(vector_span k (has_insert.insert p ↑s))

The vector_span of adding a point to a finite-dimensional subspace is finite-dimensional.

source

theorem finite_dimensional_direction_affine_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [finite_dimensional k ↥(s.direction)] (p : P) :

finite_dimensional k ↥((affine_span k (has_insert.insert p ↑s)).direction)

The direction of the affine span of adding a point to a finite-dimensional subspace is finite-dimensional.

source

theorem finite_dimensional_vector_span_insert_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) [finite_dimensional k ↥(vector_span k s)] (p : P) :

finite_dimensional k ↥(vector_span k (has_insert.insert p s))

The vector_span of adding a point to a set with a finite-dimensional vector_span is finite-dimensional.

source

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

Prop

A set of points is collinear if their vector_span has dimension at most 1.

Equations

collinear k s = (module.rank k ↥(vector_span k s) ≤ 1)

source

theorem collinear_iff_dim_le_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :

collinear k s ↔ module.rank k ↥(vector_span k s) ≤ 1

The definition of collinear.

source

theorem collinear_iff_finrank_le_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) [finite_dimensional k ↥(vector_span k s)] :

collinear k s ↔ finite_dimensional.finrank k ↥(vector_span k s) ≤ 1

A set of points, whose vector_span is finite-dimensional, is collinear if and only if their vector_span has dimension at most 1.

source

theorem collinear_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] :

collinear k ∅

The empty set is collinear.

source

theorem collinear_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) :

collinear k {p}

A single point is collinear.

source

theorem collinear_iff_of_mem (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p₀ : P} (h : p₀ ∈ s) :

collinear k s ↔ ∃ (v : V), ∀ (p : P), p ∈ s → (∃ (r : k), p = r • v +ᵥ p₀)

Given a point p₀ in a set of points, that set is collinear if and only if the points can all be expressed as multiples of the same vector, added to p₀.

source

theorem collinear_iff_exists_forall_eq_smul_vadd (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :

collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ (p : P), p ∈ s → (∃ (r : k), p = r • v +ᵥ p₀)

A set of points is collinear if and only if they can all be expressed as multiples of the same vector, added to the same base point.

source

theorem collinear_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :

collinear k {p₁, p₂}

Two points are collinear.

source

theorem affine_independent_iff_not_collinear (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : fin 3 → P) :

affine_independent k p ↔ ¬collinear k (set.range p)

Three points are affinely independent if and only if they are not collinear.

source

theorem collinear_iff_not_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : fin 3 → P) :

collinear k (set.range p) ↔ ¬affine_independent k p

Three points are collinear if and only if they are not affinely independent.

source

theorem finrank_vector_span_insert_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) (p : P) :

finite_dimensional.finrank k ↥(vector_span k (has_insert.insert p ↑s)) ≤ finite_dimensional.finrank k ↥(s.direction) + 1

Adding a point to a finite-dimensional subspace increases the dimension by at most one.

source

theorem finrank_vector_span_insert_le_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) (p : P) :

finite_dimensional.finrank k ↥(vector_span k (has_insert.insert p s)) ≤ finite_dimensional.finrank k ↥(vector_span k s) + 1

Adding a point to a set with a finite-dimensional span increases the dimension by at most one.

mathlib documentation

Finite-dimensional subspaces of affine spaces. #

Main definitions #