isTangentAt_orthRadius_iff_mem — Mathlib

English

A sphere S is tangent to the affine subspace s.orthRadius(p) at p if and only if p belongs to S.

Русский

Сфера S касается аффинного подпространства s.orthRadius(p) в точке p тогда, когда p принадлежит сфере.

LaTeX

$$$ s.IsTangentAt p (s.orthRadius p) \\iff p \\in s $$$

Lean4

@[simp]
theorem isTangentAt_orthRadius_iff_mem {s : Sphere P} {p : P} : s.IsTangentAt p (s.orthRadius p) ↔ p ∈ s :=
  ⟨fun h ↦ h.mem_sphere, fun h ↦ ⟨h, self_mem_orthRadius _ _, le_rfl⟩⟩

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