Preliminary lemmas and definitions used by the Polytopes formalization.

theorem Set.Subtype {α : Type u_1} {property : α → Prop} (S : Set α) (hS : ∀ s ∈ S, property s) : ∃ (S' : Set { x : α // property x }), Subtype.val '' S' = S ∧ Subtype.val ⁻¹' S = S'

Lifts a set whose elements satisfy property to the corresponding subtype.

theorem Set.Finite.translation {α : Type} [AddGroup α] {S : Set α} (hS : S.Finite) (x : α) : (S + {x}).Finite

theorem Set.mem_translation {α : Type} [AddGroup α] {S : Set α} (x s : α) : s ∈ S + {x} ↔ s - x ∈ S

theorem Set.vsub_eq_sub {G : Type} [AddGroup G] (g1 g2 : Set G) : g1 -ᵥ g2 = g1 - g2

theorem Set.sub_eq_neg_add {α : Type} [AddGroup α] (S : Set α) (x : α) : S - {x} = S + {-x}

theorem Set.neg_add_cancel_right' {α : Type} [AddGroup α] {S : Set α} (x : α) : S - {x} + {x} = S

theorem Set.Nonempty.sInter_inter_comm {α : Type u_1} {s : Set (Set α)} (hs : s.Nonempty) {t : Set α} : ⋂₀ ((fun (x : Set α) => x ∩ t) '' s) = ⋂₀ s ∩ t

theorem Set.Nonempty.image_sInter {α : Type u_1} {β : Type u_2} {S : Set (Set α)} (hS : S.Nonempty) {f : α → β} (hf : Function.Injective f) : f '' ⋂₀ S = ⋂ s ∈ S, f '' s

def Equiv.VSubconst {E P : Type} [AddCommGroup E] [AddTorsor E P] (x : P) : P ≃ E

The equivalence P ≃ E sending a point p to the vector p -ᵥ x.

Equations

• Equiv.VSubconst x = { toFun := fun (x_1 : P) => x_1 -ᵥ x, invFun := fun (x_1 : E) => x_1 +ᵥ x, left_inv := ⋯, right_inv := ⋯ }

theorem Equiv.coe_VSubconst {E P : Type} [AddCommGroup E] [AddTorsor E P] (x : P) : ⇑(VSubconst x) = fun (x_1 : P) => x_1 -ᵥ x

def AffineEquiv.VSubconst (𝕜 : Type) {E P : Type} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddTorsor E P] (x : P) : P ≃ᵃ[𝕜] E

The affine equivalence P ≃ᵃ[𝕜] E sending a point p to the vector p -ᵥ x.

Equations

• AffineEquiv.VSubconst 𝕜 x = { toEquiv := Equiv.VSubconst x, linear := LinearEquiv.refl 𝕜 E, map_vadd' := ⋯ }

theorem AffineEquiv.Vsubconst_toEquiv (𝕜 : Type) {E P : Type} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddTorsor E P] (x : P) : (VSubconst 𝕜 x).toEquiv = Equiv.VSubconst x

theorem AffineEquiv.Vsubconst_linear_apply (𝕜 : Type) {E P : Type} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddTorsor E P] (x : P) (v : E) : (VSubconst 𝕜 x).linear v = v

theorem AffineEquiv.coe_VSubconst (𝕜 : Type) {E P : Type} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddTorsor E P] (x : P) : ⇑(VSubconst 𝕜 x) = fun (x_1 : P) => x_1 -ᵥ x

def AffineIsometryEquiv.VSubconst (𝕜 : Type) {E P : Type} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [PseudoMetricSpace P] [NormedAddTorsor E P] (x : P) : P ≃ᵃⁱ[𝕜] E

The affine isometry equivalence P ≃ᵃⁱ[𝕜] E sending a point p to the vector p -ᵥ x.

Equations

• AffineIsometryEquiv.VSubconst 𝕜 x = { toAffineEquiv := AffineEquiv.VSubconst 𝕜 x, norm_map := ⋯ }

@[simp]

theorem AffineIsometryEquiv.coe_VSubconst (𝕜 : Type) {E P : Type} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [PseudoMetricSpace P] [NormedAddTorsor E P] (x : P) : ⇑(VSubconst 𝕜 x) = fun (x_1 : P) => x_1 -ᵥ x

theorem Submodule.mem_orthogonal_Basis {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) (b : Module.Basis ι 𝕜 ↥K) (v : E) : v ∈ Kᗮ ↔ ∀ (i : ι), inner 𝕜 (↑(b i)) v = 0

theorem AffineMap.preimage_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} {f : E →ᵃ[𝕜] F} (hf : Function.Injective f.toFun) (hs : s ⊆ Set.range ⇑f) : ⇑f ⁻¹' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f ⁻¹' s)

theorem affineSpan_nontrivial (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Nontrivial ↑s) : Nontrivial ↥(affineSpan k s)

The affine span of a nontrivial set is nontrivial.

theorem AffineSubspace.direction_nontrivial_of_nontrivial (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (Q : AffineSubspace k P) : Nontrivial ↥Q → Nontrivial ↥Q.direction

A nontrivial affine subspace has nontrivial direction.

theorem AffineSubspace.direction_subset_subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {Q : AffineSubspace k P} {S T : Set P} (hS : S ⊆ ↑Q) (hT : T ⊆ ↑Q) : S -ᵥ T ⊆ ↑Q.direction

If two sets are contained in an affine subspace, their difference lies in its direction.

def Matrix.rowOpPivot {R : Type u_1} [Field R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) (i : Fin m) (x : Fin n) (h : A i x ≠ 0) : Matrix (Fin m) (Fin n) R

The row operation that normalizes a pivot row and clears the pivot column.

Equations

• A.rowOpPivot i x h = fun (j : Fin m) => if j = i then (A i x)⁻¹ • A i else -A j x • (A i x)⁻¹ • A i + A j

def Nat.finListRange (n : ℕ) : List (Fin n)

The list of all elements of Fin n, in increasing order.

Equations

• Nat.finListRange 0 = []
• m.succ.finListRange = 0 :: List.map Fin.succ m.finListRange

theorem Fin.mem_fin_list_range {n : ℕ} (i : Fin n) : i ∈ n.finListRange

def Vector.Listdrop {R : Type u_1} {n : ℕ} (m : ℕ) : Vector R n → Vector R (n - m)

Drops the first m entries from a length-indexed vector.

Equations

• Vector.Listdrop m v = v.drop m