inner_right_eq_zero_of_mem — Mathlib

English

If a tangent at p to as exists, then for any x ∈ as, the inner product ⟪p − center, x − p⟫ equals 0.

Русский

Если существует касательная в точке p к as, для любого x ∈ as выполняется ⟪p − center, x − p⟫ = 0.

LaTeX

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

Lean4

theorem inner_right_eq_zero_of_mem {s : Sphere P} {p : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) {x : P}
    (hx : x ∈ as) : ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0 :=
  mem_orthRadius_iff_inner_right.1 (h.le_orthRadius hx)

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