polarCoordReal_source — Mathlib

English

The source of polarCoordReal(K) is the full product space with the polar coordinate source on the second factor.

Русский

Источник polarCoordReal(K) — полный продукт пространства с источником полярных координат на второй компоненте.

LaTeX

$$$\\operatorname{polarCoordReal}(K).\\operatorname{source} = \\operatorname{Set.univ} \\times\\! \\bigl(\\operatorname{Set.univ.pi} (\\lambda\\_ , \\operatorname{polarCoord.source})\\bigr)$$$

Lean4

theorem polarCoordReal_source : (polarCoordReal K).source = Set.univ ×ˢ (Set.univ.pi fun _ ↦ polarCoord.source) :=
  rfl

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