chaar_self — Mathlib

English

If K1 ⊆ K2 then chaar(K0, K1) ≤ chaar(K0, K2).

Русский

Если K1 ⊆ K2, то chaar(K0, K1) ≤ chaar(K0, K2).

LaTeX

$$$\text{chaar}(K_0, K_1) \le \text{chaar}(K_0, K_2)\quad(K_1 \subseteq K_2)$$$

Lean4

@[to_additive addCHaar_self]
theorem chaar_self (K₀ : PositiveCompacts G) : chaar K₀ K₀.toCompacts = 1 :=
  by
  let eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts
  have : Continuous eval := continuous_apply _
  change chaar K₀ ∈ eval ⁻¹' {(1 : ℝ)}
  apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
  unfold clPrehaar; rw [IsClosed.closure_subset_iff]
  · rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩; apply prehaar_self
    rw [h2U.interior_eq]; exact ⟨1, h3U⟩
  · apply continuous_iff_isClosed.mp this; exact isClosed_singleton

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