inner_pos_of_dist_lt_radius — Mathlib

English

If p1 is on a sphere and p2 is within or on the sphere, then the inner product ⟪p1−p2, p1−center⟫ is nonnegative.

Русский

Если p1 лежит на сфере, а p2 внутри или на сфере, то ⟪p1−p2, p1−центр⟫ неотрицательно.

LaTeX

$$0 ≤ ⟪p1−p2, p1−center⟫$$

Lean4

/-- Given a point on a sphere and a point inside it, the inner product between the difference of
those points and the radius vector is positive. -/
theorem inner_pos_of_dist_lt_radius {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : dist p₂ s.center < s.radius) :
    0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ := by
  by_cases h : p₁ = p₂
  · rw [h, mem_sphere] at hp₁
    exact False.elim (hp₂.ne hp₁)
  exact (inner_pos_or_eq_of_dist_le_radius hp₁ hp₂.le).resolve_right h

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