feat(topology): add lemmas about frontier (#13054)

src/topology/basic.lean

@@ -529,6 +529,12 @@ by rw [closure_compl, frontier, diff_eq]
 
 lemma frontier_subset_closure {s : set α} : frontier s ⊆ closure s := diff_subset _ _
 
+lemma frontier_closure_subset {s : set α} : frontier (closure s) ⊆ frontier s :=
+diff_subset_diff closure_closure.subset $ interior_mono subset_closure
+
+lemma frontier_interior_subset {s : set α} : frontier (interior s) ⊆ frontier s :=
+diff_subset_diff (closure_mono interior_subset) interior_interior.symm.subset
+
 /-- The complement of a set has the same frontier as the original set. -/
 @[simp] lemma frontier_compl (s : set α) : frontier sᶜ = frontier s :=
 by simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]

src/topology/connected.lean

@@ -725,6 +725,14 @@ lemma eq_univ_of_nonempty_clopen [preconnected_space α] {s : set α}
   (h : s.nonempty) (h' : is_clopen s) : s = univ :=
 by { rw is_clopen_iff at h', exact h'.resolve_left h.ne_empty }
 
+lemma frontier_eq_empty_iff [preconnected_space α] {s : set α} :
+  frontier s = ∅ ↔ s = ∅ ∨ s = univ :=
+is_clopen_iff_frontier_eq_empty.symm.trans is_clopen_iff
+
+lemma nonempty_frontier_iff [preconnected_space α] {s : set α} :
+  (frontier s).nonempty ↔ s.nonempty ∧ s ≠ univ :=
+by simp only [← ne_empty_iff_nonempty, ne.def, frontier_eq_empty_iff, not_or_distrib]
+
 lemma subtype.preconnected_space {s : set α} (h : is_preconnected s) :
   preconnected_space s :=
 { is_preconnected_univ := by rwa [← embedding_subtype_coe.to_inducing.is_preconnected_image,

src/topology/subset_properties.lean

@@ -1287,6 +1287,16 @@ is_open s ∧ is_closed s
 protected lemma is_clopen.is_open (hs : is_clopen s) : is_open s := hs.1
 protected lemma is_clopen.is_closed (hs : is_clopen s) : is_closed s := hs.2
 
+lemma is_clopen_iff_frontier_eq_empty {s : set α} : is_clopen s ↔ frontier s = ∅ :=
+begin
+  rw [is_clopen, ← closure_eq_iff_is_closed, ← interior_eq_iff_open, frontier, diff_eq_empty],
+  refine ⟨λ h, (h.2.trans h.1.symm).subset, λ h, _⟩,
+  exact ⟨interior_subset.antisymm (subset_closure.trans h),
+    (h.trans interior_subset).antisymm subset_closure⟩
+end
+
+alias is_clopen_iff_frontier_eq_empty ↔ is_clopen.frontier_eq _
+
 theorem is_clopen.union {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∪ t) :=
 ⟨hs.1.union ht.1, hs.2.union ht.2⟩