Affine coordinates with a prescribed first coordinate

A continuous linear equivalence e : V ≃L[ℝ] ℝ × F' identifies a real normed affine space P over V, once an origin z is chosen, with ℝ × F'. Its first coordinate can be replaced by any continuous functional ℓ not vanishing on e.symm (1, 0): keeping the second coordinate of e, the map y ↦ (ℓ (y -ᵥ z), (e (y -ᵥ z)).2) is still a homeomorphism P ≃ₜ ℝ × F'.

Main results

• TauCeti.exists_homeomorph_fst_eq: a homeomorphism P ≃ₜ ℝ × F' with first coordinate y ↦ ℓ (y -ᵥ z).

theorem TauCeti.exists_homeomorph_fst_eq {V : Type u_1} {P : Type u_2} {F' : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [NormedAddCommGroup F'] [NormedSpace ℝ F'] (e : V ≃L[ℝ] ℝ × F') (ℓ : StrongDual ℝ V) (hℓ : ℓ (e.symm (1, 0)) ≠ 0) (z : P) : ∃ (Φ : P ≃ₜ ℝ × F'), ∀ (y : P), (Φ y).1 = ℓ (y -ᵥ z)

A continuous linear equivalence e : V ≃L[ℝ] ℝ × F' can have its first coordinate replaced by any continuous functional ℓ not vanishing on e.symm (1, 0). Centred at z, this gives a homeomorphism P ≃ₜ ℝ × F' whose first coordinate is y ↦ ℓ (y -ᵥ z).