theorem translate_eq_exists_add_of_isCompl (n : ℕ) (L W : Submodule ℝ (Fin n → ℝ)) (hLW : IsCompl L W) (x0 : Fin n → ℝ) : SetTranslate n (↑L) x0 = {x : Fin n → ℝ | ∃ (y : Fin n → ℝ), x = x0 + (Submodule.IsCompl.projection hLW) y}

A translate of a submodule can be written using a projection onto the submodule.

theorem graph_of_affineMap_exists_fin (n : ℕ) (C : Set (Fin n → ℝ)) (L W : Submodule ℝ (Fin n → ℝ)) (Φ : (Fin n → ℝ) ≃ₗ[ℝ] ↥L × ↥W) (f : ↥L →ᵃ[ℝ] ↥W) (hgraph : ⇑Φ '' C = {p : ↥L × ↥W | p.2 = f p.1}) : ∃ (n1 : ℕ) (n2 : ℕ) (f' : (Fin n1 → ℝ) →ᵃ[ℝ] Fin n2 → ℝ) (e : (Fin n1 → ℝ) × (Fin n2 → ℝ) →ₗ[ℝ] Fin n → ℝ), C = {x : Fin n → ℝ | ∃ (y1 : Fin n1 → ℝ), x = e (y1, f' y1)}

Convert a graph description in submodule coordinates to one in Fin coordinates.

theorem affineSet_eq_image_submodule_translate_and_graph (n : ℕ) (C : Set (Fin n → ℝ)) : IsAffineSet n C → C.Nonempty → C ≠ Set.univ → (∃ (m : ℕ) (k : ℕ) (L : Submodule ℝ (Fin m → ℝ)) (T : (Fin m → ℝ) →ᴬ[ℝ] Fin k → ℝ) (y0 : Fin m → ℝ) (e : (Fin k → ℝ) ≃ₗ[ℝ] Fin n → ℝ), C = {x : Fin n → ℝ | ∃ y ∈ (fun (l : Fin m → ℝ) => l + y0) '' ↑L, x = e (T y)}) ∧ ∃ (m : ℕ) (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) (x0 : Fin n → ℝ), C = {x : Fin n → ℝ | ∃ (y : Fin m → ℝ), x = x0 + A y} ∧ ∃ (n1 : ℕ) (n2 : ℕ) (f : (Fin n1 → ℝ) →ᵃ[ℝ] Fin n2 → ℝ) (e : (Fin n1 → ℝ) × (Fin n2 → ℝ) →ₗ[ℝ] Fin n → ℝ), C = {x : Fin n → ℝ | ∃ (y1 : Fin n1 → ℝ), x = e (y1, f y1)}

Text 1.13.1: Affine sets are affine images and graphs of affine maps (existence forms).