English
Basic simp consequences: monotonicity of chaar with subset relations and simple comparisons of zero.
Русский
Простые следствия монотонности chaar и простых сравнений с нулём.
LaTeX
$$$\text{chaar}(K_0, K_1) \le \text{chaar}(K_0, K_2) \text{ if } K_1 \subseteq K_2$$$
Lean4
@[to_additive addCHaar_mono]
theorem chaar_mono {K₀ : PositiveCompacts G} {K₁ K₂ : Compacts G} (h : (K₁ : Set G) ⊆ K₂) : chaar K₀ K₁ ≤ chaar K₀ K₂ :=
by
let eval : (Compacts G → ℝ) → ℝ := fun f => f K₂ - f K₁
have : Continuous eval := (continuous_apply K₂).sub (continuous_apply 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_mono _ h; rw [h2U.interior_eq]; exact ⟨1, h3U⟩
· apply continuous_iff_isClosed.mp this; exact isClosed_Ici
