signedInfDist_singleton — Mathlib

English

If s is the affine span of a singleton {q}, then s.signedInfDist(p) equals signedDist(p - q, q).

Русский

Если s — аффинное множество, порождённое единственным пунктом {q}, то s.signedInfDist(p) = signedDist(p - q, q).

LaTeX

$$$(\text{affineSpan }\mathbb{R}({q}:\{q\})).signedInfDist(p) = \operatorname{signedDist}(p - q, q)$$$

Lean4

theorem signedInfDist_singleton : (affineSpan ℝ ({ q } : Set P)).signedInfDist p = signedDist (p -ᵥ q) q := by
  simpa using signedInfDist_eq_signedDist_of_mem (mem_affineSpan ℝ (Set.mem_singleton q))

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