# Torsors of normed space actions. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem affine_subspace.is_closed_direction_iff {W : Type u_4} {Q : Type u_5} [metric_space Q] [ Q] {𝕜 : Type u_6} [normed_field 𝕜] [ W] (s : Q) :
@[simp]
theorem dist_center_homothety {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( c) p₂) = c * p₂
@[simp]
theorem nndist_center_homothety {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( c) p₂) = c‖₊ * p₂
@[simp]
theorem dist_homothety_center {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_dist.dist ( c) p₂) p₁ = c * p₂
@[simp]
theorem nndist_homothety_center {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_nndist.nndist ( c) p₂) p₁ = c‖₊ * p₂
@[simp]
theorem dist_line_map_line_map {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c₁ c₂ : 𝕜) :
has_dist.dist ( p₂) c₁) ( p₂) c₂) = c₂ * p₂
@[simp]
theorem nndist_line_map_line_map {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c₁ c₂ : 𝕜) :
has_nndist.nndist ( p₂) c₁) ( p₂) c₂) = c₂ * p₂
theorem lipschitz_with_line_map {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) :
lipschitz_with p₂) p₂)
@[simp]
theorem dist_line_map_left {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_dist.dist ( p₂) c) p₁ = c * p₂
@[simp]
theorem nndist_line_map_left {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_nndist.nndist ( p₂) c) p₁ = c‖₊ * p₂
@[simp]
theorem dist_left_line_map {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( p₂) c) = c * p₂
@[simp]
theorem nndist_left_line_map {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( p₂) c) = c‖₊ * p₂
@[simp]
theorem dist_line_map_right {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_dist.dist ( p₂) c) p₂ = 1 - c * p₂
@[simp]
theorem nndist_line_map_right {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_nndist.nndist ( p₂) c) p₂ = 1 - c‖₊ * p₂
@[simp]
theorem dist_right_line_map {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( p₂) c) = 1 - c * p₂
@[simp]
theorem nndist_right_line_map {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( p₂) c) = 1 - c‖₊ * p₂
@[simp]
theorem dist_homothety_self {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_dist.dist ( c) p₂) p₂ = 1 - c * p₂
@[simp]
theorem nndist_homothety_self {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
has_nndist.nndist ( c) p₂) p₂ = 1 - c‖₊ * p₂
@[simp]
theorem dist_self_homothety {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( c) p₂) = 1 - c * p₂
@[simp]
theorem nndist_self_homothety {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
( c) p₂) = 1 - c‖₊ * p₂
@[simp]
theorem dist_left_midpoint {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
(midpoint 𝕜 p₁ p₂) = 2⁻¹ * p₂
@[simp]
theorem nndist_left_midpoint {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
(midpoint 𝕜 p₁ p₂) = 2‖₊⁻¹ * p₂
@[simp]
theorem dist_midpoint_left {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
has_dist.dist (midpoint 𝕜 p₁ p₂) p₁ = 2⁻¹ * p₂
@[simp]
theorem nndist_midpoint_left {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
has_nndist.nndist (midpoint 𝕜 p₁ p₂) p₁ = 2‖₊⁻¹ * p₂
@[simp]
theorem dist_midpoint_right {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
has_dist.dist (midpoint 𝕜 p₁ p₂) p₂ = 2⁻¹ * p₂
@[simp]
theorem nndist_midpoint_right {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
has_nndist.nndist (midpoint 𝕜 p₁ p₂) p₂ = 2‖₊⁻¹ * p₂
@[simp]
theorem dist_right_midpoint {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
(midpoint 𝕜 p₁ p₂) = 2⁻¹ * p₂
@[simp]
theorem nndist_right_midpoint {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
(midpoint 𝕜 p₁ p₂) = 2‖₊⁻¹ * p₂
theorem dist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ p₃ p₄ : P) :
has_dist.dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) p₃ + p₄) / 2
theorem nndist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_3} [ P] {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ p₃ p₄ : P) :
has_nndist.nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) p₃ + p₄) / 2‖₊
theorem antilipschitz_with_line_map {W : Type u_4} {Q : Type u_5} [metric_space Q] [ Q] {𝕜 : Type u_6} [normed_field 𝕜] [ W] {p₁ p₂ : Q} (h : p₁ p₂) :
p₂)
theorem eventually_homothety_mem_of_mem_interior {W : Type u_4} {Q : Type u_5} [metric_space Q] [ Q] (𝕜 : Type u_6) [normed_field 𝕜] [ 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} [metric_space Q] [ Q] (𝕜 : Type u_6) [normed_field 𝕜] [ W] (x : Q) {s t : set Q} (ht : t.finite) (h : t ) :
∀ᶠ (δ : 𝕜) in nhds 1, δ) '' t s
theorem dist_midpoint_midpoint_le {V : Type u_2} [ V] (p₁ p₂ p₃ p₄ : V) :
has_dist.dist p₁ p₂) p₃ p₄) p₃ + p₄) / 2
theorem nndist_midpoint_midpoint_le {V : Type u_2} [ V] (p₁ p₂ p₃ p₄ : V) :
has_nndist.nndist p₁ p₂) p₃ p₄) p₃ + p₄) / 2
noncomputable def affine_map.of_map_midpoint {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [ P] [metric_space Q] [ Q] [ V] [ W] (f : P Q) (h : (x y : P), f x y) = (f x) (f y)) (hfc : continuous f) :

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

Equations