# Torsors of normed space actions. #

theorem AffineSubspace.isClosed_direction_iff {W : Type u_2} {Q : Type u_1} [] [] {𝕜 : Type u_3} [] [] (s : ) :
@[simp]
theorem dist_center_homothety {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist p₁ (↑() p₂) = c * dist p₁ p₂
@[simp]
theorem nndist_center_homothety {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist p₁ (↑() p₂) = c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_homothety_center {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist (↑() p₂) p₁ = c * dist p₁ p₂
@[simp]
theorem nndist_homothety_center {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist (↑() p₂) p₁ = c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_lineMap_lineMap {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c₁ : 𝕜) (c₂ : 𝕜) :
dist (↑() c₁) (↑() c₂) = dist c₁ c₂ * dist p₁ p₂
@[simp]
theorem nndist_lineMap_lineMap {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c₁ : 𝕜) (c₂ : 𝕜) :
nndist (↑() c₁) (↑() c₂) = nndist c₁ c₂ * nndist p₁ p₂
theorem lipschitzWith_lineMap {V : Type u_3} {P : Type u_2} [] {𝕜 : Type u_1} [] [] (p₁ : P) (p₂ : P) :
LipschitzWith (nndist p₁ p₂) ↑()
@[simp]
theorem dist_lineMap_left {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist (↑() c) p₁ = c * dist p₁ p₂
@[simp]
theorem nndist_lineMap_left {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist (↑() c) p₁ = c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_left_lineMap {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist p₁ (↑() c) = c * dist p₁ p₂
@[simp]
theorem nndist_left_lineMap {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist p₁ (↑() c) = c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_lineMap_right {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist (↑() c) p₂ = 1 - c * dist p₁ p₂
@[simp]
theorem nndist_lineMap_right {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist (↑() c) p₂ = 1 - c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_right_lineMap {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist p₂ (↑() c) = 1 - c * dist p₁ p₂
@[simp]
theorem nndist_right_lineMap {V : Type u_3} {P : Type u_1} [] {𝕜 : Type u_2} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist p₂ (↑() c) = 1 - c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_homothety_self {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist (↑() p₂) p₂ = 1 - c * dist p₁ p₂
@[simp]
theorem nndist_homothety_self {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist (↑() p₂) p₂ = 1 - c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_self_homothety {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
dist p₂ (↑() p₂) = 1 - c * dist p₁ p₂
@[simp]
theorem nndist_self_homothety {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p₁ : P) (p₂ : P) (c : 𝕜) :
nndist p₂ (↑() p₂) = 1 - c‖₊ * nndist p₁ p₂
@[simp]
theorem dist_left_midpoint {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
dist p₁ (midpoint 𝕜 p₁ p₂) = 2⁻¹ * dist p₁ p₂
@[simp]
theorem nndist_left_midpoint {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
nndist p₁ (midpoint 𝕜 p₁ p₂) = * nndist p₁ p₂
@[simp]
theorem dist_midpoint_left {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
dist (midpoint 𝕜 p₁ p₂) p₁ = 2⁻¹ * dist p₁ p₂
@[simp]
theorem nndist_midpoint_left {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
nndist (midpoint 𝕜 p₁ p₂) p₁ = * nndist p₁ p₂
@[simp]
theorem dist_midpoint_right {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
dist (midpoint 𝕜 p₁ p₂) p₂ = 2⁻¹ * dist p₁ p₂
@[simp]
theorem nndist_midpoint_right {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
nndist (midpoint 𝕜 p₁ p₂) p₂ = * nndist p₁ p₂
@[simp]
theorem dist_right_midpoint {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
dist p₂ (midpoint 𝕜 p₁ p₂) = 2⁻¹ * dist p₁ p₂
@[simp]
theorem nndist_right_midpoint {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) :
nndist p₂ (midpoint 𝕜 p₁ p₂) = * nndist p₁ p₂
theorem dist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) :
dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) (dist p₁ p₃ + dist p₂ p₄) / 2
theorem nndist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] [] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) :
nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) (nndist p₁ p₃ + nndist p₂ p₄) / 2‖₊
@[simp]
theorem dist_pointReflection_left {V : Type u_2} {P : Type u_1} [] (p : P) (q : P) :
dist (↑() q) p = dist p q
@[simp]
theorem dist_left_pointReflection {V : Type u_2} {P : Type u_1} [] (p : P) (q : P) :
dist p (↑() q) = dist p q
@[simp]
theorem dist_pointReflection_right {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p : P) (q : P) :
dist (↑() q) q = 2 * dist p q
@[simp]
theorem dist_right_pointReflection {V : Type u_2} {P : Type u_1} [] {𝕜 : Type u_3} [] [] (p : P) (q : P) :
dist q (↑() q) = 2 * dist p q
theorem antilipschitzWith_lineMap {W : Type u_3} {Q : Type u_1} [] [] {𝕜 : Type u_2} [] [] {p₁ : Q} {p₂ : Q} (h : p₁ p₂) :
AntilipschitzWith (nndist p₁ p₂)⁻¹ ↑()
theorem eventually_homothety_mem_of_mem_interior {W : Type u_3} {Q : Type u_1} [] [] (𝕜 : Type u_2) [] [] (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_3} {Q : Type u_1} [] [] (𝕜 : Type u_2) [] [] (x : Q) {s : Set Q} {t : Set Q} (ht : ) (h : t ) :
∀ᶠ (δ : 𝕜) in nhds 1, ↑() '' t s
theorem dist_midpoint_midpoint_le {V : Type u_1} [] (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_1} [] (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_1} {P : Type u_2} {W : Type u_3} {Q : Type u_4} [] [] [] [] [] (f : PQ) (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.

Instances For