mem_orthRadius_iff_inner_right — Mathlib

English

Let s be a sphere with center s.center in a Euclidean-like space P. For any p, x in P, x lies in the orthRadius of s with respect to p if and only if the inner product of p − s.center and x − p is zero; equivalently, p − s.center is orthogonal to x − p.

Русский

Пусть s — сфера с центром s.center в евклидовом подобном пространстве P. Для любых p, x ∈ P верно: x ∈ s.orthRadius p тогда и только тогда, когда скалярное произведение (p − s.center) и (x − p) равно нулю; эквивалентно, вектор p − s.center ортогонален вектору x − p.

LaTeX

$$$ x \in s.orthRadius p \iff \langle p - s.center, x - p \rangle = 0 $$$

Lean4

theorem mem_orthRadius_iff_inner_right {s : Sphere P} {p x : P} : x ∈ s.orthRadius p ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0 := by
  rw [mem_orthRadius_iff_inner_left, inner_eq_zero_symm]

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