English
There exists a nonempty intersection of Haar-related sets: haarProduct(K0) ∩ ⋂ V open neighborhoods of 1, clPrehaar(K0, V) is nonempty.
Русский
Существует непустое пересечение haarProduct(K0) и ⋂ V, где V — открытые окрестности 1, clPrehaar(K0, V).
LaTeX
$$$\bigl\{ haarProduct(K_0) \cap \,\bigcap_{V\text{ open neighbourhoods of }1} clPrehaar(K_0, V) \bigr\} \neq \emptyset$$$
Lean4
@[to_additive]
theorem nonempty_iInter_clPrehaar (K₀ : PositiveCompacts G) :
(haarProduct (K₀ : Set G) ∩ ⋂ V : OpenNhdsOf (1 : G), clPrehaar K₀ V).Nonempty :=
by
have : IsCompact (haarProduct (K₀ : Set G)) := by apply isCompact_univ_pi; intro K; apply isCompact_Icc
refine this.inter_iInter_nonempty (clPrehaar K₀) (fun s => isClosed_closure) fun t => ?_
let V₀ := ⋂ V ∈ t, (V : OpenNhdsOf (1 : G)).carrier
have h1V₀ : IsOpen V₀ := isOpen_biInter_finset <| by rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₁
have h2V₀ : (1 : G) ∈ V₀ := by simp only [V₀, mem_iInter]; rintro ⟨⟨V, hV₁⟩, hV₂⟩ _; exact hV₂
refine ⟨prehaar K₀ V₀, ?_⟩
constructor
· apply prehaar_mem_haarProduct K₀; use 1; rwa [h1V₀.interior_eq]
· simp only [mem_iInter]; rintro ⟨V, hV⟩ h2V; apply subset_closure
apply mem_image_of_mem; rw [mem_setOf_eq]
exact ⟨Subset.trans (iInter_subset _ ⟨V, hV⟩) (iInter_subset _ h2V), h1V₀, h2V₀⟩
