inv

Mathlib.MeasureTheory.Group.Arithmetic

URI: https://scilib.ai/kg/mathlib#MeasurableSet.inv

English

For any measurable set s of a group G with inversion, the set of inverses s^{-1} is measurable.

Русский

Для любой измеримой множества s в группе G с инверсией множество инверсий s^{-1} измеримо.

LaTeX

$$$s\\text{ Measurable} \\Rightarrow s^{-1}\\text{ Measurable}$$$

Lean4

@[to_additive]
theorem inv {s : Set G} (hs : MeasurableSet s) : MeasurableSet s⁻¹ :=
  measurable_inv hs

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

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

Разделы

Аффилиация

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