Torsors of normed space actions. #

theorem affine_subspace.is_closed_direction_iff {W : Type u_4} {Q : Type u_5} [metric_space Q] [ Q] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ W] (s : affine_subspace ๐ Q) :
@[simp]
theorem dist_center_homothety {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist pโ (โ(affine_map.homothety pโ c) pโ) = โฅcโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_homothety_center {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist (โ(affine_map.homothety pโ c) pโ) pโ = โฅcโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_line_map_line_map {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (cโ cโ : ๐) :
has_dist.dist (โ(affine_map.line_map pโ pโ) cโ) (โ(affine_map.line_map pโ pโ) cโ) = has_dist.dist cโ cโ * has_dist.dist pโ pโ
theorem lipschitz_with_line_map {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) :
lipschitz_with (has_nndist.nndist pโ pโ) โ(affine_map.line_map pโ pโ)
@[simp]
theorem dist_line_map_left {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist (โ(affine_map.line_map pโ pโ) c) pโ = โฅcโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_left_line_map {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist pโ (โ(affine_map.line_map pโ pโ) c) = โฅcโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_line_map_right {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist (โ(affine_map.line_map pโ pโ) c) pโ = โฅ1 - cโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_right_line_map {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist pโ (โ(affine_map.line_map pโ pโ) c) = โฅ1 - cโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_homothety_self {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist (โ(affine_map.homothety pโ c) pโ) pโ = โฅ1 - cโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_self_homothety {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] (pโ pโ : P) (c : ๐) :
has_dist.dist pโ (โ(affine_map.homothety pโ c) pโ) = โฅ1 - cโฅ * has_dist.dist pโ pโ
@[simp]
theorem dist_left_midpoint {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] [invertible 2] (pโ pโ : P) :
has_dist.dist pโ (midpoint ๐ pโ pโ) = โฅ2โฅโปยน * has_dist.dist pโ pโ
@[simp]
theorem dist_midpoint_left {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] [invertible 2] (pโ pโ : P) :
has_dist.dist (midpoint ๐ pโ pโ) pโ = โฅ2โฅโปยน * has_dist.dist pโ pโ
@[simp]
theorem dist_midpoint_right {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] [invertible 2] (pโ pโ : P) :
has_dist.dist (midpoint ๐ pโ pโ) pโ = โฅ2โฅโปยน * has_dist.dist pโ pโ
@[simp]
theorem dist_right_midpoint {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] [invertible 2] (pโ pโ : P) :
has_dist.dist pโ (midpoint ๐ pโ pโ) = โฅ2โฅโปยน * has_dist.dist pโ pโ
theorem dist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_3} [ P] {๐ : Type u_6} [normed_field ๐] [normed_space ๐ V] [invertible 2] (pโ pโ pโ pโ : P) :
has_dist.dist (midpoint ๐ pโ pโ) (midpoint ๐ pโ pโ) โค (has_dist.dist pโ pโ + has_dist.dist 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 ๐] [normed_space ๐ W] {pโ pโ : Q} (h : 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 ๐] [normed_space ๐ 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 ๐] [normed_space ๐ 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โ) โค (has_dist.dist pโ pโ + has_dist.dist 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