inv

Mathlib.MeasureTheory.Group.Measure

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

English

If μ is a regular measure, then μ.inv is regular.

Русский

Если μ — регулярная мера, то μ.inv — регулярная мера.

LaTeX

$$$ \mu.regular \Rightarrow \mu^{\mathrm{inv}}.regular$$$

Lean4

@[to_additive]
instance inv [ContinuousInv G] [Regular μ] : Regular μ.inv :=
  Regular.map (Homeomorph.inv G)

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

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

Разделы

Аффилиация

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