prehaar_mem_haarProduct — Mathlib

English

The quantity chaar(K0) lies in the Haar product HaarProduct(K0).

Русский

Чaar(K0) принадлежит HaarProduct(K0).

LaTeX

$$$\text{chaar}_{K_0} \in \text{haarProduct}(K_0)$$$

Lean4

@[to_additive]
theorem prehaar_mem_haarProduct (K₀ : PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) :
    prehaar (K₀ : Set G) U ∈ haarProduct (K₀ : Set G) := by rintro ⟨K, hK⟩ _; rw [mem_Icc];
  exact ⟨prehaar_nonneg K₀ _, prehaar_le_index K₀ _ hU⟩

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