mem_tangentsFrom_iff — Mathlib

English

An affine subspace as is a member of tangentsFrom p if and only if as is a member of tangentSet and p ∈ as.

Русский

Подплощадь аффинного пространства принадлежит tangentsFrom(p) тогда и только тогда, когда она принадлежит tangentSet и p ∈ as.

LaTeX

$$$ as \\in s.tangentsFrom(p) \\iff as \\in s.tangentSet \\wedge p \\in as $$$

Lean4

theorem mem_tangentsFrom_iff {as : AffineSubspace ℝ P} {s : Sphere P} {p : P} :
    as ∈ s.tangentsFrom p ↔ as ∈ s.tangentSet ∧ p ∈ as :=
  Iff.rfl

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