toSphere_ne_zero

Mathlib.MeasureTheory.Constructions.HaarToSphere

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.toSphere_ne_zero

English

If the space E is nontrivial, then μ.toSphere ≠ 0 for a Haar measure μ.

Русский

Если пространство E не тривиально, то μ.toSphere ≠ 0 для меры Хаара μ.

LaTeX

$$$\\mu.toSphere \\neq 0$ безусловно при не тривиальности E$$

Lean4

@[simp]
theorem toSphere_ne_zero [Nontrivial E] : μ.toSphere ≠ 0 := by simp [toSphere_eq_zero_iff, not_subsingleton]

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

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

Разделы

Аффилиация

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