innerRegular_inv_iff

Mathlib.MeasureTheory.Group.Measure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.innerRegular_inv_iff

English

The image of an inner regular measure under the inversion map is inner regular; i.e., μ.inv.InnerRegular.

Русский

Образ меры при обращении сохраняет внутреннюю регулярность.

LaTeX

$$$ \mu^{\mathrm{inv}}.InnerRegular $$$

Lean4

@[to_additive]
theorem innerRegular_inv_iff : μ.inv.InnerRegular ↔ μ.InnerRegular :=
  InnerRegular.map_iff (Homeomorph.inv G)

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

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

Разделы

Аффилиация

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