Topological properties of affine spaces and maps

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

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.

@[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.

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.

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.

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.

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))

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₂))

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

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

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

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)

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)

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

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

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)