α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ ∀ (a : G), IsOpen {a}
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ DiscreteTopology G
rw [← singletons_open_iff_discrete]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ IsOpen {g}
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ ∀ (a : G), IsOpen {a}
intro g
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ IsOpen {g}
suffices {g} = (fun x : G => g⁻¹ * x) ⁻¹' {1} by
  rw [this]
  exact (continuous_mul_left g⁻¹).isOpen_preimage _ h
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
simp only [mul_one, Set.preimage_mul_left_singleton, eq_self_iff_true, inv_inv,
  Set.singleton_eq_singleton_iff]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen ((fun x => g⁻¹ * x) ⁻¹' {1})
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen {g}
rw [this]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen ((fun x => g⁻¹ * x) ⁻¹' {1})
exact (continuous_mul_left g⁻¹).isOpen_preimage _ h