G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
⊢ chaar K₀ ⊥ = 0
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
⊢ chaar K₀ ⊥ = 0
let eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ chaar K₀ ⊥ = 0
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
⊢ chaar K₀ ⊥ = 0
have : Continuous eval := continuous_apply ⊥
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ chaar K₀ ∈ eval ⁻¹' {0}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ chaar K₀ ⊥ = 0
show chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ chaar K₀ ∈ eval ⁻¹' {0}
apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}
unfold clPrehaar
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {0})
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}
rw [IsClosed.closure_subset_iff]
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
U : Set G
left✝ : U ∈ {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}
⊢ prehaar (↑K₀) U ∈ eval ⁻¹' {0}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}
rintro _ ⟨U, _, rfl⟩
no goals
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
U : Set G
left✝ : U ∈ {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}
⊢ prehaar (↑K₀) U ∈ eval ⁻¹' {0}
apply prehaar_empty
case a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ IsClosed {0}
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ IsClosed (eval ⁻¹' {0})
apply continuous_iff_isClosed.mp this
no goals
case a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f ⊥
this : Continuous eval
⊢ IsClosed {0}
exact isClosed_singleton