no goals
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
⊢ IsCoveringMap f ↔ IsCoveringMapOn f Set.univ
simp only [IsCoveringMap, IsCoveringMapOn, Set.mem_univ, forall_true_left]