English
For K1, K2 compact, the chaar of their supremum is at most the sum of their chaars.
Русский
Для K1,K2 компактных: chaar(K0, sup(K1,K2)) ≤ chaar(K0, K1) + chaar(K0, K2).
LaTeX
$$$\text{haar}(K_0, \mathrm{sup}(K_1, K_2)) \le \text{haar}(K_0, K_1) + \text{haar}(K_0, K_2)$$$
Lean4
@[to_additive addCHaar_sup_le]
theorem chaar_sup_le {K₀ : PositiveCompacts G} (K₁ K₂ : Compacts G) : chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂ :=
by
let eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
have : Continuous eval := by exact ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ K₂))
rw [← sub_nonneg]; change chaar K₀ ∈ eval ⁻¹' Ici (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_preimage, mem_Ici, sub_nonneg]
apply prehaar_sup_le; rw [h2U.interior_eq]; exact ⟨1, h3U⟩
· apply continuous_iff_isClosed.mp this; exact isClosed_Ici
