abs_signedDist_eq_dist_iff_vsub_mem_span

English

The equality |signedDist v p q| = dist p q holds if and only if q −ᵥ p lies in the span of v.

Русский

Равенство |signedDist v p q| = dist p q эквивалентно тому, что q −ᵥ p лежит в развязке по v.

LaTeX

$$abs(signedDist v p q) = dist p q \Leftrightarrow q -ᵥ p ∈ \mathbb{R} \cdot v$$

Lean4

theorem abs_signedDist_eq_dist_iff_vsub_mem_span : |signedDist v p q| = dist p q ↔ q -ᵥ p ∈ ℝ ∙ v :=
  by
  rw [Submodule.mem_span_singleton]
  rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, real_inner_smul_left, abs_mul, abs_inv,
    abs_norm]
  by_cases h : v = 0
  · simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]
  rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
  rw [← Real.norm_eq_abs, ((norm_inner_eq_norm_tfae ℝ v (q -ᵥ p)).out 0 2 :)]
  simp [h, eq_comm]

Похожие утверждения