stereographic_target — Mathlib

English

The target of the stereographic projection stereographic hv is the universal set, i.e., all points of the orthogonal complement are attainable.

Русский

Целевая область проекции stereographic hv — всякое множество; достигаются все точки (ℝ·v)⊥.

LaTeX

$$$\\text{stereographic } hv\\;\\text{target} = \\mathsf{Set.univ}$$$

Lean4

@[simp]
theorem stereographic_target (hv : ‖v‖ = 1) : (stereographic hv).target = Set.univ :=
  rfl

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