α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x : G
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
⊢ LocallyCompactSpace G
refine' locally_compact_of_compact_nhds fun x => _
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x : G
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
obtain ⟨y, hy⟩ := K.interior_nonempty
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
let F := Homeomorph.mulLeft (x * y⁻¹)
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑F '' ↑K ∈ 𝓝 x
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
refine' ⟨F '' K, _, K.isCompact.image F.continuous⟩
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑F '' ↑K ∈ 𝓝 x
suffices F.symm ⁻¹' K ∈ 𝓝 x by
  convert this using 1
  apply Equiv.image_eq_preimage
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
apply ContinuousAt.preimage_mem_nhds F.symm.continuous.continuousAt
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
have : F.symm x = y := by simp only [Homeomorph.mulLeft_symm, mul_inv_rev,
    inv_inv, Homeomorph.coe_mulLeft, inv_mul_cancel_right]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 y
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
rw [this]
no goals
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 y
exact mem_interior_iff_mem_nhds.1 hy
case h.e'_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
⊢ ↑F '' ↑K = ↑(Homeomorph.symm F) ⁻¹' ↑K
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
⊢ ↑F '' ↑K ∈ 𝓝 x
convert this using 1
no goals
case h.e'_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
⊢ ↑F '' ↑K = ↑(Homeomorph.symm F) ⁻¹' ↑K
apply Equiv.image_eq_preimage
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑(Homeomorph.symm F) x = y
simp only [Homeomorph.mulLeft_symm, mul_inv_rev,
inv_inv, Homeomorph.coe_mulLeft, inv_mul_cancel_right]