# Topological properties of affine spaces and maps #

This file contains a few facts regarding the continuity of affine maps.

source
theorem AffineMap.continuous_linear_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [AddCommGroup W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] [Ring R] [Module R V] [Module R W] {f : P →ᵃ[R] Q} :
Continuous ⇑f.linear ↔ Continuous ⇑f

If `f` is an affine map, then its linear part is continuous iff `f` is continuous.

source
@[deprecated AffineMap.continuous_linear_iff (since := "2025-09-13")]
theorem AffineMap.continuous_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [AddCommGroup W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] [Ring R] [Module R V] [Module R W] {f : P →ᵃ[R] Q} :
Continuous ⇑f ↔ Continuous ⇑f.linear

An affine map is continuous iff its underlying linear map is continuous. See also `AffineMap.continuous_linear_iff`.

source
theorem AffineMap.isOpenMap_linear_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [AddCommGroup W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] [Ring R] [Module R V] [Module R W] {f : P →ᵃ[R] Q} :
IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

If `f` is an affine map, then its linear part is an open map iff `f` is an open map.

source
theorem AffineMap.lineMap_continuous_uncurry {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] :
Continuous fun (pqt : P × P × R) => (lineMap pqt.1 pqt.2.1) pqt.2.2

The line map is continuous in all arguments.

source
theorem AffineMap.lineMap_continuous {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] {p q : P} :
Continuous ⇑(lineMap p q)

The line map is continuous.

source
theorem Filter.Tendsto.lineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] {α : Type u_6} {l : Filter α} {f₁ f₂ : α → P} {g : α → R} {p₁ p₂ : P} {c : R} (h₁ : Tendsto f₁ l (nhds p₁)) (h₂ : Tendsto f₂ l (nhds p₂)) (hg : Tendsto g l (nhds c)) :
Tendsto (fun (x : α) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) l (nhds ((AffineMap.lineMap p₁ p₂) c))
source
theorem Filter.Tendsto.midpoint {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] {α : Type u_6} {l : Filter α} [Invertible 2] {f₁ f₂ : α → P} {p₁ p₂ : P} (h₁ : Tendsto f₁ l (nhds p₁)) (h₂ : Tendsto f₂ l (nhds p₂)) :
Tendsto (fun (x : α) => _root_.midpoint R (f₁ x) (f₂ x)) l (nhds (_root_.midpoint R p₁ p₂))
source
theorem ContinuousWithinAt.lineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [TopologicalSpace X] {f₁ f₂ : X → P} {g : X → R} {s : Set X} {x : X} (h₁ : ContinuousWithinAt f₁ s x) (h₂ : ContinuousWithinAt f₂ s x) (hg : ContinuousWithinAt g s x) :
ContinuousWithinAt (fun (x : X) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s x
source
theorem ContinuousAt.lineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [TopologicalSpace X] {f₁ f₂ : X → P} {g : X → R} {x : X} (h₁ : ContinuousAt f₁ x) (h₂ : ContinuousAt f₂ x) (hg : ContinuousAt g x) :
ContinuousAt (fun (x : X) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) x
source
theorem ContinuousOn.lineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [TopologicalSpace X] {f₁ f₂ : X → P} {g : X → R} {s : Set X} (h₁ : ContinuousOn f₁ s) (h₂ : ContinuousOn f₂ s) (hg : ContinuousOn g s) :
ContinuousOn (fun (x : X) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s
source
theorem Continuous.lineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Ring R] [Module R V] [TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [TopologicalSpace X] {f₁ f₂ : X → P} {g : X → R} (h₁ : Continuous f₁) (h₂ : Continuous f₂) (hg : Continuous g) :
Continuous fun (x : X) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)
source
theorem AffineMap.homothety_continuous {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [CommRing R] [Module R V] [ContinuousConstSMul R V] (x : P) (t : R) :
Continuous ⇑(homothety x t)
source
theorem eventually_homothety_mem_of_mem_interior (R : Type u_1) {W : Type u_4} {Q : Type u_5} [AddCommGroup W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] [CommRing R] [TopologicalSpace R] [Module R W] [ContinuousSMul R W] (x : Q) {s : Set Q} {y : Q} (hy : y ∈ interior s) :
∀ᶠ (δ : R) in nhds 1, (AffineMap.homothety x δ) y ∈ s
source
theorem eventually_homothety_image_subset_of_finite_subset_interior (R : Type u_1) {W : Type u_4} {Q : Type u_5} [AddCommGroup W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] [CommRing R] [TopologicalSpace R] [Module R W] [ContinuousSMul R W] (x : Q) {s t : Set Q} (ht : t.Finite) (h : t ⊆ interior s) :
∀ᶠ (δ : R) in nhds 1, ⇑(AffineMap.homothety x δ) '' t ⊆ s
source
theorem AffineMap.homothety_isOpenMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [Field R] [Module R V] [ContinuousConstSMul R V] (x : P) (t : R) (ht : t ≠ 0) :
IsOpenMap ⇑(homothety x t)