chaar_empty — Mathlib

English

The chaar value on the empty compact is zero: chaar(K0, ∅) = 0.

Русский

Значение chaar на пустом компактном множестве равно нулю: chaar(K0, ∅) = 0.

LaTeX

$$$\text{chaar}(K_0, \emptyset) = 0$$$

Lean4

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

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