From 397230527de2ee2e7e0f3b7a9d45b0d2ad1eca01 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Fri, 23 Sep 2022 04:37:05 +0000 Subject: [PATCH] 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 | 2 +- src/analysis/convex/strict.lean | 2 +- src/topology/basic.lean | 34 +++++++++---------- src/topology/locally_finite.lean | 2 +- src/topology/maps.lean | 2 +- .../metric_space/hausdorff_distance.lean | 2 +- src/topology/nhds_set.lean | 2 +- src/topology/sets/opens.lean | 2 +- src/topology/subset_properties.lean | 2 +- src/topology/uniform_space/basic.lean | 2 +- 10 files changed, 26 insertions(+), 26 deletions(-) diff --git a/src/analysis/calculus/extend_deriv.lean b/src/analysis/calculus/extend_deriv.lean index 73f30665aba7b..469273820c714 100644 --- a/src/analysis/calculus/extend_deriv.lean +++ b/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∥, diff --git a/src/analysis/convex/strict.lean b/src/analysis/convex/strict.lean index bd63c97e0952d..6d9659453d38e 100644 --- a/src/analysis/convex/strict.lean +++ b/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) _ }, diff --git a/src/topology/basic.lean b/src/topology/basic.lean index 8e23d770d3e54..91a2f6f769f51 100644 --- a/src/topology/basic.lean +++ b/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,7 +1082,7 @@ 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, @@ -1090,13 +1090,13 @@ begin 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 diff --git a/src/topology/locally_finite.lean b/src/topology/locally_finite.lean index 58eaf95870161..ded3c28916569 100644 --- a/src/topology/locally_finite.lean +++ b/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 diff --git a/src/topology/maps.lean b/src/topology/maps.lean index 45c4b0b3318ef..a7252ab91a5ef 100644 --- a/src/topology/maps.lean +++ b/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⟩ diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 1e59651bbb2e9..a5d2c5fda17de 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/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 α) : diff --git a/src/topology/nhds_set.lean b/src/topology/nhds_set.lean index c50a4a94bb142..d6e72c0bad38d 100644 --- a/src/topology/nhds_set.lean +++ b/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 diff --git a/src/topology/sets/opens.lean b/src/topology/sets/opens.lean index 0a8fd73565891..63e011e115239 100644 --- a/src/topology/sets/opens.lean +++ b/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 } diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index c2d43ef7b82bb..b8a1f62f23125 100644 --- a/src/topology/subset_properties.lean +++ b/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⟩ diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index b95814c22b205..696fdecd164a2 100644 --- a/src/topology/uniform_space/basic.lean +++ b/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])