isTangent_of_mem_tangentSet — Mathlib

English

Let s be a sphere in P and as any affine subspace of P. If as is one of the maximal tangent spaces to s (i.e., as ∈ tangentSet), then s is tangent to as.

Русский

Пусть s — сфера в P, а as — аффинное подпредпосылка пространства. Если as является одной из максимальных касательных сфер к s (то есть as ∈ tangentSet), то s касается as.

LaTeX

$$$ \\forall as \\in \\mathrm{AffineSubspace}_{\\mathbb{R}}P,\\ \\forall s \\in \\mathrm{Sphere}P,\\quad as \\in \\mathrm{tangentSet}(s) \\Rightarrow s \\IsTangent as $$$

Lean4

theorem isTangent_of_mem_tangentSet {as : AffineSubspace ℝ P} {s : Sphere P} (h : as ∈ s.tangentSet) : s.IsTangent as :=
  by
  rcases h with ⟨p, hps, rfl⟩
  exact isTangent_orthRadius_iff_mem.2 hps

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