English
Various simplifications show nonempty intersections persist under clPrehaar and related operations.
Русский
Различные упрощения показывают, что непустые пересечения сохраняются при работе с clPrehaar и аналогичными операциями.
LaTeX
$$$\text{...}$$$
Lean4
@[to_additive is_left_invariant_addCHaar]
theorem is_left_invariant_chaar {K₀ : PositiveCompacts G} (g : G) (K : Compacts G) :
chaar K₀ (K.map _ <| continuous_mul_left g) = chaar K₀ K :=
by
let eval : (Compacts G → ℝ) → ℝ := fun f => f (K.map _ <| continuous_mul_left g) - f K
have : Continuous eval := (continuous_apply (K.map _ _)).sub (continuous_apply K)
rw [← sub_eq_zero]; change chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}
apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
unfold clPrehaar; rw [IsClosed.closure_subset_iff]
· rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩
simp only [eval, mem_singleton_iff, mem_preimage, sub_eq_zero]
apply is_left_invariant_prehaar; rw [h2U.interior_eq]; exact ⟨1, h3U⟩
· apply continuous_iff_isClosed.mp this; exact isClosed_singleton
