prehaar_self

Mathlib.MeasureTheory.Measure.Haar.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.haar.prehaar_self

← MathLib Explorer

English

For any K0, U nonempty interior, prehaar(K0, U, K0.toCompacts) equals 1.

Русский

Для K0 и непустого interior U: prehaar(K0, U, K0.toCompacts) = 1.

LaTeX

$$$\text{prehaar}_{K_0}(U, K_0^{\mathrm{toCompacts}}) = 1$$$

Lean4

@[to_additive]
theorem prehaar_self {K₀ : PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) :
    prehaar (K₀ : Set G) U K₀.toCompacts = 1 :=
  div_self <| ne_of_gt <| mod_cast index_pos K₀ hU

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

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

Разделы

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

Аффилиация

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