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}),