toMeasurableInv

Mathlib.MeasureTheory.Group.Arithmetic

URI: https://scilib.ai/kg/mathlib#DiscreteMeasurableSpace.toMeasurableInv

← MathLib Explorer

English

On a type α with a discrete measurable structure, the inversion map α → α is measurable.

Русский

На типе α с дискретной структурой измеримости инверсия является измеримой.

LaTeX

$$$\text{MeasurableInv}\,\alpha$$$

Lean4

@[to_additive] -- See note [lower instance priority]

instance (priority := 100) toMeasurableInv [DiscreteMeasurableSpace α] : MeasurableInv α :=
  ⟨.of_discrete⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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