continuousOn_stereoToFun — Mathlib

English

The forward stereographic projection stereoToFun v is ContDiffOn on the domain where the inner product condition holds, and this continues to hold after composition with the orthogonal projection.

Русский

Прямое стереографическое проецирование stereoToFun v гладко на области, где выполнено условие по скалярному продукту, и это сохраняется после композиции с ортогональной проекцией.

LaTeX

$$ContDiffOn Real n (stereoToFun v) (setOf x => Ne (ContinuousLinearMap.funLike.coe (ContinuousLinearMap.funLike.coe (innerSL Real) v) x) 1)$$

Lean4

theorem continuousOn_stereoToFun : ContinuousOn (stereoToFun v) {x : E | innerSL _ v x ≠ (1 : ℝ)} :=
  (contDiffOn_stereoToFun (n := 0)).continuousOn

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