instChartedSpaceSphere — Mathlib

English

The source of stereographic' is the complement of the point v on the sphere.

Русский

Источник stereographic' — дополнение к точке v на сфере.

LaTeX

$$$(stereographic' n v).source = { v }^{\\mathrm{c}}$$$

Lean4

/-- The unit sphere in an `n + 1`-dimensional inner product space `E` is a charted space
modelled on the Euclidean space of dimension `n`. -/
instance instChartedSpaceSphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
    ChartedSpace (EuclideanSpace ℝ (Fin n)) (sphere (0 : E) 1)
    where
  atlas := {f | ∃ v : sphere (0 : E) 1, f = stereographic' n v}
  chartAt v := stereographic' n (-v)
  mem_chart_source v := by simpa using ne_neg_of_mem_unit_sphere ℝ v
  chart_mem_atlas v := ⟨-v, rfl⟩

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