measurable_symm

Mathlib.MeasureTheory.Constructions.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.measurable_symm

English

The symmetry map σ on the unit interval is measurable.

Русский

Симметричная карта σ на единичном интервале измерима.

LaTeX

$$$\text{Measurable}(\sigma)$$$

Lean4

@[fun_prop, measurability]
theorem measurable_symm : Measurable σ :=
  continuous_symm.measurable

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

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

Разделы

Аффилиация

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