continuous_stereoInvFun — Mathlib

English

The stereographic inverse stereoInvFun is a continuous map with respect to the base topology; it is a continuous inverse on its domain.

Русский

Обратная стереографическая отображение stereoInvFun непрерывна на своей области определения.

LaTeX

$$$\\text{Continuous} (stereoInvFun \\ hv) \\, (hv: \\|v\\|=1)$$$

Lean4

theorem continuous_stereoInvFun (hv : ‖v‖ = 1) : Continuous (stereoInvFun hv) :=
  continuous_induced_rng.2 ((contDiff_stereoInvFunAux (m := 0)).continuous.comp continuous_subtype_val)

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