chaar_mem_haarProduct

Mathlib.MeasureTheory.Measure.Haar.Basic

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

← MathLib Explorer

English

For any K0, V open neighborhood of 1, chaar(K0) belongs to clPrehaar(K0) V.

Русский

Для любых K0 и V — открытое окрестность 1: chaar(K0) ∈ clPrehaar(K0, V).

LaTeX

$$$\text{chaar}(K_0) \in \text{clPrehaar}(K_0, V)$$$

Lean4

@[to_additive addCHaar_mem_addHaarProduct]
theorem chaar_mem_haarProduct (K₀ : PositiveCompacts G) : chaar K₀ ∈ haarProduct (K₀ : Set G) :=
  (Classical.choose_spec (nonempty_iInter_clPrehaar K₀)).1

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

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

Разделы

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

Аффилиация

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