mem_tangentSet_iff — Mathlib

English

For any as and s, q ∈ tangentSet iff there exists p with q ∈ s and s.orthRadius(p) = as.

Русский

Для любых as и s верно: q принадлежит tangentSet тогда и только тогда, когда существует p such that q ∈ s и s.orthRadius(p) = as.

LaTeX

$$$ q \\in s.tangentSet \\iff \\exists p, p \\in s \\land s.orthRadius(p) = as $$$

Lean4

theorem mem_tangentSet_iff {as : AffineSubspace ℝ P} {s : Sphere P} :
    as ∈ s.tangentSet ↔ ∃ p, p ∈ s ∧ s.orthRadius p = as :=
  Iff.rfl

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