stereographic'_target — Mathlib

English

The target of stereographic' is the full Euclidean space dimension n, i.e., Set.univ in the Euclidean target.

Русский

Целевая область stereographic' — полное евклидово пространство размерности n.

LaTeX

$$$(stereographic' n v).target = Set.univ$$$

Lean4

@[simp]
theorem stereographic'_target {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
    (stereographic' n v).target = Set.univ := by simp [stereographic']

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