α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ (t_1 : TopologicalSpace β),
    t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace} → Continuous f
α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ Continuous f
rw [continuous_sInf_rng]
case intro.intro
α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
t' : GroupTopology β
ht' : t' ∈ {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
⊢ Continuous f
α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ (t_1 : TopologicalSpace β),
    t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace} → Continuous f
rintro _ ⟨t', ht', rfl⟩
no goals
case intro.intro
α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
t' : GroupTopology β
ht' : t' ∈ {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
⊢ Continuous f
exact continuous_iff_coinduced_le.2 ht'