α : Type ?u.99524
V : Type u_1
P : Type ?u.99530
W : Type ?u.99533
Q : Type ?u.99536
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
this : dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
α : Type ?u.99524
V : Type u_1
P : Type ?u.99530
W : Type ?u.99533
Q : Type ?u.99536
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
have := dist_midpoint_midpoint_le' (𝕜 := ℝ) p₁ p₂ p₃ p₄
α : Type ?u.99524
V : Type u_1
P : Type ?u.99530
W : Type ?u.99533
Q : Type ?u.99536
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
this : dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
α : Type ?u.99524
V : Type u_1
P : Type ?u.99530
W : Type ?u.99533
Q : Type ?u.99536
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
this : dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
rw [Real.norm_eq_abs, abs_two] at this
no goals
α : Type ?u.99524
V : Type u_1
P : Type ?u.99530
W : Type ?u.99533
Q : Type ?u.99536
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
this : dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
exact this