notMem_of_dist_lt — Mathlib

English

If p is closer to the center than the radius, then p is not in as. Equivalently, dist(p, center) < radius implies p ∉ as.

Русский

Если расстояние от p до центра меньше радиуса, то p не принадлежит as.

LaTeX

$$$ \\operatorname{dist}(p, s.center) < s.radius \\Rightarrow p \\notin as $$$

Lean4

theorem notMem_of_dist_lt {s : Sphere P} {as : AffineSubspace ℝ P} (h : s.IsTangent as) {p : P}
    (hp : dist p s.center < s.radius) : p ∉ as := by
  contrapose! hp
  exact h.radius_le_dist_center hp

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