feat(analysis/topology, data/set): some zerology (#295)

analysis/topology/topological_space.lean

@@ -225,6 +225,15 @@ closure_minimal (subset.trans h subset_closure) is_closed_closure
 @[simp] lemma closure_empty : closure (∅ : set α) = ∅ :=
 closure_eq_of_is_closed is_closed_empty
 
+lemma closure_empty_iff (s : set α) : closure s = ∅ ↔ s = ∅ :=
+begin
+  split ; intro h,
+  { rw set.eq_empty_iff_forall_not_mem,
+    intros x H,
+    simpa [h] using subset_closure H },
+  { exact (eq.symm h) ▸ closure_empty },
+end
+
 @[simp] lemma closure_univ : closure (univ : set α) = univ :=
 closure_eq_of_is_closed is_closed_univ
 

data/set/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Leonardo de Moura
 -/
-import tactic.ext tactic.finish data.subtype
+import tactic.ext tactic.finish data.subtype tactic.interactive
 open function
 
 namespace set
@@ -175,6 +175,16 @@ by simp [ext_iff]
 
 theorem eq_univ_of_forall {s : set α} : (∀ x, x ∈ s) → s = univ := eq_univ_iff_forall.2
 
+lemma nonempty_iff_univ_ne_empty {α : Type*} : nonempty α ↔ (univ : set α) ≠ ∅ :=
+begin
+  split,
+  { rintro ⟨a⟩ H2,
+    show a ∈ (∅ : set α), by rw ←H2 ; trivial },
+  { intro H,
+    cases exists_mem_of_ne_empty H with a _,
+    exact ⟨a⟩ }
+end
+
 /- union -/
 
 theorem union_def {s₁ s₂ : set α} : s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂} := rfl
@@ -922,6 +932,13 @@ subset.antisymm
 theorem range_subset_iff {ι : Type*} {f : ι → β} {s : set β} : range f ⊆ s ↔ ∀ y, f y ∈ s :=
 forall_range_iff
 
+lemma nonempty_of_nonempty_range {α : Type*} {β : Type*} {f : α → β} (H : ¬range f = ∅) : nonempty α :=
+begin
+  cases exists_mem_of_ne_empty H with x h,
+  cases mem_range.1 h with y _,
+  exact ⟨y⟩
+end
+
 theorem image_preimage_eq_inter_range {f : α → β} {t : set β} :
   f '' preimage f t = t ∩ range f :=
 set.ext $ assume x, ⟨assume ⟨x, hx, heq⟩, heq ▸ ⟨hx, mem_range_self _⟩,