# Torsors of normed space actions. #

theorem AffineSubspace.isClosed_direction_iff {W : Type u_4} {Q : Type u_5} [] [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ W] (s : AffineSubspace ๐ Q) :
IsClosed โs.direction โ IsClosed โs
@[simp]
theorem dist_center_homothety {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist pโ ((AffineMap.homothety pโ c) pโ) = * dist pโ pโ
@[simp]
theorem nndist_center_homothety {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist pโ ((AffineMap.homothety pโ c) pโ) = * nndist pโ pโ
@[simp]
theorem dist_homothety_center {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist ((AffineMap.homothety pโ c) pโ) pโ = * dist pโ pโ
@[simp]
theorem nndist_homothety_center {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist ((AffineMap.homothety pโ c) pโ) pโ = * nndist pโ pโ
@[simp]
theorem dist_lineMap_lineMap {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (cโ : ๐) (cโ : ๐) :
dist ((AffineMap.lineMap pโ pโ) cโ) ((AffineMap.lineMap pโ pโ) cโ) = dist cโ cโ * dist pโ pโ
@[simp]
theorem nndist_lineMap_lineMap {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (cโ : ๐) (cโ : ๐) :
nndist ((AffineMap.lineMap pโ pโ) cโ) ((AffineMap.lineMap pโ pโ) cโ) = nndist cโ cโ * nndist pโ pโ
theorem lipschitzWith_lineMap {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) :
LipschitzWith (nndist pโ pโ) โ(AffineMap.lineMap pโ pโ)
@[simp]
theorem dist_lineMap_left {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist ((AffineMap.lineMap pโ pโ) c) pโ = * dist pโ pโ
@[simp]
theorem nndist_lineMap_left {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist ((AffineMap.lineMap pโ pโ) c) pโ = * nndist pโ pโ
@[simp]
theorem dist_left_lineMap {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist pโ ((AffineMap.lineMap pโ pโ) c) = * dist pโ pโ
@[simp]
theorem nndist_left_lineMap {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist pโ ((AffineMap.lineMap pโ pโ) c) = * nndist pโ pโ
@[simp]
theorem dist_lineMap_right {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist ((AffineMap.lineMap pโ pโ) c) pโ = โ1 - cโ * dist pโ pโ
@[simp]
theorem nndist_lineMap_right {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist ((AffineMap.lineMap pโ pโ) c) pโ = โ1 - cโโ * nndist pโ pโ
@[simp]
theorem dist_right_lineMap {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist pโ ((AffineMap.lineMap pโ pโ) c) = โ1 - cโ * dist pโ pโ
@[simp]
theorem nndist_right_lineMap {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist pโ ((AffineMap.lineMap pโ pโ) c) = โ1 - cโโ * nndist pโ pโ
@[simp]
theorem dist_homothety_self {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist ((AffineMap.homothety pโ c) pโ) pโ = โ1 - cโ * dist pโ pโ
@[simp]
theorem nndist_homothety_self {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist ((AffineMap.homothety pโ c) pโ) pโ = โ1 - cโโ * nndist pโ pโ
@[simp]
theorem dist_self_homothety {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
dist pโ ((AffineMap.homothety pโ c) pโ) = โ1 - cโ * dist pโ pโ
@[simp]
theorem nndist_self_homothety {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] (pโ : P) (pโ : P) (c : ๐) :
nndist pโ ((AffineMap.homothety pโ c) pโ) = โ1 - cโโ * nndist pโ pโ
@[simp]
theorem dist_left_midpoint {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
dist pโ (midpoint ๐ pโ pโ) = * dist pโ pโ
@[simp]
theorem nndist_left_midpoint {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
nndist pโ (midpoint ๐ pโ pโ) = * nndist pโ pโ
@[simp]
theorem dist_midpoint_left {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
dist (midpoint ๐ pโ pโ) pโ = * dist pโ pโ
@[simp]
theorem nndist_midpoint_left {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
nndist (midpoint ๐ pโ pโ) pโ = * nndist pโ pโ
@[simp]
theorem dist_midpoint_right {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
dist (midpoint ๐ pโ pโ) pโ = * dist pโ pโ
@[simp]
theorem nndist_midpoint_right {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
nndist (midpoint ๐ pโ pโ) pโ = * nndist pโ pโ
@[simp]
theorem dist_right_midpoint {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
dist pโ (midpoint ๐ pโ pโ) = * dist pโ pโ
@[simp]
theorem nndist_right_midpoint {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) :
nndist pโ (midpoint ๐ pโ pโ) = * nndist pโ pโ
theorem dist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) (pโ : P) (pโ : P) :
dist (midpoint ๐ pโ pโ) (midpoint ๐ pโ pโ) โค (dist pโ pโ + dist pโ pโ) /
theorem nndist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_3} [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ V] [] (pโ : P) (pโ : P) (pโ : P) (pโ : P) :
nndist (midpoint ๐ pโ pโ) (midpoint ๐ pโ pโ) โค (nndist pโ pโ + nndist pโ pโ) /
@[simp]
theorem dist_pointReflection_left {V : Type u_2} {P : Type u_3} [] (p : P) (q : P) :
dist () p = dist p q
@[simp]
theorem dist_left_pointReflection {V : Type u_2} {P : Type u_3} [] (p : P) (q : P) :
dist p () = dist p q
theorem dist_pointReflection_right {V : Type u_2} {P : Type u_3} [] (๐ : Type u_6) [NormedField ๐] [NormedSpace ๐ V] (p : P) (q : P) :
dist () q = * dist p q
theorem dist_right_pointReflection {V : Type u_2} {P : Type u_3} [] (๐ : Type u_6) [NormedField ๐] [NormedSpace ๐ V] (p : P) (q : P) :
dist q () = * dist p q
theorem antilipschitzWith_lineMap {W : Type u_4} {Q : Type u_5} [] [] {๐ : Type u_6} [NormedField ๐] [NormedSpace ๐ W] {pโ : Q} {pโ : Q} (h : pโ โ  pโ) :
AntilipschitzWith (nndist pโ pโ)โปยน โ(AffineMap.lineMap pโ pโ)
theorem eventually_homothety_mem_of_mem_interior {W : Type u_4} {Q : Type u_5} [] [] (๐ : Type u_6) [NormedField ๐] [NormedSpace ๐ W] (x : Q) {s : Set Q} {y : Q} (hy : y โ ) :
โแถ  (ฮด : ๐) in nhds 1, () y โ s
theorem eventually_homothety_image_subset_of_finite_subset_interior {W : Type u_4} {Q : Type u_5} [] [] (๐ : Type u_6) [NormedField ๐] [NormedSpace ๐ W] (x : Q) {s : Set Q} {t : Set Q} (ht : t.Finite) (h : t โ ) :
โแถ  (ฮด : ๐) in nhds 1, โ() '' t โ s
theorem dist_midpoint_midpoint_le {V : Type u_2} [] (pโ : V) (pโ : V) (pโ : V) (pโ : V) :
dist (midpoint โ pโ pโ) (midpoint โ pโ pโ) โค (dist pโ pโ + dist pโ pโ) / 2
theorem nndist_midpoint_midpoint_le {V : Type u_2} [] (pโ : V) (pโ : V) (pโ : V) (pโ : V) :
nndist (midpoint โ pโ pโ) (midpoint โ pโ pโ) โค (nndist pโ pโ + nndist pโ pโ) / 2
def AffineMap.ofMapMidpoint {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [] [] [] [] [] (f : P โ Q) (h : โ (x y : P), f () = midpoint โ (f x) (f y)) (hfc : ) :

A continuous map between two normed affine spaces is an affine map provided that it sends midpoints to midpoints.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DilationEquiv.smulTorsor_symm_apply {๐ : Type u_1} {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] {P : Type u_3} [] (c : P) {k : ๐} (hk : k โ  0) :
โ (x : P), ().symm x = ( โข fun (x : P) => x -แตฅ c) x
@[simp]
theorem DilationEquiv.smulTorsor_apply {๐ : Type u_1} {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] {P : Type u_3} [] (c : P) {k : ๐} (hk : k โ  0) :
โ (x : E), () x = k โข x +แตฅ c
def DilationEquiv.smulTorsor {๐ : Type u_1} {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] {P : Type u_3} [] (c : P) {k : ๐} (hk : k โ  0) :

Scaling by an element k of the scalar ring as a DilationEquiv with ratio โkโโ, mapping from a normed space to a normed torsor over that space sending 0 to c.

Equations
Instances For
@[simp]
theorem DilationEquiv.smulTorsor_ratio {๐ : Type u_1} {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] {P : Type u_3} [] {c : P} {k : ๐} (hk : k โ  0) {x : E} {y : E} (h : dist x y โ  0) :
@[simp]
theorem DilationEquiv.smulTorsor_preimage_ball {๐ : Type u_1} {E : Type u_2} [] [Module ๐ E] [BoundedSMul ๐ E] {P : Type u_3} [] {c : P} {k : ๐} (hk : k โ  0) :
โ() โปยน' =