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