α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint]
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
try infer_instance
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / ‖2‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul]
no goals
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / ‖2‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _)
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
α : Type ?u.73606
V : Type u_3
P : Type u_1
W : Type ?u.73615
Q : Type ?u.73618
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
infer_instance