From 3685146a9f9723f8ee52ce16a705fe721148b7be Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 17 Dec 2020 13:27:36 +0000 Subject: [PATCH] chore(topology/algebra/ordered): deduplicate (#5399) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Drop `mem_nhds_unbounded` in favor of `mem_nhds_iff_exists_Ioo_subset'`. * Use `(h : ∃ l, l < a)` instead of `{l} (hl : l < a)` in `mem_nhds_iff_exists_Ioo_subset'`. This way we can `apply` the theorem without generating non-`Prop` goals and we can get the arguments directly from `no_bot` / `no_top`. * add `nhds_basis_Ioo'` and `nhds_basis_Ioo`. --- src/order/complete_lattice.lean | 4 +++ src/topology/algebra/ordered.lean | 50 ++++++++++--------------------- src/topology/instances/real.lean | 6 ++-- 3 files changed, 22 insertions(+), 38 deletions(-) diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean index eeab9b77a6025..375e0e7ac09a5 100644 --- a/src/order/complete_lattice.lean +++ b/src/order/complete_lattice.lean @@ -636,6 +636,10 @@ lemma binfi_inf {p : ι → Prop} {f : Π i (hi : p i), α} {a : α} (h : ∃ i, by haveI : nonempty {i // p i} := (let ⟨i, hi⟩ := h in ⟨⟨i, hi⟩⟩); rw [infi_subtype', infi_subtype', infi_inf] +lemma inf_binfi {p : ι → Prop} {f : Π i (hi : p i), α} {a : α} (h : ∃ i, p i) : + a ⊓ (⨅i (h : p i), f i h) = (⨅ i (h : p i), a ⊓ f i h) := +by simpa only [inf_comm] using binfi_inf h + theorem supr_sup_eq {f g : β → α} : (⨆ x, f x ⊔ g x) = (⨆ x, f x) ⊔ (⨆ x, g x) := @infi_inf_eq (order_dual α) β _ _ _ diff --git a/src/topology/algebra/ordered.lean b/src/topology/algebra/ordered.lean index 957dcae4fc945..c895751b4d9ee 100644 --- a/src/topology/algebra/ordered.lean +++ b/src/topology/algebra/ordered.lean @@ -674,16 +674,8 @@ tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh lemma nhds_order_unbounded {a : α} (hu : ∃u, a < u) (hl : ∃l, l < a) : 𝓝 a = (⨅l (h₂ : l < a) u (h₂ : a < u), 𝓟 (Ioo l u)) := -calc 𝓝 a = (⨅ba, 𝓟 {c | c < b}) : nhds_eq_order a - ... = (⨅ba, 𝓟 {c | c < b})) : binfi_inf hl - ... = (⨅la, 𝓟 {c | c < u} ⊓ 𝓟 {c | l < c})) : - begin - congr, funext x, - congr, funext hx, - rw [inf_comm], - apply binfi_inf hu - end - ... = _ : by simp [inter_comm]; refl +have ∃ u, u ∈ Ioi a, from hu, have ∃ l, l ∈ Iio a, from hl, +by { simp only [nhds_eq_order, inf_binfi, binfi_inf, *, inf_principal, Ioi_inter_Iio], refl } lemma tendsto_order_unbounded {f : β → α} {a : α} {x : filter β} (hu : ∃u, a < u) (hl : ∃l, l < a) (h : ∀l u, l < a → a < u → ∀ᶠ b in x, l < f b ∧ f b < u) : @@ -857,25 +849,6 @@ lemma exists_Ico_subset_of_mem_nhds {a : α} {s : set α} (hs : s ∈ 𝓝 a) (h ∃ u (_ : a < u), Ico a u ⊆ s := let ⟨l', hl'⟩ := h in let ⟨l, hl⟩ := exists_Ico_subset_of_mem_nhds' hs hl' in ⟨l, hl.fst.1, hl.snd⟩ -lemma mem_nhds_unbounded {a : α} {s : set α} (hu : ∃u, a < u) (hl : ∃l, l < a) : - s ∈ 𝓝 a ↔ (∃l u, l < a ∧ a < u ∧ ∀b, l < b → b < u → b ∈ s) := -let ⟨l, hl'⟩ := hl, ⟨u, hu'⟩ := hu in -have 𝓝 a = (⨅p : {l // l < a} × {u // a < u}, 𝓟 (Ioo p.1.val p.2.val)), - by simp [nhds_order_unbounded hu hl, infi_subtype, infi_prod], -iff.intro - (assume hs, by rw [this] at hs; from infi_sets_induct hs - ⟨l, u, hl', hu', by simp⟩ - begin - intro p, rcases p with ⟨⟨l, hl⟩, ⟨u, hu⟩⟩, - simp [set.subset_def], - intros s₁ s₂ hs₁ l' hl' u' hu' hs₂, - refine ⟨max l l', _, min u u', _⟩; - simp [*, lt_min_iff, max_lt_iff] {contextual := tt} - end - (assume s₁ s₂ h ⟨l, u, h₁, h₂, h₃⟩, ⟨l, u, h₁, h₂, assume b hu hl, h $ h₃ _ hu hl⟩)) - (assume ⟨l, u, hl, hu, h⟩, - by rw [this]; exact mem_infi_sets ⟨⟨l, hl⟩, ⟨u, hu⟩⟩ (assume b ⟨h₁, h₂⟩, h b h₁ h₂)) - lemma order_separated {a₁ a₂ : α} (h : a₁ < a₂) : ∃u v : set α, is_open u ∧ is_open v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ (∀b₁∈u, ∀b₂∈v, b₁ < b₂) := match dense_or_discrete a₁ a₂ with @@ -945,15 +918,14 @@ instance order_topology.regular_space : regular_space α := /-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`, provided `a` is neither a bottom element nor a top element. -/ -lemma mem_nhds_iff_exists_Ioo_subset' {a l' u' : α} {s : set α} - (hl' : l' < a) (hu' : a < u') : +lemma mem_nhds_iff_exists_Ioo_subset' {a : α} {s : set α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) : s ∈ 𝓝 a ↔ ∃l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s := begin split, { assume h, - rcases exists_Ico_subset_of_mem_nhds' h hu' with ⟨u, au, hu⟩, - rcases exists_Ioc_subset_of_mem_nhds' h hl' with ⟨l, la, hl⟩, - refine ⟨l, u, ⟨la.2, au.1⟩, λx hx, _⟩, + rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩, + rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩, + refine ⟨l, u, ⟨la, au⟩, λx hx, _⟩, cases le_total a x with hax hax, { exact hu ⟨hax, hx.2⟩ }, { exact hl ⟨hx.1, hax⟩ } }, @@ -965,7 +937,15 @@ end -/ lemma mem_nhds_iff_exists_Ioo_subset [no_top_order α] [no_bot_order α] {a : α} {s : set α} : s ∈ 𝓝 a ↔ ∃l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s := -let ⟨l', hl'⟩ := no_bot a in let ⟨u', hu'⟩ := no_top a in mem_nhds_iff_exists_Ioo_subset' hl' hu' +mem_nhds_iff_exists_Ioo_subset' (no_bot a) (no_top a) + +lemma nhds_basis_Ioo' {a : α} (hl : ∃l, l < a) (hu : ∃u, a < u) : + (𝓝 a).has_basis (λ b : α × α, b.1 < a ∧ a < b.2) (λ b, Ioo b.1 b.2) := +⟨λ s, (mem_nhds_iff_exists_Ioo_subset' hl hu).trans $ by simp⟩ + +lemma nhds_basis_Ioo [no_top_order α] [no_bot_order α] {a : α} : + (𝓝 a).has_basis (λ b : α × α, b.1 < a ∧ a < b.2) (λ b, Ioo b.1 b.2) := +nhds_basis_Ioo' (no_bot a) (no_top a) lemma filter.eventually.exists_Ioo_subset [no_top_order α] [no_bot_order α] {a : α} {p : α → Prop} (hp : ∀ᶠ x in 𝓝 a, p x) : diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean index c7cfc8862951f..d378e359da697 100644 --- a/src/topology/instances/real.lean +++ b/src/topology/instances/real.lean @@ -106,12 +106,12 @@ lemma real.is_topological_basis_Ioo_rat : is_topological_basis_of_open_of_nhds (by simp [is_open_Ioo] {contextual:=tt}) (assume a v hav hv, - let ⟨l, u, hl, hu, h⟩ := (mem_nhds_unbounded (no_top _) (no_bot _)).mp (mem_nhds_sets hv hav), + let ⟨l, u, ⟨hl, hu⟩, h⟩ := mem_nhds_iff_exists_Ioo_subset.mp (mem_nhds_sets hv hav), ⟨q, hlq, hqa⟩ := exists_rat_btwn hl, ⟨p, hap, hpu⟩ := exists_rat_btwn hu in ⟨Ioo q p, - by simp; exact ⟨q, p, rat.cast_lt.1 $ lt_trans hqa hap, rfl⟩, - ⟨hqa, hap⟩, assume a' ⟨hqa', ha'p⟩, h _ (lt_trans hlq hqa') (lt_trans ha'p hpu)⟩) + by { simp only [mem_Union], exact ⟨q, p, rat.cast_lt.1 $ hqa.trans hap, rfl⟩ }, + ⟨hqa, hap⟩, assume a' ⟨hqa', ha'p⟩, h ⟨hlq.trans hqa', ha'p.trans hpu⟩⟩) instance : second_countable_topology ℝ := ⟨⟨(⋃(a b : ℚ) (h : a < b), {Ioo a b}),