Supplementary results for continuous group homomorphisms

theorem MonoidHom.continuous_iff {G : Type u_1} {H : Type u_2} [Group G] [Monoid H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousMul G] [ContinuousMul H] (f : G →* H) : Continuous ⇑f ↔ ∀ (s : Set H), 1 ∈ s → IsOpen s → ∃ (t : Set G), 1 ∈ t ∧ IsOpen t ∧ t ⊆ ⇑f ⁻¹' s

theorem AddMonoidHom.continuous_iff {G : Type u_1} {H : Type u_2} [AddGroup G] [AddMonoid H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousAdd G] [ContinuousAdd H] (f : G →+ H) : Continuous ⇑f ↔ ∀ (s : Set H), 0 ∈ s → IsOpen s → ∃ (t : Set G), 0 ∈ t ∧ IsOpen t ∧ t ⊆ ⇑f ⁻¹' s