tangentsFrom — Mathlib

English

The set tangentsFrom(s,p) consists of all maximal tangent spaces to s that contain the point p.

Русский

Множество tangentsFrom(s,p) состоит из всех максимальных касательных пространств к s, проходящих через точку p.

LaTeX

$$$ \\mathrm{tangentsFrom}(s,p) = \\{ as \\in s.tangentSet \\mid p \\in as \\}$$$

Lean4

/-- The set of all maximal tangent spaces to the sphere `s` containing the point `p`. -/
def tangentsFrom (s : Sphere P) (p : P) : Set (AffineSubspace ℝ P) :=
  {as ∈ s.tangentSet | p ∈ as}

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