chore(topology): rename interior_eq_of_open (#3614)

This allows to use dot notation and is more consistent with
its closed twin is_closed.closure_eq

Author: PatrickMassot

src/analysis/normed_space/basic.lean

@@ -827,7 +827,7 @@ end
 theorem frontier_ball [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r) :
   frontier (ball x r) = sphere x r :=
 begin
-  rw [frontier, closure_ball x hr, interior_eq_of_open is_open_ball],
+  rw [frontier, closure_ball x hr, is_open_ball.interior_eq],
   ext x, exact (@eq_iff_le_not_lt ℝ _ _ _).symm
 end
 

src/geometry/manifold/charted_space.lean

@@ -221,15 +221,15 @@ def id_groupoid (H : Type u) [topological_space H] : structure_groupoid H :=
       rcases h with ⟨x, hx⟩,
       rcases he x hx with ⟨s, open_s, xs, hs⟩,
       have x's : x ∈ (e.restr s).source,
-      { rw [restr_source, interior_eq_of_open open_s],
+      { rw [restr_source, open_s.interior_eq],
         exact ⟨hx, xs⟩ },
       cases hs,
       { replace hs : local_homeomorph.restr e s = local_homeomorph.refl H,
           by simpa only using hs,
         have : (e.restr s).source = univ, by { rw hs, simp },
         change (e.to_local_equiv).source ∩ interior s = univ at this,
         have : univ ⊆ interior s, by { rw ← this, exact inter_subset_right _ _ },
-        have : s = univ, by rwa [interior_eq_of_open open_s, univ_subset_iff] at this,
+        have : s = univ, by rwa [open_s.interior_eq, univ_subset_iff] at this,
         simpa only [this, restr_univ] using hs },
       { exfalso,
         rw mem_set_of_eq at hs,
@@ -298,14 +298,14 @@ def pregroupoid.groupoid (PG : pregroupoid H) : structure_groupoid H :=
       rcases he x xu with ⟨s, s_open, xs, hs⟩,
       refine ⟨s, s_open, xs, _⟩,
       convert hs.1,
-      exact (interior_eq_of_open s_open).symm },
+      exact s_open.interior_eq.symm },
     { apply PG.locality e.open_target (λx xu, _),
       rcases he (e.symm x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩,
       refine ⟨e.target ∩ e.symm ⁻¹' s, _, ⟨xu, xs⟩, _⟩,
       { exact continuous_on.preimage_open_of_open e.continuous_inv_fun e.open_target s_open },
       { rw [← inter_assoc, inter_self],
         convert hs.2,
-        exact (interior_eq_of_open s_open).symm } },
+        exact s_open.interior_eq.symm } },
   end,
   eq_on_source' := λe e' he ee', begin
     split,
@@ -393,7 +393,7 @@ def id_restr_groupoid : structure_groupoid H :=
     rcases h x hx with ⟨s, hs, hxs, s', hs', hes'⟩,
     have hes : x ∈ (e.restr s).source,
     { rw e.restr_source, refine ⟨hx, _⟩,
-      rw interior_eq_of_open hs, exact hxs },
+      rw hs.interior_eq, exact hxs },
     simpa only with mfld_simps using local_homeomorph.eq_on_source.eq_on hes' hes,
   end,
   eq_on_source' := begin
@@ -412,7 +412,7 @@ instance closed_under_restriction_id_restr_groupoid :
     rintros e ⟨s', hs', he⟩ s hs,
     use [s' ∩ s, is_open_inter hs' hs],
     refine setoid.trans (local_homeomorph.eq_on_source.restr he s) _,
-    exact ⟨by simp only [interior_eq_of_open hs] with mfld_simps, by simp only with mfld_simps⟩,
+    exact ⟨by simp only [hs.interior_eq] with mfld_simps, by simp only with mfld_simps⟩,
   end ⟩
 
 /-- A groupoid is closed under restriction if and only if it contains the trivial restriction-closed
@@ -426,7 +426,7 @@ begin
     rintros e ⟨s, hs, hes⟩,
     refine G.eq_on_source _ hes,
     convert closed_under_restriction' G.id_mem hs,
-    rw interior_eq_of_open hs,
+    rw hs.interior_eq,
     simp only with mfld_simps },
   { intros h,
     split,

src/geometry/manifold/local_invariant_properties.lean

@@ -515,8 +515,8 @@ lemma is_local_structomorph_within_at_local_invariant_prop [closed_under_restric
       refine ⟨e.restr (interior u), _, _, _⟩,
       { exact closed_under_restriction' heG (is_open_interior) },
       { have : s ∩ u ∩ e.source = s ∩ (e.source ∩ u) := by mfld_set_tac,
-        simpa only [this, interior_interior, interior_eq_of_open hu] with mfld_simps using hef },
-      { simp only [*, interior_interior, interior_eq_of_open hu] with mfld_simps } }
+        simpa only [this, interior_interior, hu.interior_eq] with mfld_simps using hef },
+      { simp only [*, interior_interior, hu.interior_eq] with mfld_simps } }
   end,
   right_invariance := begin
     intros s x f e' he'G he'x h hx,

src/topology/algebra/ordered.lean

@@ -248,13 +248,13 @@ lemma is_open_Ioo : is_open (Ioo a b) :=
 is_open_inter is_open_Ioi is_open_Iio
 
 @[simp] lemma interior_Ioi : interior (Ioi a) = Ioi a :=
-interior_eq_of_open is_open_Ioi
+is_open_Ioi.interior_eq
 
 @[simp] lemma interior_Iio : interior (Iio a) = Iio a :=
-interior_eq_of_open is_open_Iio
+is_open_Iio.interior_eq
 
 @[simp] lemma interior_Ioo : interior (Ioo a b) = Ioo a b :=
-interior_eq_of_open is_open_Ioo
+is_open_Ioo.interior_eq
 
 /-- Intermediate value theorem for two functions: if `f` and `g` are two continuous functions
 on a preconnected space and `f a ≤ g a` and `g b ≤ f b`, then for some `x` we have `f x = g x`. -/

src/topology/basic.lean

@@ -216,11 +216,11 @@ sUnion_subset $ assume t ⟨h₁, h₂⟩, h₂
 lemma interior_maximal {s t : set α} (h₁ : t ⊆ s) (h₂ : is_open t) : t ⊆ interior s :=
 subset_sUnion_of_mem ⟨h₂, h₁⟩
 
-lemma interior_eq_of_open {s : set α} (h : is_open s) : interior s = s :=
+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 :=
-⟨assume h, h ▸ is_open_interior, interior_eq_of_open⟩
+⟨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]
@@ -233,13 +233,13 @@ lemma interior_mono {s t : set α} (h : s ⊆ t) : interior s ⊆ interior t :=
 interior_maximal (subset.trans interior_subset h) is_open_interior
 
 @[simp] lemma interior_empty : interior (∅ : set α) = ∅ :=
-interior_eq_of_open is_open_empty
+is_open_empty.interior_eq
 
 @[simp] lemma interior_univ : interior (univ : set α) = univ :=
-interior_eq_of_open is_open_univ
+is_open_univ.interior_eq
 
 @[simp] lemma interior_interior {s : set α} : interior (interior s) = interior s :=
-interior_eq_of_open is_open_interior
+is_open_interior.interior_eq
 
 @[simp] lemma interior_inter {s t : set α} : interior (s ∩ t) = interior s ∩ interior t :=
 subset.antisymm
@@ -405,7 +405,7 @@ lemma is_closed.frontier_eq {s : set α} (hs : is_closed s) : frontier s = s \ i
 by rw [frontier, hs.closure_eq]
 
 lemma is_open.frontier_eq {s : set α} (hs : is_open s) : frontier s = closure s \ s :=
-by rw [frontier, interior_eq_of_open hs]
+by rw [frontier, hs.interior_eq]
 
 /-- The frontier of a set is closed. -/
 lemma is_closed_frontier {s : set α} : is_closed (frontier s) :=

src/topology/continuous_on.lean

@@ -591,7 +591,7 @@ lemma continuous_on.preimage_interior_subset_interior_preimage {f : α → β} {
 calc s ∩ f ⁻¹' (interior t) ⊆ interior (s ∩ f ⁻¹' t) :
   interior_maximal (inter_subset_inter (subset.refl _) (preimage_mono interior_subset))
     (hf.preimage_open_of_open hs is_open_interior)
-... = s ∩ interior (f ⁻¹' t) : by rw [interior_inter, interior_eq_of_open hs]
+... = s ∩ interior (f ⁻¹' t) : by rw [interior_inter, hs.interior_eq]
 
 lemma continuous_on_of_locally_continuous_on {f : α → β} {s : set α}
   (h : ∀x∈s, ∃t, is_open t ∧ x ∈ t ∧ continuous_on f (s ∩ t)) : continuous_on f s :=

src/topology/local_homeomorph.lean

@@ -201,15 +201,15 @@ begin
         exact e.continuous_on_symm.preimage_interior_subset_interior_preimage e.open_target
       end
     ... = e.source ∩ e ⁻¹' (interior (e.target ∩ e.symm ⁻¹' (e ⁻¹' s))) :
-      by rw [interior_inter, interior_eq_of_open e.open_target]
+      by rw [interior_inter, e.open_target.interior_eq]
     ... = e.source ∩ e ⁻¹' (interior (e.target ∩ s)) :
       begin
         have := e.to_local_equiv.target_inter_inv_preimage_preimage,
         simp only [coe_coe_symm, coe_coe] at this,
         rw this
       end
     ... = e.source ∩ e ⁻¹' e.target ∩ e ⁻¹' (interior s) :
-      by rw [interior_inter, preimage_inter, interior_eq_of_open e.open_target, inter_assoc]
+      by rw [interior_inter, preimage_inter, e.open_target.interior_eq, inter_assoc]
     ... = e.source ∩ e ⁻¹' (interior s) : by mfld_set_tac }
 end
 
@@ -269,11 +269,11 @@ lemma restr_target (s : set α) :
   (e.restr s).target = e.target ∩ e.symm ⁻¹' (interior s) := rfl
 
 lemma restr_source' (s : set α) (hs : is_open s) : (e.restr s).source = e.source ∩ s :=
-by rw [e.restr_source, interior_eq_of_open hs]
+by rw [e.restr_source, hs.interior_eq]
 
 lemma restr_to_local_equiv' (s : set α) (hs : is_open s):
   (e.restr s).to_local_equiv = e.to_local_equiv.restr s :=
-by rw [e.restr_to_local_equiv, interior_eq_of_open hs]
+by rw [e.restr_to_local_equiv, hs.interior_eq]
 
 lemma restr_eq_of_source_subset {e : local_homeomorph α β} {s : set α} (h : e.source ⊆ s) :
   e.restr s = e :=
@@ -282,7 +282,7 @@ begin
   rw restr_to_local_equiv,
   apply local_equiv.restr_eq_of_source_subset,
   have := interior_mono h,
-  rwa interior_eq_of_open (e.open_source) at this
+  rwa e.open_source.interior_eq at this
 end
 
 @[simp, mfld_simps] lemma restr_univ {e : local_homeomorph α β} : e.restr univ = e :=
@@ -291,7 +291,7 @@ restr_eq_of_source_subset (subset_univ _)
 lemma restr_source_inter (s : set α) : e.restr (e.source ∩ s) = e.restr s :=
 begin
   refine local_homeomorph.ext _ _ (λx, rfl) (λx, rfl) _,
-  simp [interior_eq_of_open e.open_source],
+  simp [e.open_source.interior_eq],
   rw [← inter_assoc, inter_self]
 end
 
@@ -400,7 +400,7 @@ eq_of_local_equiv_eq $ local_equiv.refl_trans e.to_local_equiv
 lemma trans_of_set {s : set β} (hs : is_open s) :
   e.trans (of_set s hs) = e.restr (e ⁻¹' s) :=
 local_homeomorph.ext _ _ (λx, rfl) (λx, rfl) $
-  by simp [local_equiv.trans_source, (e.preimage_interior _).symm, interior_eq_of_open hs]
+  by simp [local_equiv.trans_source, (e.preimage_interior _).symm, hs.interior_eq]
 
 lemma trans_of_set' {s : set β} (hs : is_open s) :
   e.trans (of_set s hs) = e.restr (e.source ∩ e ⁻¹' s) :=
@@ -409,7 +409,7 @@ by rw [trans_of_set, restr_source_inter]
 lemma of_set_trans {s : set α} (hs : is_open s) :
   (of_set s hs).trans e = e.restr s :=
 local_homeomorph.ext _ _ (λx, rfl) (λx, rfl) $
-  by simp [local_equiv.trans_source, interior_eq_of_open hs, inter_comm]
+  by simp [local_equiv.trans_source, hs.interior_eq, inter_comm]
 
 lemma of_set_trans' {s : set α} (hs : is_open s) :
   (of_set s hs).trans e = e.restr (e.source ∩ s) :=
@@ -420,7 +420,7 @@ by rw [of_set_trans, restr_source_inter]
   (of_set s hs).trans (of_set s' hs') = of_set (s ∩ s') (is_open_inter hs hs')  :=
 begin
   rw (of_set s hs).trans_of_set hs',
-  ext; simp [interior_eq_of_open hs']
+  ext; simp [hs'.interior_eq]
 end
 
 lemma restr_trans (s : set α) :

src/topology/opens.lean

@@ -77,9 +77,7 @@ complete_lattice.copy
 begin
   funext,
   apply subtype.ext_iff_val.mpr,
-  symmetry,
-  apply interior_eq_of_open,
-  exact (is_open_inter U.2 V.2),
+  exact (is_open_inter U.2 V.2).interior_eq.symm,
 end
 /- Sup -/ (λ Us, ⟨⋃₀ (coe '' Us), is_open_sUnion $ λ U hU,
 by { rcases hU with ⟨⟨V, hV⟩, h, h'⟩, dsimp at h', subst h', exact hV}⟩)

src/topology/subset_properties.lean

@@ -577,7 +577,7 @@ lemma exists_compact_subset [locally_compact_space α] {x : α} {U : set α}
 begin
   rcases locally_compact_space.local_compact_nhds x U _ with ⟨K, h1K, h2K, h3K⟩,
   { refine ⟨K, h3K, _, h2K⟩, rwa [ mem_interior_iff_mem_nhds] },
-  rwa [← mem_interior_iff_mem_nhds, interior_eq_of_open hU]
+  rwa [← mem_interior_iff_mem_nhds, hU.interior_eq]
 end
 
 end compact