torusMap_zero_radius

Mathlib.MeasureTheory.Integral.TorusIntegral

URI: https://scilib.ai/kg/mathlib#torusMap_zero_radius

English

When radius is zero, torusMap reduces to a constant map with value c.

Русский

Радиус нулевой: torusMap становится константой равной c.

LaTeX

$$$\\mathrm{torusMap}(c,0) = \\mathrm{const}(\\mathbb{R}^n)\\ c$$$

Lean4

@[simp]
theorem torusMap_zero_radius (c : ℂⁿ) : torusMap c 0 = const (ℝⁿ) c :=
  funext fun _ ↦ torusMap_eq_center_iff.2 rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru