chore(topology/basic): rename lemmas (#16598)

`interior_eq_iff_open` -> `interior_eq_iff_is_open`, it's dual lemma `closure_eq_iff_is_closed` renamed in #4
`subset_interior_iff_open` -> `subset_interior_iff_is_open`
`subset_interior_iff_subset_of_open` -> `is_open.subset_interior_iff`, it's dual lemma `is_closed.closure_subset_iff` renamed in #3251
`closure_inter_open` -> `is_open.closure_inter`
`closure_inter_open'` -> `is_open.closure_inter'`

src/analysis/calculus/extend_deriv.lean

@@ -58,7 +58,7 @@ begin
   { rw closure_prod_eq at this,
     intros y y_in,
     apply this ⟨x, y⟩,
-    have : B ∩ closure s ⊆ closure (B ∩ s), from closure_inter_open is_open_ball,
+    have : B ∩ closure s ⊆ closure (B ∩ s), from is_open_ball.closure_inter,
     exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩ },
   have key : ∀ p : E × E, p ∈ (B ∩ s) ×ˢ (B ∩ s) → ∥f p.2 - f p.1 - (f' p.2 - f' p.1)∥
     ≤ ε * ∥p.2 - p.1∥,

src/analysis/convex/strict.lean

@@ -144,7 +144,7 @@ variables [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [ord
 lemma strict_convex_Iic (r : β) : strict_convex 𝕜 (Iic r) :=
 begin
   rintro x (hx : x ≤ r) y (hy : y ≤ r) hxy a b ha hb hab,
-  refine (subset_interior_iff_subset_of_open is_open_Iio).2 Iio_subset_Iic_self _,
+  refine is_open_Iio.subset_interior_iff.2 Iio_subset_Iic_self _,
   rw ←convex.combo_self hab r,
   obtain rfl | hx := hx.eq_or_lt,
   { exact add_lt_add_left (smul_lt_smul_of_pos (hy.lt_of_ne hxy.symm) hb) _ },

src/topology/basic.lean

@@ -248,13 +248,13 @@ subset_sUnion_of_mem ⟨h₂, h₁⟩
 lemma is_open.interior_eq {s : set α} (h : is_open s) : interior s = s :=
 subset.antisymm interior_subset (interior_maximal (subset.refl s) h)
 
-lemma interior_eq_iff_open {s : set α} : interior s = s ↔ is_open s :=
+lemma interior_eq_iff_is_open {s : set α} : interior s = s ↔ is_open s :=
 ⟨assume h, h ▸ is_open_interior, is_open.interior_eq⟩
 
-lemma subset_interior_iff_open {s : set α} : s ⊆ interior s ↔ is_open s :=
-by simp only [interior_eq_iff_open.symm, subset.antisymm_iff, interior_subset, true_and]
+lemma subset_interior_iff_is_open {s : set α} : s ⊆ interior s ↔ is_open s :=
+by simp only [interior_eq_iff_is_open.symm, subset.antisymm_iff, interior_subset, true_and]
 
-lemma subset_interior_iff_subset_of_open {s t : set α} (h₁ : is_open s) :
+lemma is_open.subset_interior_iff {s t : set α} (h₁ : is_open s) :
   s ⊆ interior t ↔ s ⊆ t :=
 ⟨assume h, subset.trans h interior_subset, assume h₂, interior_maximal h₂ h₁⟩
 
@@ -305,7 +305,7 @@ have interior (s ∪ t) ⊆ s, from
     have u \ s ⊆ t,
       from assume x ⟨h₁, h₂⟩, or.resolve_left (hu₂ h₁) h₂,
     have u \ s ⊆ interior t,
-      by rwa subset_interior_iff_subset_of_open (is_open.sdiff hu₁ h₁),
+      by rwa (is_open.sdiff hu₁ h₁).subset_interior_iff,
     have u \ s ⊆ ∅,
       by rwa h₂ at this,
     this ⟨hx₁, hx₂⟩,
@@ -314,7 +314,7 @@ subset.antisymm
   (interior_mono $ subset_union_left _ _)
 
 lemma is_open_iff_forall_mem_open : is_open s ↔ ∀ x ∈ s, ∃ t ⊆ s, is_open t ∧ x ∈ t :=
-by rw ← subset_interior_iff_open; simp only [subset_def, mem_interior]
+by rw ← subset_interior_iff_is_open; simp only [subset_def, mem_interior]
 
 lemma interior_Inter_subset (s : ι → set α) : interior (⋂ i, s i) ⊆ ⋂ i, interior (s i) :=
 subset_Inter $ λ i, interior_mono $ Inter_subset _ _
@@ -364,9 +364,9 @@ lemma is_closed.closure_subset_iff {s t : set α} (h₁ : is_closed t) :
   closure s ⊆ t ↔ s ⊆ t :=
 ⟨subset.trans subset_closure, assume h, closure_minimal h h₁⟩
 
-lemma is_closed.mem_iff_closure_subset {α : Type*} [topological_space α] {U : set α}
-  (hU : is_closed U) {x : α} : x ∈ U ↔ closure ({x} : set α) ⊆ U :=
-(hU.closure_subset_iff.trans set.singleton_subset_iff).symm
+lemma is_closed.mem_iff_closure_subset {s : set α} (hs : is_closed s) {x : α} :
+  x ∈ s ↔ closure ({x} : set α) ⊆ s :=
+(hs.closure_subset_iff.trans set.singleton_subset_iff).symm
 
 @[mono] lemma closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t :=
 closure_minimal (subset.trans h subset_closure) is_closed_closure
@@ -959,7 +959,7 @@ lemma subset_interior_iff_nhds {s V : set α} : s ⊆ interior V ↔ ∀ x ∈ s
 show (∀ x, x ∈ s →  x ∈ _) ↔ _, by simp_rw mem_interior_iff_mem_nhds
 
 lemma is_open_iff_nhds {s : set α} : is_open s ↔ ∀a∈s, 𝓝 a ≤ 𝓟 s :=
-calc is_open s ↔ s ⊆ interior s : subset_interior_iff_open.symm
+calc is_open s ↔ s ⊆ interior s : subset_interior_iff_is_open.symm
   ... ↔ (∀a∈s, 𝓝 a ≤ 𝓟 s) : by rw [interior_eq_nhds]; refl
 
 lemma is_open_iff_mem_nhds {s : set α} : is_open s ↔ ∀a∈s, s ∈ 𝓝 a :=
@@ -973,7 +973,7 @@ theorem is_open_iff_ultrafilter {s : set α} :
   is_open s ↔ (∀ (x ∈ s) (l : ultrafilter α), ↑l ≤ 𝓝 x → s ∈ l) :=
 by simp_rw [is_open_iff_mem_nhds, ← mem_iff_ultrafilter]
 
-lemma is_open_singleton_iff_nhds_eq_pure {α : Type*} [topological_space α] (a : α) :
+lemma is_open_singleton_iff_nhds_eq_pure (a : α) :
   is_open ({a} : set α) ↔ 𝓝 a = pure a :=
 begin
   split,
@@ -1082,21 +1082,21 @@ calc is_closed s ↔ closure s ⊆ s : closure_subset_iff_is_closed.symm
 lemma is_closed_iff_nhds {s : set α} : is_closed s ↔ ∀ x, (∀ U ∈ 𝓝 x, (U ∩ s).nonempty) → x ∈ s :=
 by simp_rw [is_closed_iff_cluster_pt, cluster_pt, inf_principal_ne_bot_iff]
 
-lemma closure_inter_open {s t : set α} (h : is_open s) : s ∩ closure t ⊆ closure (s ∩ t) :=
+lemma is_open.closure_inter {s t : set α} (h : is_open s) : s ∩ closure t ⊆ closure (s ∩ t) :=
 begin
   rintro a ⟨hs, ht⟩,
   have : s ∈ 𝓝 a := is_open.mem_nhds h hs,
   rw mem_closure_iff_nhds_ne_bot at ht ⊢,
   rwa [← inf_principal, ← inf_assoc, inf_eq_left.2 (le_principal_iff.2 this)],
 end
 
-lemma closure_inter_open' {s t : set α} (h : is_open t) : closure s ∩ t ⊆ closure (s ∩ t) :=
-by simpa only [inter_comm] using closure_inter_open h
+lemma is_open.closure_inter' {s t : set α} (h : is_open t) : closure s ∩ t ⊆ closure (s ∩ t) :=
+by simpa only [inter_comm] using h.closure_inter
 
 lemma dense.open_subset_closure_inter {s t : set α} (hs : dense s) (ht : is_open t) :
   t ⊆ closure (t ∩ s) :=
 calc t = t ∩ closure s   : by rw [hs.closure_eq, inter_univ]
-   ... ⊆ closure (t ∩ s) : closure_inter_open ht
+   ... ⊆ closure (t ∩ s) : ht.closure_inter
 
 lemma mem_closure_of_mem_closure_union {s₁ s₂ : set α} {x : α} (h : x ∈ closure (s₁ ∪ s₂))
   (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ :=
@@ -1112,7 +1112,7 @@ end
 /-- The intersection of an open dense set with a dense set is a dense set. -/
 lemma dense.inter_of_open_left {s t : set α} (hs : dense s) (ht : dense t) (hso : is_open s) :
   dense (s ∩ t) :=
-λ x, (closure_minimal (closure_inter_open hso) is_closed_closure) $
+λ x, (closure_minimal hso.closure_inter is_closed_closure) $
   by simp [hs.closure_eq, ht.closure_eq]
 
 /-- The intersection of a dense set with an open dense set is a dense set. -/
@@ -1127,7 +1127,7 @@ let ⟨U, hsub, ho, hx⟩ := mem_nhds_iff.1 ht in
 
 lemma closure_diff {s t : set α} : closure s \ closure t ⊆ closure (s \ t) :=
 calc closure s \ closure t = (closure t)ᶜ ∩ closure s : by simp only [diff_eq, inter_comm]
-  ... ⊆ closure ((closure t)ᶜ ∩ s) : closure_inter_open $ is_open_compl_iff.mpr $ is_closed_closure
+  ... ⊆ closure ((closure t)ᶜ ∩ s) : (is_open_compl_iff.mpr $ is_closed_closure).closure_inter
   ... = closure (s \ closure t) : by simp only [diff_eq, inter_comm]
   ... ⊆ closure (s \ t) : closure_mono $ diff_subset_diff (subset.refl s) subset_closure
 

src/topology/locally_finite.lean

@@ -78,7 +78,7 @@ begin
   intro x,
   rcases hf x with ⟨s, hsx, hsf⟩,
   refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset $ λ i hi, _⟩,
-  exact (hi.mono (closure_inter_open' is_open_interior)).of_closure.mono
+  exact (hi.mono is_open_interior.closure_inter').of_closure.mono
     (inter_subset_inter_right _ interior_subset)
 end
 

src/topology/maps.lean

@@ -365,7 +365,7 @@ lemma is_open_map_iff_nhds_le [topological_space α] [topological_space β] {f :
 
 lemma is_open_map_iff_interior [topological_space α] [topological_space β] {f : α → β} :
   is_open_map f ↔ ∀ s, f '' (interior s) ⊆ interior (f '' s) :=
-⟨is_open_map.image_interior_subset, λ hs u hu, subset_interior_iff_open.mp $
+⟨is_open_map.image_interior_subset, λ hs u hu, subset_interior_iff_is_open.mp $
   calc f '' u = f '' (interior u) : by rw hu.interior_eq
           ... ⊆ interior (f '' u) : hs u⟩
 

src/topology/metric_space/hausdorff_distance.lean

@@ -990,7 +990,7 @@ end
 
 lemma thickening_subset_interior_cthickening (δ : ℝ) (E : set α) :
   thickening δ E ⊆ interior (cthickening δ E) :=
-(subset_interior_iff_open.mpr (is_open_thickening)).trans
+(subset_interior_iff_is_open.mpr (is_open_thickening)).trans
   (interior_mono (thickening_subset_cthickening δ E))
 
 lemma closure_thickening_subset_cthickening (δ : ℝ) (E : set α) :

src/topology/nhds_set.lean

@@ -54,7 +54,7 @@ lemma has_basis_nhds_set (s : set α) : (𝓝ˢ s).has_basis (λ U, is_open U 
 ⟨λ t, by simp [mem_nhds_set_iff_exists, and_assoc]⟩
 
 lemma is_open.mem_nhds_set (hU : is_open s) : s ∈ 𝓝ˢ t ↔ t ⊆ s :=
-by rw [← subset_interior_iff_mem_nhds_set, interior_eq_iff_open.mpr hU]
+by rw [← subset_interior_iff_mem_nhds_set, interior_eq_iff_is_open.mpr hU]
 
 lemma principal_le_nhds_set : 𝓟 s ≤ 𝓝ˢ s :=
 λ s hs, (subset_interior_iff_mem_nhds_set.mpr hs).trans interior_subset

src/topology/sets/opens.lean

@@ -69,7 +69,7 @@ open order_dual (of_dual to_dual)
 
 /-- The galois coinsertion between sets and opens. -/
 def gi : galois_coinsertion subtype.val (@interior α _) :=
-{ choice := λ s hs, ⟨s, interior_eq_iff_open.mp $ le_antisymm interior_subset hs⟩,
+{ choice := λ s hs, ⟨s, interior_eq_iff_is_open.mp $ le_antisymm interior_subset hs⟩,
   gc := gc,
   u_l_le := λ _, interior_subset,
   choice_eq := λ s hs, le_antisymm hs interior_subset }

src/topology/subset_properties.lean

@@ -1390,7 +1390,7 @@ 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],
+  rw [is_clopen, ← closure_eq_iff_is_closed, ← interior_eq_iff_is_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⟩

src/topology/uniform_space/basic.lean

@@ -848,7 +848,7 @@ le_antisymm
     let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs in
     have s ⊆ interior d, from
       calc s ⊆ t : hst
-       ... ⊆ interior d : (subset_interior_iff_subset_of_open ht).mpr $
+       ... ⊆ interior d : ht.subset_interior_iff.mpr $
         λ x (hx : x ∈ t), let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx in hs_comp ⟨x, h₁, y, h₂, h₃⟩,
     have interior d ∈ 𝓤 α, by filter_upwards [hs] using this,
     by simp [this])