ordered.lean

/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
-/
import tactic.tfae
import order.liminf_limsup
import data.set.intervals
import topology.algebra.group
import topology.constructions

/-! # Theory of topology on ordered spaces

## Main definitions

The order topology on an ordered space is the topology generated by all open intervals (or
equivalently by those of the form `(-∞, a)` and `(b, +∞)`). We define it as `preorder.topology α`.
However, we do *not* register it as an instance (as many existing ordered types already have
topologies, which would be equal but not definitionally equal to `preorder.topology α`). Instead,
we introduce a class `order_topology α`(which is a `Prop`, also known as a mixin) saying that on
the type `α` having already a topological space structure and a preorder structure, the topological
structure is equal to the order topology.

We also introduce another (mixin) class `order_closed_topology α` saying that the set of points
`(x, y)` with `x ≤ y` is closed in the product space. This is automatically satisfied on a linear
order with the order topology.

We prove many basic properties of such topologies.

## Main statements

This file contains the proofs of the following facts. For exact requirements (`order_closed_topology`
vs `order_topology`, `preorder` vs `partial_order` vs `linear_order` etc) see their statements.

### Open / closed sets

* `is_open_lt` : if `f` and `g` are continuous functions, then `{x | f x < g x}` is open;
* `is_open_Iio`, `is_open_Ioi`, `is_open_Ioo` : open intervals are open;
* `is_closed_le` : if `f` and `g` are continuous functions, then `{x | f x ≤ g x}` is closed;
* `is_closed_Iic`, `is_closed_Ici`, `is_closed_Icc` : closed intervals are closed;
* `frontier_le_subset_eq`, `frontier_lt_subset_eq` : frontiers of both `{x | f x ≤ g x}`
  and `{x | f x < g x}` are included by `{x | f x = g x}`;
* `exists_Ioc_subset_of_mem_nhds`, `exists_Ico_subset_of_mem_nhds` : if `x < y`, then any
  neighborhood of `x` includes an interval `[x, z)` for some `z ∈ (x, y]`, and any neighborhood
  of `y` includes an interval `(z, y]` for some `z ∈ [x, y)`.

### Convergence and inequalities

* `le_of_tendsto_of_tendsto` : if `f` converges to `a`, `g` converges to `b`, and eventually
  `f x ≤ g x`, then `a ≤ b`
* `le_of_tendsto`, `ge_of_tendsto` : if `f` converges to `a` and eventually `f x ≤ b`
  (resp., `b ≤ f x`), then `a ≤ b` (resp., `b ≤ a);

### Min, max, `Sup` and `Inf`

* `continuous.min`, `continuous.max`: pointwise `min`/`max` of two continuous functions is continuous.
* `tendsto.min`, `tendsto.max` : if `f` tends to `a` and `g` tends to `b`, then their pointwise
  `min`/`max` tend to `min a b` and `max a b`, respectively.
* `tendsto_of_tendsto_of_tendsto_of_le_of_le` : theorem known as squeeze theorem,
  sandwich theorem, theorem of Carabinieri, and two policemen (and a drunk) theorem; if `g` and `h`
  both converge to `a`, and eventually `g x ≤ f x ≤ h x`, then `f` converges to `a`.

### Connected sets and Intermediate Value Theorem

* `is_connected_I??` : all intervals `I??` are connected,
* `is_connected.intermediate_value`, `intermediate_value_univ` : Intermediate Value Theorem for
  connected sets and connected spaces, respectively;
* `intermediate_value_Icc`, `intermediate_value_Icc'`: Intermediate Value Theorem for functions
  on closed intervals.

### Miscellaneous facts

* `compact.exists_forall_le`, `compact.exists_forall_ge` : extreme value theorem, a continuous
  function on a compact set takes its minimum and maximum values.
* `is_closed.Icc_subset_of_forall_mem_nhds_within` : “Continuous induction” principle;
  if `s ∩ [a, b]` is closed, `a ∈ s`, and for each `x ∈ [a, b) ∩ s` some of its right neighborhoods
  is included `s`, then `[a, b] ⊆ s`.
* `is_closed.Icc_subset_of_forall_exists_gt`, `is_closed.mem_of_ge_of_forall_exists_gt` : two
  other versions of the “continuous induction” principle.

## Implementation

We do _not_ register the order topology as an instance on a preorder (or even on a linear order).
Indeed, on many such spaces, a topology has already been constructed in a different way (think
of the discrete spaces `ℕ` or `ℤ`, or `ℝ` that could inherit a topology as the completion of `ℚ`),
and is in general not defeq to the one generated by the intervals. We make it available as a
definition `preorder.topology α` though, that can be registered as an instance when necessary, or
for specific types.
-/

open classical set lattice filter topological_space
open_locale topological_space classical

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

/-- A topology on a set which is both a topological space and a preorder is _order-closed_ if the
set of points `(x, y)` with `x ≤ y` is closed in the product space. We introduce this as a mixin.
This property is satisfied for the order topology on a linear order, but it can be satisfied more
generally, and suffices to derive many interesting properties relating order and topology. -/
class order_closed_topology (α : Type*) [topological_space α] [preorder α] : Prop :=
(is_closed_le' : is_closed (λp:α×α, p.1 ≤ p.2))

instance : Π [topological_space α], topological_space (order_dual α) := id

section order_closed_topology

section preorder
variables [topological_space α] [preorder α] [t : order_closed_topology α]
include t

lemma is_closed_le [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
  is_closed {b | f b ≤ g b} :=
continuous_iff_is_closed.mp (hf.prod_mk hg) _ t.is_closed_le'

lemma is_closed_le' (a : α) : is_closed {b | b ≤ a} :=
is_closed_le continuous_id continuous_const

lemma is_closed_Iic {a : α} : is_closed (Iic a) :=
is_closed_le' a

lemma is_closed_ge' (a : α) : is_closed {b | a ≤ b} :=
is_closed_le continuous_const continuous_id

lemma is_closed_Ici {a : α} : is_closed (Ici a) :=
is_closed_ge' a

instance : order_closed_topology (order_dual α) :=
⟨continuous_swap _ (@order_closed_topology.is_closed_le' α _ _ _)⟩

lemma is_closed_Icc {a b : α} : is_closed (Icc a b) :=
is_closed_inter is_closed_Ici is_closed_Iic

lemma le_of_tendsto_of_tendsto {f g : β → α} {b : filter β} {a₁ a₂ : α} (hb : b ≠ ⊥)
  (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) (h : ∀ᶠ x in b, f x ≤ g x) :
  a₁ ≤ a₂ :=
have tendsto (λb, (f b, g b)) b (𝓝 (a₁, a₂)),
  by rw [nhds_prod_eq]; exact hf.prod_mk hg,
show (a₁, a₂) ∈ {p:α×α | p.1 ≤ p.2},
  from mem_of_closed_of_tendsto hb this t.is_closed_le' h

lemma le_of_tendsto {f : β → α} {a b : α} {x : filter β}
  (nt : x ≠ ⊥) (lim : tendsto f x (𝓝 a)) (h : f ⁻¹' {c | c ≤ b} ∈ x) : a ≤ b :=
le_of_tendsto_of_tendsto nt lim tendsto_const_nhds h

lemma ge_of_tendsto {f : β → α} {a b : α} {x : filter β}
  (nt : x ≠ ⊥) (lim : tendsto f x (𝓝 a)) (h : f ⁻¹' {c | b ≤ c} ∈ x) : b ≤ a :=
le_of_tendsto_of_tendsto nt tendsto_const_nhds lim h

@[simp] lemma closure_le_eq [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
  closure {b | f b ≤ g b} = {b | f b ≤ g b} :=
closure_eq_iff_is_closed.mpr $ is_closed_le hf hg

lemma closure_lt_subset_le [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
  closure {b | f b < g b} ⊆ {b | f b ≤ g b} :=
by { rw [←closure_le_eq hf hg], exact closure_mono (λ b, le_of_lt) }

lemma continuous_within_at.closure_le [topological_space β]
 {f g : β → α} {s : set β} {x : β} (hx : x ∈ closure s)
 (hf : continuous_within_at f s x)
 (hg : continuous_within_at g s x)
 (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x :=
begin
  show (f x, g x) ∈ {p : α × α | p.1 ≤ p.2},
  suffices : (f x, g x) ∈ closure {p : α × α | p.1 ≤ p.2},
    by rwa ← closure_eq_iff_is_closed.2 (order_closed_topology.is_closed_le' α),
  exact (continuous_within_at.prod hf hg).mem_closure hx h
end

end preorder

section partial_order
variables [topological_space α] [partial_order α] [t : order_closed_topology α]
include t

private lemma is_closed_eq : is_closed {p : α × α | p.1 = p.2} :=
by simp [le_antisymm_iff];
   exact is_closed_inter t.is_closed_le' (is_closed_le continuous_snd continuous_fst)

@[priority 90] -- see Note [lower instance priority]
instance order_closed_topology.to_t2_space : t2_space α :=
{ t2 :=
  have is_open {p : α × α | p.1 ≠ p.2}, from is_closed_eq,
  assume a b h,
  let ⟨u, v, hu, hv, ha, hb, h⟩ := is_open_prod_iff.mp this a b h in
  ⟨u, v, hu, hv, ha, hb,
    set.eq_empty_iff_forall_not_mem.2 $ assume a ⟨h₁, h₂⟩,
    have a ≠ a, from @h (a, a) ⟨h₁, h₂⟩,
    this rfl⟩ }

end partial_order

section linear_order
variables [topological_space α] [linear_order α] [order_closed_topology α]

lemma is_open_lt [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
  is_open {b | f b < g b} :=
by simp [lt_iff_not_ge, -not_le]; exact is_closed_le hg hf

lemma is_open_Iio {a : α} : is_open (Iio a) :=
is_open_lt continuous_id continuous_const

lemma is_open_Ioi {a : α} : is_open (Ioi a) :=
is_open_lt continuous_const continuous_id

lemma is_open_Ioo {a b : α} : is_open (Ioo a b) :=
is_open_inter is_open_Ioi is_open_Iio

lemma is_connected.forall_Icc_subset {s : set α} (hs : is_connected s)
  {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
  Icc a b ⊆ s :=
begin
  assume x hx,
  obtain ⟨y, hy, hy'⟩ : (s ∩ ((Iic x) ∩ (Ici x))).nonempty,
    from is_connected_closed_iff.1 hs (Iic x) (Ici x) is_closed_Iic is_closed_Ici
      (λ y _, le_total y x) ⟨a, ha, hx.1⟩ ⟨b, hb, hx.2⟩,
  exact le_antisymm hy'.1 hy'.2 ▸ hy
end

/-- Intermediate Value Theorem for continuous functions on connected sets. -/
lemma is_connected.intermediate_value {γ : Type*} [topological_space γ] {s : set γ}
  (hs : is_connected s) {a b : γ} (ha : a ∈ s) (hb : b ∈ s) {f : γ → α} (hf : continuous_on f s) :
  Icc (f a) (f b) ⊆ f '' s :=
(hs.image f hf).forall_Icc_subset (mem_image_of_mem f ha) (mem_image_of_mem f hb)

/-- Intermediate Value Theorem for continuous functions on connected spaces. -/
lemma intermediate_value_univ {γ : Type*} [topological_space γ] [H : connected_space γ]
  (a b : γ) {f : γ → α} (hf : continuous f) :
  Icc (f a) (f b) ⊆ range f :=
@image_univ _ _ f ▸ H.is_connected_univ.intermediate_value trivial trivial hf.continuous_on

end linear_order

section decidable_linear_order
variables [topological_space α] [decidable_linear_order α] [order_closed_topology α] {f g : β → α}

section
variables [topological_space β] (hf : continuous f) (hg : continuous g)
include hf hg

lemma frontier_le_subset_eq : frontier {b | f b ≤ g b} ⊆ {b | f b = g b} :=
begin
  rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg],
  rintros b ⟨hb₁, hb₂⟩,
  refine le_antisymm hb₁ (closure_lt_subset_le hg hf _),
  convert hb₂ using 2, simp only [not_le.symm], refl
end

lemma frontier_lt_subset_eq : frontier {b | f b < g b} ⊆ {b | f b = g b} :=
by rw ← frontier_compl;
   convert frontier_le_subset_eq hg hf; simp [ext_iff, eq_comm]

lemma continuous.max : continuous (λb, max (f b) (g b)) :=
have ∀b∈frontier {b | f b ≤ g b}, g b = f b, from assume b hb, (frontier_le_subset_eq hf hg hb).symm,
continuous_if this hg hf

lemma continuous.min : continuous (λb, min (f b) (g b)) :=
have ∀b∈frontier {b | f b ≤ g b}, f b = g b, from assume b hb, frontier_le_subset_eq hf hg hb,
continuous_if this hf hg

end

lemma tendsto.max {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) :
  tendsto (λb, max (f b) (g b)) b (𝓝 (max a₁ a₂)) :=
show tendsto ((λp:α×α, max p.1 p.2) ∘ (λb, (f b, g b))) b (𝓝 (max a₁ a₂)),
  from tendsto.comp
    begin
      rw [←nhds_prod_eq],
      from continuous_iff_continuous_at.mp (continuous_fst.max continuous_snd) _
    end
    (hf.prod_mk hg)

lemma tendsto.min {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) :
  tendsto (λb, min (f b) (g b)) b (𝓝 (min a₁ a₂)) :=
show tendsto ((λp:α×α, min p.1 p.2) ∘ (λb, (f b, g b))) b (𝓝 (min a₁ a₂)),
  from tendsto.comp
    begin
      rw [←nhds_prod_eq],
      from continuous_iff_continuous_at.mp (continuous_fst.min continuous_snd) _
    end
    (hf.prod_mk hg)

end decidable_linear_order

end order_closed_topology

/-- The order topology on an ordered type is the topology generated by open intervals. We register
it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed.
We define it as a mixin. If you want to introduce the order topology on a preorder, use
`preorder.topology`. -/
class order_topology (α : Type*) [t : topological_space α] [preorder α] : Prop :=
(topology_eq_generate_intervals : t = generate_from {s | ∃a, s = Ioi a ∨ s = Iio a})

/-- (Order) topology on a partial order `α` generated by the subbase of open intervals
`(a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an
instance as many ordered sets are already endowed with the same topology, most often in a non-defeq
way though. Register as a local instance when necessary. -/
def preorder.topology (α : Type*) [preorder α] : topological_space α :=
generate_from {s : set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α | b < a}}

section order_topology

instance {α : Type*} [topological_space α] [partial_order α] [order_topology α] :
  order_topology (order_dual α) :=
⟨by convert @order_topology.topology_eq_generate_intervals α _ _ _;
  conv in (_ ∨ _) { rw or.comm }; refl⟩

section partial_order
variables [topological_space α] [partial_order α] [t : order_topology α]
include t

lemma is_open_iff_generate_intervals {s : set α} :
  is_open s ↔ generate_open {s | ∃a, s = Ioi a ∨ s = Iio a} s :=
by rw [t.topology_eq_generate_intervals]; refl

lemma is_open_lt' (a : α) : is_open {b:α | a < b} :=
by rw [@is_open_iff_generate_intervals α _ _ t]; exact generate_open.basic _ ⟨a, or.inl rfl⟩

lemma is_open_gt' (a : α) : is_open {b:α | b < a} :=
by rw [@is_open_iff_generate_intervals α _ _ t]; exact generate_open.basic _ ⟨a, or.inr rfl⟩

lemma lt_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a < x :=
mem_nhds_sets (is_open_lt' _) h

lemma le_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a ≤ x :=
(𝓝 b).sets_of_superset (lt_mem_nhds h) $ assume b hb, le_of_lt hb

lemma gt_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x < b :=
mem_nhds_sets (is_open_gt' _) h

lemma ge_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b :=
(𝓝 a).sets_of_superset (gt_mem_nhds h) $ assume b hb, le_of_lt hb

lemma nhds_eq_order (a : α) :
  𝓝 a = (⨅b ∈ Iio a, principal (Ioi b)) ⊓ (⨅b ∈ Ioi a, principal (Iio b)) :=
by rw [t.topology_eq_generate_intervals, nhds_generate_from];
from le_antisymm
  (le_inf
    (le_infi $ assume b, le_infi $ assume hb,
      infi_le_of_le {c : α | b < c} $ infi_le _ ⟨hb, b, or.inl rfl⟩)
    (le_infi $ assume b, le_infi $ assume hb,
      infi_le_of_le {c : α | c < b} $ infi_le _ ⟨hb, b, or.inr rfl⟩))
  (le_infi $ assume s, le_infi $ assume ⟨ha, b, hs⟩,
    match s, ha, hs with
    | _, h, (or.inl rfl) := inf_le_left_of_le $ infi_le_of_le b $ infi_le _ h
    | _, h, (or.inr rfl) := inf_le_right_of_le $ infi_le_of_le b $ infi_le _ h
    end)

@[nolint] -- see Note [nolint_ge]
lemma tendsto_order {f : β → α} {a : α} {x : filter β} :
  tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ (∀ a' > a, ∀ᶠ b in x, f b < a') :=
by simp [nhds_eq_order a, tendsto_inf, tendsto_infi, tendsto_principal]

/-- Also known as squeeze or sandwich theorem. -/
lemma tendsto_of_tendsto_of_tendsto_of_le_of_le {f g h : β → α} {b : filter β} {a : α}
  (hg : tendsto g b (𝓝 a)) (hh : tendsto h b (𝓝 a))
  (hgf : ∀ᶠ b in b, g b ≤ f b) (hfh : ∀ᶠ b in b, f b ≤ h b) :
  tendsto f b (𝓝 a) :=
tendsto_order.2
  ⟨assume a' h',
    have ∀ᶠ b in b, a' < g b, from (tendsto_order.1 hg).left a' h',
    by filter_upwards [this, hgf] assume a, lt_of_lt_of_le,
    assume a' h',
    have ∀ᶠ b in b, h b < a', from (tendsto_order.1 hh).right a' h',
    by filter_upwards [this, hfh] assume a h₁ h₂, lt_of_le_of_lt h₂ h₁⟩

lemma nhds_order_unbounded {a : α} (hu : ∃u, a < u) (hl : ∃l, l < a) :
  𝓝 a = (⨅l (h₂ : l < a) u (h₂ : a < u), principal (Ioo l u)) :=
let ⟨u, hu⟩ := hu, ⟨l, hl⟩ := hl in
calc 𝓝 a = (⨅b<a, principal {c | b < c}) ⊓ (⨅b>a, principal {c | c < b}) : nhds_eq_order a
  ... = (⨅b<a, principal {c | b < c} ⊓ (⨅b>a, principal {c | c < b})) :
    binfi_inf hl
  ... = (⨅l<a, (⨅u>a, principal {c | c < u} ⊓ principal {c | l < c})) :
    begin
      congr, funext x,
      congr, funext hx,
      rw [inf_comm],
      apply binfi_inf hu
    end
  ... = _ : by simp [inter_comm]; 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) :
  tendsto f x (𝓝 a) :=
by rw [nhds_order_unbounded hu hl];
from (tendsto_infi.2 $ assume l, tendsto_infi.2 $ assume hl,
  tendsto_infi.2 $ assume u, tendsto_infi.2 $ assume hu, tendsto_principal.2 $ h l u hl hu)

end partial_order

@[nolint] -- see Note [nolint_ge]
theorem induced_order_topology' {α : Type u} {β : Type v}
  [partial_order α] [ta : topological_space β] [partial_order β] [order_topology β]
  (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
  (H₁ : ∀ {a x}, x < f a → ∃ b < a, x ≤ f b)
  (H₂ : ∀ {a x}, f a < x → ∃ b > a, f b ≤ x) :
  @order_topology _ (induced f ta) _ :=
begin
  letI := induced f ta,
  refine ⟨eq_of_nhds_eq_nhds (λ a, _)⟩,
  rw [nhds_induced, nhds_generate_from, nhds_eq_order (f a)],
  apply le_antisymm,
  { refine le_infi (λ s, le_infi $ λ hs, le_principal_iff.2 _),
    rcases hs with ⟨ab, b, rfl|rfl⟩,
    { exact mem_comap_sets.2 ⟨{x | f b < x},
        mem_inf_sets_of_left $ mem_infi_sets _ $ mem_infi_sets (hf.2 ab) $ mem_principal_self _,
        λ x, hf.1⟩ },
    { exact mem_comap_sets.2 ⟨{x | x < f b},
        mem_inf_sets_of_right $ mem_infi_sets _ $ mem_infi_sets (hf.2 ab) $ mem_principal_self _,
        λ x, hf.1⟩ } },
  { rw [← map_le_iff_le_comap],
    refine le_inf _ _; refine le_infi (λ x, le_infi $ λ h, le_principal_iff.2 _); simp,
    { rcases H₁ h with ⟨b, ab, xb⟩,
      refine mem_infi_sets _ (mem_infi_sets ⟨ab, b, or.inl rfl⟩ (mem_principal_sets.2 _)),
      exact λ c hc, lt_of_le_of_lt xb (hf.2 hc) },
    { rcases H₂ h with ⟨b, ab, xb⟩,
      refine mem_infi_sets _ (mem_infi_sets ⟨ab, b, or.inr rfl⟩ (mem_principal_sets.2 _)),
      exact λ c hc, lt_of_lt_of_le (hf.2 hc) xb } },
end

theorem induced_order_topology {α : Type u} {β : Type v}
  [partial_order α] [ta : topological_space β] [partial_order β] [order_topology β]
  (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
  (H : ∀ {x y}, x < y → ∃ a, x < f a ∧ f a < y) :
  @order_topology _ (induced f ta) _ :=
induced_order_topology' f @hf
  (λ a x xa, let ⟨b, xb, ba⟩ := H xa in ⟨b, hf.1 ba, le_of_lt xb⟩)
  (λ a x ax, let ⟨b, ab, bx⟩ := H ax in ⟨b, hf.1 ab, le_of_lt bx⟩)

lemma nhds_top_order [topological_space α] [order_top α] [order_topology α] :
  𝓝 (⊤:α) = (⨅l (h₂ : l < ⊤), principal (Ioi l)) :=
by simp [nhds_eq_order (⊤:α)]

lemma nhds_bot_order [topological_space α] [order_bot α] [order_topology α] :
  𝓝 (⊥:α) = (⨅l (h₂ : ⊥ < l), principal (Iio l)) :=
by simp [nhds_eq_order (⊥:α)]

section linear_order

variables [topological_space α] [linear_order α] [order_topology α]

lemma exists_Ioc_subset_of_mem_nhds' {a : α} {s : set α} (hs : s ∈ 𝓝 a) {l : α} (hl : l < a) :
  ∃ l' ∈ Ico l a, Ioc l' a ⊆ s :=
begin
  rw [nhds_eq_order a] at hs,
  rcases hs with ⟨t₁, ht₁, t₂, ht₂, hts⟩,
  -- First we show that `t₂` includes `(-∞, a]`, so it suffices to show `(l', ∞) ⊆ t₁`
  suffices : ∃ l' ∈ Ico l a, Ioi l' ⊆ t₁,
  { have A : principal (Iic a) ≤ ⨅ b ∈ Ioi a, principal (Iio b),
      from (le_infi $ λ b, le_infi $ λ hb, principal_mono.2 $ Iic_subset_Iio.2 hb),
    have B : t₁ ∩ Iic a ⊆ s,
      from subset.trans (inter_subset_inter_right _ (A ht₂)) hts,
    from this.imp (λ l', Exists.imp $ λ hl' hl x hx, B ⟨hl hx.1, hx.2⟩) },
  clear hts ht₂ t₂,
  -- Now we find `l` such that `(l', ∞) ⊆ t₁`
  letI := classical.DLO α,
  rw [mem_binfi] at ht₁,
  { rcases ht₁ with ⟨b, hb, hb'⟩,
    exact ⟨max b l, ⟨le_max_right _ _, max_lt hb hl⟩,
      λ x hx, hb' $ Ioi_subset_Ioi (le_max_left _ _) hx⟩ },
  { intros b hb b' hb', simp only [mem_Iio] at hb hb',
    use [max b b', max_lt hb hb'],
    simp [le_refl] },
  exact ⟨l, hl⟩
end

lemma exists_Ico_subset_of_mem_nhds' {a : α} {s : set α} (hs : s ∈ 𝓝 a) {u : α} (hu : a < u) :
  ∃ u' ∈ Ioc a u, Ico a u' ⊆ s :=
begin
  convert @exists_Ioc_subset_of_mem_nhds' (order_dual α) _ _ _ _ _ hs _ hu,
  ext, rw [dual_Ico, dual_Ioc]
end

lemma exists_Ioc_subset_of_mem_nhds {a : α} {s : set α} (hs : s ∈ 𝓝 a) (h : ∃ l, l < a) :
  ∃ l < a, Ioc l a ⊆ s :=
let ⟨l', hl'⟩ := h in let ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds' hs hl' in ⟨l, hl.fst.2, hl.snd⟩

lemma exists_Ico_subset_of_mem_nhds {a : α} {s : set α} (hs : s ∈ 𝓝 a) (h : ∃ u, a < u) :
  ∃ 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}, principal (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₂,
      letI := classical.DLO α,
      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
| or.inl ⟨a, ha₁, ha₂⟩ := ⟨{a' | a' < a}, {a' | a < a'}, is_open_gt' a, is_open_lt' a, ha₁, ha₂,
    assume b₁ h₁ b₂ h₂, lt_trans h₁ h₂⟩
| or.inr ⟨h₁, h₂⟩ := ⟨{a | a < a₂}, {a | a₁ < a}, is_open_gt' a₂, is_open_lt' a₁, h, h,
    assume b₁ hb₁ b₂ hb₂,
    calc b₁ ≤ a₁ : h₂ _ hb₁
      ... < a₂ : h
      ... ≤ b₂ : h₁ _ hb₂⟩
end

@[priority 100] -- see Note [lower instance priority]
instance order_topology.to_order_closed_topology : order_closed_topology α :=
{ is_closed_le' :=
    is_open_prod_iff.mpr $ assume a₁ a₂ (h : ¬ a₁ ≤ a₂),
      have h : a₂ < a₁, from lt_of_not_ge h,
      let ⟨u, v, hu, hv, ha₁, ha₂, h⟩ := order_separated h in
      ⟨v, u, hv, hu, ha₂, ha₁, assume ⟨b₁, b₂⟩ ⟨h₁, h₂⟩, not_le_of_gt $ h b₂ h₂ b₁ h₁⟩ }

lemma order_topology.t2_space : t2_space α := by apply_instance

@[priority 100] -- see Note [lower instance priority]
instance order_topology.regular_space : regular_space α :=
{ regular := assume s a hs ha,
    have hs' : -s ∈ 𝓝 a, from mem_nhds_sets hs ha,
    have ∃t:set α, is_open t ∧ (∀l∈ s, l < a → l ∈ t) ∧ 𝓝 a ⊓ principal t = ⊥,
      from by_cases
        (assume h : ∃l, l < a,
          let ⟨l, hl, h⟩ := exists_Ioc_subset_of_mem_nhds hs' h in
          match dense_or_discrete l a with
          | or.inl ⟨b, hb₁, hb₂⟩ := ⟨{a | a < b}, is_open_gt' _,
              assume c hcs hca, show c < b,
                from lt_of_not_ge $ assume hbc, h ⟨lt_of_lt_of_le hb₁ hbc, le_of_lt hca⟩ hcs,
              inf_principal_eq_bot $ (𝓝 a).sets_of_superset (mem_nhds_sets (is_open_lt' _) hb₂) $
                assume x (hx : b < x), show ¬ x < b, from not_lt.2 $ le_of_lt hx⟩
          | or.inr ⟨h₁, h₂⟩ := ⟨{a' | a' < a}, is_open_gt' _, assume b hbs hba, hba,
              inf_principal_eq_bot $ (𝓝 a).sets_of_superset (mem_nhds_sets (is_open_lt' _) hl) $
                assume x (hx : l < x), show ¬ x < a, from not_lt.2 $ h₁ _ hx⟩
          end)
        (assume : ¬ ∃l, l < a, ⟨∅, is_open_empty, assume l _ hl, (this ⟨l, hl⟩).elim,
          by rw [principal_empty, inf_bot_eq]⟩),
    let ⟨t₁, ht₁o, ht₁s, ht₁a⟩ := this in
    have ∃t:set α, is_open t ∧ (∀u∈ s, u>a → u ∈ t) ∧ 𝓝 a ⊓ principal t = ⊥,
      from by_cases
        (assume h : ∃u, u > a,
          let ⟨u, hu, h⟩ := exists_Ico_subset_of_mem_nhds hs' h in
          match dense_or_discrete a u with
          | or.inl ⟨b, hb₁, hb₂⟩ := ⟨{a | b < a}, is_open_lt' _,
              assume c hcs hca, show c > b,
                from lt_of_not_ge $ assume hbc, h ⟨le_of_lt hca, lt_of_le_of_lt hbc hb₂⟩ hcs,
              inf_principal_eq_bot $ (𝓝 a).sets_of_superset (mem_nhds_sets (is_open_gt' _) hb₁) $
                assume x (hx : b > x), show ¬ x > b, from not_lt.2 $ le_of_lt hx⟩
          | or.inr ⟨h₁, h₂⟩ := ⟨{a' | a' > a}, is_open_lt' _, assume b hbs hba, hba,
              inf_principal_eq_bot $ (𝓝 a).sets_of_superset (mem_nhds_sets (is_open_gt' _) hu) $
                assume x (hx : u > x), show ¬ x > a, from not_lt.2 $ h₂ _ hx⟩
          end)
        (assume : ¬ ∃u, u > a, ⟨∅, is_open_empty, assume l _ hl, (this ⟨l, hl⟩).elim,
          by rw [principal_empty, inf_bot_eq]⟩),
    let ⟨t₂, ht₂o, ht₂s, ht₂a⟩ := this in
    ⟨t₁ ∪ t₂, is_open_union ht₁o ht₂o,
      assume x hx,
      have x ≠ a, from assume eq, ha $ eq ▸ hx,
      (ne_iff_lt_or_gt.mp this).imp (ht₁s _ hx) (ht₂s _ hx),
      by rw [←sup_principal, inf_sup_left, ht₁a, ht₂a, bot_sup_eq]⟩,
  ..order_topology.t2_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') :
  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, _⟩,
    cases le_total a x with hax hax,
    { exact hu ⟨hax, hx.2⟩ },
    { exact hl ⟨hx.1, hax⟩ } },
  { rintros ⟨l, u, ha, h⟩,
    apply mem_sets_of_superset (mem_nhds_sets is_open_Ioo ha) h }
end

/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`. -/
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'

/-!
### Neighborhoods to the left and to the right

Limits to the left and to the right of real functions are defined in terms of neighborhoods to
the left and to the right, either open or closed, i.e., members of `nhds_within a (Ioi a)` and
`nhds_wihin a (Ici a)` on the right, and similarly on the left. Such neighborhoods can be
characterized as the sets containing suitable intervals to the right or to the left of `a`.
We give now these characterizations. -/

-- NB: If you extend the list, append to the end please to avoid breaking the API
/-- The following statements are equivalent:

0. `s` is a neighborhood of `a` within `(a, +∞)`
1. `s` is a neighborhood of `a` within `(a, b]`
2. `s` is a neighborhood of `a` within `(a, b)`
3. `s` includes `(a, u)` for some `u ∈ (a, b]`
4. `s` includes `(a, u)` for some `u > a` -/
lemma tfae_mem_nhds_within_Ioi {a b : α} (hab : a < b) (s : set α) :
  tfae [s ∈ nhds_within a (Ioi a), -- 0 : `s` is a neighborhood of `a` within `(a, +∞)`
    s ∈ nhds_within a (Ioc a b),   -- 1 : `s` is a neighborhood of `a` within `(a, b]`
    s ∈ nhds_within a (Ioo a b),   -- 2 : `s` is a neighborhood of `a` within `(a, b)`
    ∃ u ∈ Ioc a b, Ioo a u ⊆ s,    -- 3 : `s` includes `(a, u)` for some `u ∈ (a, b]`
    ∃ u ∈ Ioi a, Ioo a u ⊆ s] :=   -- 4 : `s` includes `(a, u)` for some `u > a`
begin
  tfae_have : 1 → 2, from λ h, nhds_within_mono _ Ioc_subset_Ioi_self h,
  tfae_have : 2 → 3, from λ h, nhds_within_mono _ Ioo_subset_Ioc_self h,
  tfae_have : 4 → 5, from λ ⟨u, umem, hu⟩, ⟨u, umem.1, hu⟩,
  tfae_have : 5 → 1,
  { rintros ⟨u, hau, hu⟩,
    exact mem_nhds_within.2 ⟨Iio u, is_open_Iio, hau, by rwa [inter_comm, Ioi_inter_Iio]⟩ },
  tfae_have : 3 → 4,
  { assume h,
    rcases mem_nhds_within_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩,
    rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩,
    refine ⟨u, au, λx hx, _⟩,
    refine hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, _⟩,
    exact Ioo_subset_Ioo_right au.2 hx  },
  tfae_finish
end

@[simp] lemma nhds_within_Ioc_eq_nhds_within_Ioi {a b : α} (h : a < b) :
  nhds_within a (Ioc a b) = nhds_within a (Ioi a) :=
filter.ext $ λ s, (tfae_mem_nhds_within_Ioi h s).out 1 0

@[simp] lemma nhds_within_Ioo_eq_nhds_within_Ioi {a b : α} (hu : a < b) :
  nhds_within a (Ioo a b) = nhds_within a (Ioi a) :=
filter.ext $ λ s, (tfae_mem_nhds_within_Ioi hu s).out 2 0

lemma mem_nhds_within_Ioi_iff_exists_mem_Ioc_Ioo_subset {a u' : α} {s : set α} (hu' : a < u') :
  s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioc a u', Ioo a u ⊆ s :=
(tfae_mem_nhds_within_Ioi hu' s).out 0 3

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u < u'`, provided `a` is not a top element. -/
lemma mem_nhds_within_Ioi_iff_exists_Ioo_subset' {a u' : α} {s : set α} (hu' : a < u') :
  s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioi a, Ioo a u ⊆ s :=
(tfae_mem_nhds_within_Ioi hu' s).out 0 4

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u`. -/
lemma mem_nhds_within_Ioi_iff_exists_Ioo_subset [no_top_order α] {a : α} {s : set α} :
  s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioi a, Ioo a u ⊆ s :=
let ⟨u', hu'⟩ := no_top a in mem_nhds_within_Ioi_iff_exists_Ioo_subset' hu'

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u]`
with `a < u`. -/
lemma mem_nhds_within_Ioi_iff_exists_Ioc_subset [no_top_order α] [densely_ordered α]
  {a : α} {s : set α} : s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioi a, Ioc a u ⊆ s :=
begin
  rw mem_nhds_within_Ioi_iff_exists_Ioo_subset,
  split,
  { rintros ⟨u, au, as⟩,
    rcases dense au with ⟨v, hv⟩,
    exact ⟨v, hv.1, λx hx, as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩ },
  { rintros ⟨u, au, as⟩,
    exact ⟨u, au, subset.trans Ioo_subset_Ioc_self as⟩ }
end

lemma Ioo_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) :
  Ioo a c ∈ nhds_within b (Ioi b) :=
(mem_nhds_within_Ioi_iff_exists_Ioo_subset' H.2).2 ⟨c, H.2, Ioo_subset_Ioo_left H.1⟩

lemma Ioc_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) :
  Ioc a c ∈ nhds_within b (Ioi b) :=
mem_sets_of_superset (Ioo_mem_nhds_within_Ioi H) Ioo_subset_Ioc_self

lemma Ico_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) :
  Ico a c ∈ nhds_within b (Ioi b) :=
mem_sets_of_superset (Ioo_mem_nhds_within_Ioi H) Ioo_subset_Ico_self

lemma Icc_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) :
  Icc a c ∈ nhds_within b (Ioi b) :=
mem_sets_of_superset (Ioo_mem_nhds_within_Ioi H) Ioo_subset_Icc_self

/-- The following statements are equivalent:

0. `s` is a neighborhood of `b` within `(-∞, b)`
1. `s` is a neighborhood of `b` within `[a, b)`
2. `s` is a neighborhood of `b` within `(a, b)`
3. `s` includes `(l, b)` for some `l ∈ [a, b)`
4. `s` includes `(l, b)` for some `l < b` -/
lemma tfae_mem_nhds_within_Iio {a b : α} (h : a < b) (s : set α) :
  tfae [s ∈ nhds_within b (Iio b), -- 0 : `s` is a neighborhood of `b` within `(-∞, b)`
    s ∈ nhds_within b (Ico a b),   -- 1 : `s` is a neighborhood of `b` within `[a, b)`
    s ∈ nhds_within b (Ioo a b),   -- 2 : `s` is a neighborhood of `b` within `(a, b)`
    ∃ l ∈ Ico a b, Ioo l b ⊆ s,    -- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)`
    ∃ l ∈ Iio b, Ioo l b ⊆ s] :=   -- 4 : `s` includes `(l, b)` for some `l < b`
begin
  have := @tfae_mem_nhds_within_Ioi (order_dual α) _ _ _ _ _ h s,
  -- If we call `convert` here, it generates wrong equations, so we need to simplify first
  simp only [exists_prop] at this ⊢,
  rw [dual_Ioi, dual_Ioc, dual_Ioo] at this,
  convert this; ext l; rw [dual_Ioo]
end

@[simp] lemma nhds_within_Ico_eq_nhds_within_Iio {a b : α} (h : a < b) :
  nhds_within b (Ico a b) = nhds_within b (Iio b) :=
filter.ext $ λ s, (tfae_mem_nhds_within_Iio h s).out 1 0

@[simp] lemma nhds_within_Ioo_eq_nhds_within_Iio {a b : α} (h : a < b) :
  nhds_within b (Ioo a b) = nhds_within b (Iio b) :=
filter.ext $ λ s, (tfae_mem_nhds_within_Iio h s).out 2 0

lemma mem_nhds_within_Iio_iff_exists_mem_Ico_Ioo_subset {a l' : α} {s : set α} (hl' : l' < a) :
  s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Ico l' a, Ioo l a ⊆ s :=
(tfae_mem_nhds_within_Iio hl' s).out 0 3

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`, provided `a` is not a bottom element. -/
lemma mem_nhds_within_Iio_iff_exists_Ioo_subset' {a l' : α} {s : set α} (hl' : l' < a) :
  s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Iio a, Ioo l a ⊆ s :=
(tfae_mem_nhds_within_Iio hl' s).out 0 4

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`. -/
lemma mem_nhds_within_Iio_iff_exists_Ioo_subset [no_bot_order α] {a : α} {s : set α} :
  s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Iio a, Ioo l a ⊆ s :=
let ⟨l', hl'⟩ := no_bot a in mem_nhds_within_Iio_iff_exists_Ioo_subset' hl'

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `[l, a)`
with `l < a`. -/
lemma mem_nhds_within_Iio_iff_exists_Ico_subset [no_bot_order α] [densely_ordered α]
  {a : α} {s : set α} : s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Iio a, Ico l a ⊆ s :=
begin
  convert @mem_nhds_within_Ioi_iff_exists_Ioc_subset (order_dual α) _ _ _ _ _ _ _,
  simp only [dual_Ioc], refl
end

lemma Ioo_mem_nhds_within_Iio {a b c : α} (h : b ∈ Ioc a c) :
  Ioo a c ∈ nhds_within b (Iio b) :=
(mem_nhds_within_Iio_iff_exists_Ioo_subset' h.1).2 ⟨a, h.1, Ioo_subset_Ioo_right h.2⟩

lemma Ioc_mem_nhds_within_Iio {a b c : α} (h : b ∈ Ioc a c) :
  Ioc a c ∈ nhds_within b (Iio b) :=
mem_sets_of_superset (Ioo_mem_nhds_within_Iio h) Ioo_subset_Ioc_self

lemma Ico_mem_nhds_within_Iio {a b c : α} (h : b ∈ Ioc a c) :
  Ico a c ∈ nhds_within b (Iio b) :=
mem_sets_of_superset (Ioo_mem_nhds_within_Iio h) Ioo_subset_Ico_self

lemma Icc_mem_nhds_within_Iio {a b c : α} (h : b ∈ Ioc a c) :
  Icc a c ∈ nhds_within b (Iio b) :=
mem_sets_of_superset (Ioo_mem_nhds_within_Iio h) Ioo_subset_Icc_self

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u`, provided `a` is not a top element. -/
lemma mem_nhds_within_Ici_iff_exists_Ico_subset' {a u' : α} {s : set α} (hu' : a < u') :
  s ∈ nhds_within a (Ici a) ↔ ∃u, a < u ∧ Ico a u ⊆ s :=
begin
  split,
  { assume h,
    rcases mem_nhds_within_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩,
    rcases exists_Ico_subset_of_mem_nhds va ⟨u', hu'⟩ with ⟨u, au, hu⟩,
    refine ⟨u, au, λx hx, _⟩,
    refine hv ⟨_, hx.1⟩,
    exact hu hx },
  { rintros ⟨u, au, hu⟩,
    rw mem_nhds_within_iff_exists_mem_nhds_inter,
    refine ⟨Iio u, mem_nhds_sets is_open_Iio au, _⟩,
    rwa [inter_comm, Ici_inter_Iio] }
end

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u`. -/
lemma mem_nhds_within_Ici_iff_exists_Ico_subset [no_top_order α] {a : α} {s : set α} :
  s ∈ nhds_within a (Ici a) ↔ ∃u, a < u ∧ Ico a u ⊆ s :=
let ⟨u', hu'⟩ := no_top a in mem_nhds_within_Ici_iff_exists_Ico_subset' hu'

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u]`
with `a < u`. -/
lemma mem_nhds_within_Ici_iff_exists_Icc_subset [no_top_order α] [densely_ordered α]
  {a : α} {s : set α} : s ∈ nhds_within a (Ici a) ↔ ∃u, a < u ∧ Icc a u ⊆ s :=
begin
  rw mem_nhds_within_Ici_iff_exists_Ico_subset,
  split,
  { rintros ⟨u, au, as⟩,
    rcases dense au with ⟨v, hv⟩,
    exact ⟨v, hv.1, λx hx, as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩ },
  { rintros ⟨u, au, as⟩,
    exact ⟨u, au, subset.trans Ico_subset_Icc_self as⟩ }
end

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`, provided `a` is not a bottom element. -/
lemma mem_nhds_within_Iic_iff_exists_Ioc_subset' {a l' : α} {s : set α} (hl' : l' < a) :
  s ∈ nhds_within a (Iic a) ↔ ∃l, l < a ∧ Ioc l a ⊆ s :=
begin
  split,
  { assume h,
    rcases mem_nhds_within_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩,
    rcases exists_Ioc_subset_of_mem_nhds va ⟨l', hl'⟩ with ⟨l, la, hl⟩,
    refine ⟨l, la, λx hx, _⟩,
    refine hv ⟨_, hx.2⟩,
    exact hl hx },
  { rintros ⟨l, la, ha⟩,
    rw mem_nhds_within_iff_exists_mem_nhds_inter,
    refine ⟨Ioi l, mem_nhds_sets is_open_Ioi la, _⟩,
    rwa [Ioi_inter_Iic] }
end

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`. -/
lemma mem_nhds_within_Iic_iff_exists_Ioc_subset [no_bot_order α] {a : α} {s : set α} :
  s ∈ nhds_within a (Iic a) ↔ ∃l, l < a ∧ Ioc l a ⊆ s :=
let ⟨l', hl'⟩ := no_bot a in mem_nhds_within_Iic_iff_exists_Ioc_subset' hl'

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `[l, a]`
with `l < a`. -/
lemma mem_nhds_within_Iic_iff_exists_Icc_subset [no_bot_order α] [densely_ordered α]
  {a : α} {s : set α} : s ∈ nhds_within a (Iic a) ↔ ∃l, l < a ∧ Icc l a ⊆ s :=
begin
  rw mem_nhds_within_Iic_iff_exists_Ioc_subset,
  split,
  { rintros ⟨l, la, as⟩,
    rcases dense la with ⟨v, hv⟩,
    refine ⟨v, hv.2, λx hx, as ⟨lt_of_lt_of_le hv.1 hx.1, hx.2⟩⟩, },
  { rintros ⟨l, la, as⟩,
    exact ⟨l, la, subset.trans Ioc_subset_Icc_self as⟩ }
end

end linear_order

lemma preimage_neg [add_group α] : preimage (has_neg.neg : α → α) = image (has_neg.neg : α → α) :=
(image_eq_preimage_of_inverse neg_neg neg_neg).symm

lemma filter.map_neg [add_group α] : map (has_neg.neg : α → α) = comap (has_neg.neg : α → α) :=
funext $ assume f, map_eq_comap_of_inverse (funext neg_neg) (funext neg_neg)

section topological_add_group

variables [topological_space α] [ordered_comm_group α] [topological_add_group α]

lemma neg_preimage_closure {s : set α} : (λr:α, -r) ⁻¹' closure s = closure ((λr:α, -r) '' s) :=
have (λr:α, -r) ∘ (λr:α, -r) = id, from funext neg_neg,
by rw [preimage_neg]; exact
  (subset.antisymm (image_closure_subset_closure_image continuous_neg) $
    calc closure ((λ (r : α), -r) '' s) = (λr, -r) '' ((λr, -r) '' closure ((λ (r : α), -r) '' s)) :
        by rw [←image_comp, this, image_id]
      ... ⊆ (λr, -r) '' closure ((λr, -r) '' ((λ (r : α), -r) '' s)) :
        mono_image $ image_closure_subset_closure_image continuous_neg
      ... = _ : by rw [←image_comp, this, image_id])

end topological_add_group

section order_topology

variables [topological_space α] [topological_space β]
  [linear_order α] [linear_order β] [order_topology α] [order_topology β]

lemma nhds_principal_ne_bot_of_is_lub {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) :
  𝓝 a ⊓ principal s ≠ ⊥ :=
let ⟨a', ha'⟩ := hs in
forall_sets_nonempty_iff_ne_bot.mp $ assume t ht,
  let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := mem_inf_sets.mp ht in
  by_cases
    (assume h : a = a',
      have a ∈ t₁, from mem_of_nhds ht₁,
      have a ∈ t₂, from ht₂ $ by rwa [h],
      ⟨a, ht ⟨‹a ∈ t₁›, ‹a ∈ t₂›⟩⟩)
    (assume : a ≠ a',
      have a' < a, from lt_of_le_of_ne (ha.left ‹a' ∈ s›) this.symm,
      let ⟨l, hl, hlt₁⟩ := exists_Ioc_subset_of_mem_nhds ht₁ ⟨a', this⟩ in
      have ∃a'∈s, l < a',
        from classical.by_contradiction $ assume : ¬ ∃a'∈s, l < a',
          have ∀a'∈s, a' ≤ l, from assume a ha, not_lt.1 $ assume ha', this ⟨a, ha, ha'⟩,
          have ¬ l < a, from not_lt.2 $ ha.right this,
          this ‹l < a›,
      let ⟨a', ha', ha'l⟩ := this in
      have a' ∈ t₁, from hlt₁ ⟨‹l < a'›, ha.left ha'⟩,
      ⟨a', ht ⟨‹a' ∈ t₁›, ht₂ ‹a' ∈ s›⟩⟩)

lemma nhds_principal_ne_bot_of_is_glb : ∀ {a : α} {s : set α}, is_glb s a → s.nonempty →
  𝓝 a ⊓ principal s ≠ ⊥ :=
@nhds_principal_ne_bot_of_is_lub (order_dual α) _ _ _

lemma is_lub_of_mem_nhds {s : set α} {a : α} {f : filter α}
  (hsa : a ∈ upper_bounds s) (hsf : s ∈ f) (hfa : f ⊓ 𝓝 a ≠ ⊥) : is_lub s a :=
⟨hsa, assume b hb,
  not_lt.1 $ assume hba,
  have s ∩ {a | b < a} ∈ f ⊓ 𝓝 a,
    from inter_mem_inf_sets hsf (mem_nhds_sets (is_open_lt' _) hba),
  let ⟨x, ⟨hxs, hxb⟩⟩ := nonempty_of_mem_sets hfa this in
  have b < b, from lt_of_lt_of_le hxb $ hb hxs,
  lt_irrefl b this⟩

lemma is_glb_of_mem_nhds : ∀ {s : set α} {a : α} {f : filter α},
  a ∈ lower_bounds s → s ∈ f → f ⊓ 𝓝 a ≠ ⊥ → is_glb s a :=
@is_lub_of_mem_nhds (order_dual α) _ _ _

lemma is_lub_of_is_lub_of_tendsto {f : α → β} {s : set α} {a : α} {b : β}
  (hf : ∀x∈s, ∀y∈s, x ≤ y → f x ≤ f y) (ha : is_lub s a) (hs : s.nonempty)
  (hb : tendsto f (𝓝 a ⊓ principal s) (𝓝 b)) : is_lub (f '' s) b :=
have hnbot : (𝓝 a ⊓ principal s) ≠ ⊥, from nhds_principal_ne_bot_of_is_lub ha hs,
have ∀a'∈s, ¬ b < f a',
  from assume a' ha' h,
  have ∀ᶠ x in 𝓝 b, x < f a', from mem_nhds_sets (is_open_gt' _) h,
  let ⟨t₁, ht₁, t₂, ht₂, hs⟩ := mem_inf_sets.mp (hb this) in
  by_cases
    (assume h : a = a',
      have a ∈ t₁ ∩ t₂, from ⟨mem_of_nhds ht₁, ht₂ $ by rwa [h]⟩,
      have f a < f a', from hs this,
      lt_irrefl (f a') $ by rwa [h] at this)
    (assume h : a ≠ a',
      have a' < a, from lt_of_le_of_ne (ha.left ha') h.symm,
      have {x | a' < x} ∈ 𝓝 a, from mem_nhds_sets (is_open_lt' _) this,
      have {x | a' < x} ∩ t₁ ∈ 𝓝 a, from inter_mem_sets this ht₁,
      have ({x | a' < x} ∩ t₁) ∩ s ∈ 𝓝 a ⊓ principal s,
        from inter_mem_inf_sets this (subset.refl s),
      let ⟨x, ⟨hx₁, hx₂⟩, hx₃⟩ := nonempty_of_mem_sets hnbot this in
      have hxa' : f x < f a', from hs ⟨hx₂, ht₂ hx₃⟩,
      have ha'x : f a' ≤ f x, from hf _ ha' _ hx₃ $ le_of_lt hx₁,
      lt_irrefl _ (lt_of_le_of_lt ha'x hxa')),
and.intro
  (assume b' ⟨a', ha', h_eq⟩, h_eq ▸ not_lt.1 $ this _ ha')
  (assume b' hb', le_of_tendsto hnbot hb $
      mem_inf_sets_of_right $ assume x hx, hb' $ mem_image_of_mem _ hx)

lemma is_glb_of_is_glb_of_tendsto {f : α → β} {s : set α} {a : α} {b : β}
  (hf : ∀x∈s, ∀y∈s, x ≤ y → f x ≤ f y) : is_glb s a → s.nonempty →
  tendsto f (𝓝 a ⊓ principal s) (𝓝 b) → is_glb (f '' s) b :=
@is_lub_of_is_lub_of_tendsto (order_dual α) (order_dual β) _ _ _ _ _ _ f s a b
  (λ x hx y hy, hf y hy x hx)

lemma is_glb_of_is_lub_of_tendsto : ∀ {f : α → β} {s : set α} {a : α} {b : β},
  (∀x∈s, ∀y∈s, x ≤ y → f y ≤ f x) → is_lub s a → s.nonempty →
  tendsto f (𝓝 a ⊓ principal s) (𝓝 b) → is_glb (f '' s) b :=
@is_lub_of_is_lub_of_tendsto α (order_dual β) _ _ _ _ _ _

lemma is_lub_of_is_glb_of_tendsto : ∀ {f : α → β} {s : set α} {a : α} {b : β},
  (∀x∈s, ∀y∈s, x ≤ y → f y ≤ f x) → is_glb s a → s.nonempty →
  tendsto f (𝓝 a ⊓ principal s) (𝓝 b) → is_lub (f '' s) b :=
@is_glb_of_is_glb_of_tendsto α (order_dual β) _ _ _ _ _ _

lemma mem_closure_of_is_lub {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) : a ∈ closure s :=
by rw closure_eq_nhds; exact nhds_principal_ne_bot_of_is_lub ha hs

lemma mem_of_is_lub_of_is_closed {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) (sc : is_closed s) : a ∈ s :=
by rw ←closure_eq_of_is_closed sc; exact mem_closure_of_is_lub ha hs

lemma mem_closure_of_is_glb {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) : a ∈ closure s :=
by rw closure_eq_nhds; exact nhds_principal_ne_bot_of_is_glb ha hs

lemma mem_of_is_glb_of_is_closed {a : α} {s : set α} (ha : is_glb s a) (hs : s.nonempty) (sc : is_closed s) : a ∈ s :=
by rw ←closure_eq_of_is_closed sc; exact mem_closure_of_is_glb ha hs

/-- A compact set is bounded below -/
lemma bdd_below_of_compact {α : Type u} [topological_space α] [linear_order α]
  [order_closed_topology α] [nonempty α] {s : set α} (hs : compact s) : bdd_below s :=
begin
  by_contra H,
  letI := classical.DLO α,
  rcases hs.elim_finite_subcover_image (λ x (_ : x ∈ s), @is_open_Ioi _ _ _ _ x) _
    with ⟨t, st, ft, ht⟩,
  { refine H ((bdd_below_finite ft).imp $ λ C hC y hy, _),
    rcases mem_bUnion_iff.1 (ht hy) with ⟨x, hx, xy⟩,
    exact le_trans (hC hx) (le_of_lt xy) },
  { refine λ x hx, mem_bUnion_iff.2 (not_imp_comm.1 _ H),
    exact λ h, ⟨x, λ y hy, le_of_not_lt (h.imp $ λ ys, ⟨_, hy, ys⟩)⟩ }
end

/-- A compact set is bounded above -/
lemma bdd_above_of_compact {α : Type u} [topological_space α] [linear_order α]
  [order_topology α] : Π [nonempty α] {s : set α}, compact s → bdd_above s :=
@bdd_below_of_compact (order_dual α) _ _ _

end order_topology

section linear_order

variables [topological_space α] [linear_order α] [order_topology α] [densely_ordered α]

/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`, unless `a` is a top
element. -/
lemma closure_Ioi' {a b : α} (hab : a < b) :
  closure (Ioi a) = Ici a :=
begin
  apply subset.antisymm,
  { exact closure_minimal Ioi_subset_Ici_self is_closed_Ici },
  { assume x hx,
    by_cases h : x = a,
    { rw h, exact mem_closure_of_is_glb is_glb_Ioi ⟨_, hab⟩ },
    { exact subset_closure (lt_of_le_of_ne hx (ne.symm h)) } }
end

/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`. -/
lemma closure_Ioi (a : α) [no_top_order α] :
  closure (Ioi a) = Ici a :=
let ⟨b, hb⟩ := no_top a in closure_Ioi' hb

/-- The closure of the interval `(-∞, a)` is the closed interval `(-∞, a]`, unless `a` is a bottom
element. -/
lemma closure_Iio' {a b : α} (hab : b < a) :
  closure (Iio a) = Iic a :=
begin
  apply subset.antisymm,
  { exact closure_minimal Iio_subset_Iic_self is_closed_Iic },
  { assume x hx,
    by_cases h : x = a,
    { rw h, exact mem_closure_of_is_lub is_lub_Iio ⟨_, hab⟩ },
    { apply subset_closure, by simpa [h] using lt_or_eq_of_le hx } }
end

/-- The closure of the interval `(-∞, a)` is the interval `(-∞, a]`. -/
lemma closure_Iio (a : α) [no_bot_order α] :
  closure (Iio a) = Iic a :=
let ⟨b, hb⟩ := no_bot a in closure_Iio' hb

/-- The closure of the open interval `(a, b)` is the closed interval `[a, b]`. -/
lemma closure_Ioo {a b : α} (hab : a < b) :
  closure (Ioo a b) = Icc a b :=
begin
  apply subset.antisymm,
  { exact closure_minimal Ioo_subset_Icc_self is_closed_Icc },
  { have hab' : (Ioo a b).nonempty, from nonempty_Ioo.2 hab,
    assume x hx,
    by_cases h : x = a,
    { rw h, exact mem_closure_of_is_glb (is_glb_Ioo hab) hab' },
    by_cases h' : x = b,
    { rw h', refine mem_closure_of_is_lub (is_lub_Ioo hab) hab' },
    exact subset_closure ⟨lt_of_le_of_ne hx.1 (ne.symm h), by simpa [h'] using lt_or_eq_of_le hx.2⟩ }
end

/-- The closure of the interval `(a, b]` is the closed interval `[a, b]`. -/
lemma closure_Ioc {a b : α} (hab : a < b) :
  closure (Ioc a b) = Icc a b :=
begin
  apply subset.antisymm,
  { exact closure_minimal Ioc_subset_Icc_self is_closed_Icc },
  { apply subset.trans _ (closure_mono Ioo_subset_Ioc_self),
    rw closure_Ioo hab }
end

/-- The closure of the interval `[a, b)` is the closed interval `[a, b]`. -/
lemma closure_Ico {a b : α} (hab : a < b) :
  closure (Ico a b) = Icc a b :=
begin
  apply subset.antisymm,
  { exact closure_minimal Ico_subset_Icc_self is_closed_Icc },
  { apply subset.trans _ (closure_mono Ioo_subset_Ico_self),
    rw closure_Ioo hab }
end

lemma nhds_within_Ioi_ne_bot' {a b c : α} (H₁ : a < c) (H₂ : a ≤ b) :
  nhds_within b (Ioi a) ≠ ⊥ :=
mem_closure_iff_nhds_within_ne_bot.1 $ by { rw [closure_Ioi' H₁], exact H₂ }

lemma nhds_within_Ioi_ne_bot [no_top_order α] {a b : α} (H : a ≤ b) :
  nhds_within b (Ioi a) ≠ ⊥ :=
let ⟨c, hc⟩ := no_top a in nhds_within_Ioi_ne_bot' hc H

lemma nhds_within_Ioi_self_ne_bot' {a b : α} (H : a < b) :
  nhds_within a (Ioi a) ≠ ⊥ :=
nhds_within_Ioi_ne_bot' H (le_refl a)

lemma nhds_within_Ioi_self_ne_bot [no_top_order α] (a : α) :
  nhds_within a (Ioi a) ≠ ⊥ :=
nhds_within_Ioi_ne_bot (le_refl a)

lemma nhds_within_Iio_ne_bot' {a b c : α} (H₁ : a < c) (H₂ : b ≤ c) :
  nhds_within b (Iio c) ≠ ⊥ :=
mem_closure_iff_nhds_within_ne_bot.1 $ by { rw [closure_Iio' H₁], exact H₂ }

lemma nhds_within_Iio_ne_bot [no_bot_order α] {a b : α} (H : a ≤ b) :
  nhds_within a (Iio b) ≠ ⊥ :=
let ⟨c, hc⟩ := no_bot b in nhds_within_Iio_ne_bot' hc H

lemma nhds_within_Iio_self_ne_bot' {a b : α} (H : a < b) :
  nhds_within b (Iio b) ≠ ⊥ :=
nhds_within_Iio_ne_bot' H (le_refl b)

lemma nhds_within_Iio_self_ne_bot [no_bot_order α] (a : α) :
  nhds_within a (Iio a) ≠ ⊥ :=
nhds_within_Iio_ne_bot (le_refl a)

end linear_order

section complete_linear_order

variables [complete_linear_order α] [topological_space α] [order_topology α]
  [complete_linear_order β] [topological_space β] [order_topology β] [nonempty γ]

lemma Sup_mem_closure {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) : Sup s ∈ closure s :=
mem_closure_of_is_lub is_lub_Sup hs

lemma Inf_mem_closure {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) : Inf s ∈ closure s :=
mem_closure_of_is_glb is_glb_Inf hs

lemma Sup_mem_of_is_closed {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) (hc : is_closed s) : Sup s ∈ s :=
mem_of_is_lub_of_is_closed  is_lub_Sup hs hc

lemma Inf_mem_of_is_closed {α : Type u} [topological_space α] [complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) (hc : is_closed s) : Inf s ∈ s :=
mem_of_is_glb_of_is_closed  is_glb_Inf hs hc

/-- A continuous monotone function sends supremum to supremum for nonempty sets. -/
lemma Sup_of_continuous' {f : α → β} (Mf : continuous f) (Cf : monotone f)
  {s : set α} (hs : s.nonempty) : f (Sup s) = Sup (f '' s) :=
--This is a particular case of the more general is_lub_of_is_lub_of_tendsto
(is_lub_iff_Sup_eq.1
  (is_lub_of_is_lub_of_tendsto (λ x hx y hy xy, Cf xy) is_lub_Sup hs $
    tendsto_le_left inf_le_left (Mf.tendsto _))).symm

/-- A continuous monotone function sending bot to bot sends supremum to supremum. -/
lemma Sup_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
  (fbot : f ⊥ = ⊥) {s : set α} : f (Sup s) = Sup (f '' s) :=
begin
  cases s.eq_empty_or_nonempty with h h,
  { simp [h, fbot] },
  { exact Sup_of_continuous' Mf Cf h }
end

/-- A continuous monotone function sends indexed supremum to indexed supremum. -/
lemma supr_of_continuous {f : α → β} {g : γ → α}
  (Mf : continuous f) (Cf : monotone f) : f (supr g) = supr (f ∘ g) :=
by { rw [supr, Sup_of_continuous' Mf Cf (range_nonempty g), ← range_comp, supr] }

/-- A continuous monotone function sends infimum to infimum for nonempty sets. -/
lemma Inf_of_continuous' {f : α → β} (Mf : continuous f) (Cf : monotone f)
  {s : set α} (hs : s.nonempty) : f (Inf s) = Inf (f '' s) :=
(is_glb_iff_Inf_eq.1
  (is_glb_of_is_glb_of_tendsto (λ x hx y hy xy, Cf xy) is_glb_Inf hs $
    tendsto_le_left inf_le_left (Mf.tendsto _))).symm

/-- A continuous monotone function sending top to top sends infimum to infimum. -/
lemma Inf_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
  (ftop : f ⊤ = ⊤) {s : set α} : f (Inf s) = Inf (f '' s) :=
begin
  cases s.eq_empty_or_nonempty with h h,
  { simpa [h] },
  { exact Inf_of_continuous' Mf Cf h }
end

/-- A continuous monotone function sends indexed infimum to indexed infimum. -/
lemma infi_of_continuous {f : α → β} {g : γ → α}
  (Mf : continuous f) (Cf : monotone f) : f (infi g) = infi (f ∘ g) :=
by rw [infi, Inf_of_continuous' Mf Cf (range_nonempty g), ← range_comp, infi]

end complete_linear_order


section conditionally_complete_linear_order

variables [conditionally_complete_linear_order α] [topological_space α] [order_topology α]
  [conditionally_complete_linear_order β] [topological_space β] [order_topology β] [nonempty γ]

lemma cSup_mem_closure {α : Type u} [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) (B : bdd_above s) : Sup s ∈ closure s :=
mem_closure_of_is_lub (is_lub_cSup hs B) hs

lemma cInf_mem_closure {α : Type u} [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) (B : bdd_below s) : Inf s ∈ closure s :=
mem_closure_of_is_glb (is_glb_cInf hs B) hs

lemma cSup_mem_of_is_closed {α : Type u} [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) (hc : is_closed s) (B : bdd_above s) : Sup s ∈ s :=
mem_of_is_lub_of_is_closed (is_lub_cSup hs B) hs hc

lemma cInf_mem_of_is_closed {α : Type u} [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  {s : set α} (hs : s.nonempty) (hc : is_closed s) (B : bdd_below s) : Inf s ∈ s :=
mem_of_is_glb_of_is_closed (is_glb_cInf hs B) hs hc

/-- A continuous monotone function sends supremum to supremum in conditionally complete
lattices, under a boundedness assumption. -/
lemma cSup_of_cSup_of_monotone_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
  {s : set α} (ne : s.nonempty) (H : bdd_above s) : f (Sup s) = Sup (f '' s) :=
begin
  refine (is_lub_iff_eq_of_is_lub _).1
    (is_lub_cSup (ne.image f) (bdd_above_of_bdd_above_of_monotone Cf H)),
  refine is_lub_of_is_lub_of_tendsto (λx hx y hy xy, Cf xy) (is_lub_cSup ne H) ne _,
  exact tendsto_le_left inf_le_left (Mf.tendsto _)
end

/-- A continuous monotone function sends indexed supremum to indexed supremum in conditionally complete
lattices, under a boundedness assumption. -/
lemma csupr_of_csupr_of_monotone_of_continuous {f : α → β} {g : γ → α}
  (Mf : continuous f) (Cf : monotone f) (H : bdd_above (range g)) : f (supr g) = supr (f ∘ g) :=
by rw [supr, cSup_of_cSup_of_monotone_of_continuous Mf Cf (range_nonempty _) H, ← range_comp, supr]

/-- A continuous monotone function sends infimum to infimum in conditionally complete
lattices, under a boundedness assumption. -/
lemma cInf_of_cInf_of_monotone_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
  {s : set α} (ne : s.nonempty) (H : bdd_below s) : f (Inf s) = Inf (f '' s) :=
begin
  refine (is_glb_iff_eq_of_is_glb _).1
    (is_glb_cInf (ne.image _) (bdd_below_of_bdd_below_of_monotone Cf H)),
  refine is_glb_of_is_glb_of_tendsto (λx hx y hy xy, Cf xy) (is_glb_cInf ne H) ne _,
  exact tendsto_le_left inf_le_left (Mf.tendsto _)
end

/-- A continuous monotone function sends indexed infimum to indexed infimum in conditionally complete
lattices, under a boundedness assumption. -/
lemma cinfi_of_cinfi_of_monotone_of_continuous {f : α → β} {g : γ → α}
  (Mf : continuous f) (Cf : monotone f) (H : bdd_below (range g)) : f (infi g) = infi (f ∘ g) :=
by rw [infi, cInf_of_cInf_of_monotone_of_continuous Mf Cf (range_nonempty _) H, ← range_comp, infi]

/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and the set `s ∩ [a, b)` has no maximal point, then `b ∈ s`. -/
lemma is_closed.mem_of_ge_of_forall_exists_gt {a b : α} {s : set α} (hs : is_closed (s ∩ Icc a b))
  (ha : a ∈ s) (hab : a ≤ b) (hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).nonempty) :
  b ∈ s :=
begin
  let S := s ∩ Icc a b,
  replace ha : a ∈ S, from ⟨ha, left_mem_Icc.2 hab⟩,
  have Sbd : bdd_above S, from ⟨b, λ z hz, hz.2.2⟩,
  let c := Sup (s ∩ Icc a b),
  have c_mem : c ∈ S, from cSup_mem_of_is_closed ⟨_, ha⟩ hs Sbd,
  have c_le : c ≤ b, from cSup_le ⟨_, ha⟩ (λ x hx, hx.2.2),
  cases eq_or_lt_of_le c_le with hc hc, from hc ▸ c_mem.1,
  exfalso,
  rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩,
  exact not_lt_of_le (le_cSup Sbd ⟨xs, le_trans (le_cSup Sbd ha) (le_of_lt cx), xb⟩) cx
end

/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `a ≤ x < y ≤ b`, `x ∈ s`, the set `s ∩ (x, y]`
is not empty, then `[a, b] ⊆ s`. -/
lemma is_closed.Icc_subset_of_forall_exists_gt {a b : α} {s : set α} (hs : is_closed (s ∩ Icc a b))
  (ha : a ∈ s) (hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x,  (s ∩ Ioc x y).nonempty) :
  Icc a b ⊆ s :=
begin
  assume y hy,
  have : is_closed (s ∩ Icc a y),
  { suffices : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y,
    { rw this, exact is_closed_inter hs is_closed_Icc },
    rw [inter_assoc],
    congr,
    exact (inter_eq_self_of_subset_right $ Icc_subset_Icc_right hy.2).symm },
  exact is_closed.mem_of_ge_of_forall_exists_gt this ha hy.1
    (λ x hx, hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2)
end

section densely_ordered

variables [densely_ordered α] {a b : α}

/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `x ∈ s ∩ [a, b)` the set `s` includes some open
neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`. -/
lemma is_closed.Icc_subset_of_forall_mem_nhds_within {a b : α} {s : set α}
  (hs : is_closed (s ∩ Icc a b)) (ha : a ∈ s)
  (hgt : ∀ x ∈ s ∩ Ico a b, s ∈ nhds_within x (Ioi x)) :
  Icc a b ⊆ s :=
begin
  apply hs.Icc_subset_of_forall_exists_gt ha,
  rintros x ⟨hxs, hxab⟩ y hyxb,
  have : s ∩ Ioc x y ∈ nhds_within x (Ioi x),
    from inter_mem_sets (hgt x ⟨hxs, hxab⟩) (Ioc_mem_nhds_within_Ioi ⟨le_refl _, hyxb⟩),
  exact nonempty_of_mem_sets (nhds_within_Ioi_self_ne_bot' hxab.2) this
end

/-- A closed interval is connected. -/
lemma is_connected_Icc : is_connected (Icc a b) :=
is_connected_closed_iff.2
begin
  rintros s t hs ht hab ⟨x, hx⟩ ⟨y, hy⟩,
  wlog hxy : x ≤ y := le_total x y using [x y s t, y x t s],
  have xyab : Icc x y ⊆ Icc a b := Icc_subset_Icc hx.1.1 hy.1.2,
  by_contradiction hst,
  suffices : Icc x y ⊆ s,
    from hst ⟨y, xyab $ right_mem_Icc.2 hxy, this $ right_mem_Icc.2 hxy, hy.2⟩,
  apply (is_closed_inter hs is_closed_Icc).Icc_subset_of_forall_mem_nhds_within hx.2,
  rintros z ⟨zs, hz⟩,
  have zt : z ∈ -t, from λ zt, hst ⟨z, xyab $ Ico_subset_Icc_self hz, zs, zt⟩,
  have : -t ∩ Ioc z y ∈ nhds_within z (Ioi z),
  { rw [← nhds_within_Ioc_eq_nhds_within_Ioi hz.2],
    exact mem_nhds_within.2 ⟨-t, ht, zt, subset.refl _⟩},
  apply mem_sets_of_superset this,
  have : Ioc z y ⊆ s ∪ t, from λ w hw, hab (xyab ⟨le_trans hz.1 (le_of_lt hw.1), hw.2⟩),
  exact λ w ⟨wt, wzy⟩, (this wzy).elim id (λ h, (wt h).elim)
end

lemma is_connected_iff_forall_Icc_subset {s : set α} :
  is_connected s ↔ ∀ x y ∈ s, x ≤ y → Icc x y ⊆ s :=
⟨λ h x y hx hy hxy, h.forall_Icc_subset hx hy, λ h, is_connected_of_forall_pair $ λ x y hx hy,
  ⟨Icc (min x y) (max x y), h (min x y) (max x y)
    ((min_choice x y).elim (λ h', by rwa h') (λ h', by rwa h'))
    ((max_choice x y).elim (λ h', by rwa h') (λ h', by rwa h')) min_le_max,
    ⟨min_le_left x y, le_max_left x y⟩, ⟨min_le_right x y, le_max_right x y⟩, is_connected_Icc⟩⟩

lemma is_connected_Ici : is_connected (Ici a) :=
is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ici_iff hxy).2 hx

lemma is_connected_Iic : is_connected (Iic a) :=
is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Iic_iff hxy).2 hy

lemma is_connected_Iio : is_connected (Iio a) :=
is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Iio_iff hxy).2 hy

lemma is_connected_Ioi : is_connected (Ioi a) :=
is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioi_iff hxy).2 hx

lemma is_connected_Ioo : is_connected (Ioo a b) :=
is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioo_iff hxy).2 ⟨hx.1, hy.2⟩

lemma is_connected_Ioc : is_connected (Ioc a b) :=
is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioc_iff hxy).2 ⟨hx.1, hy.2⟩

lemma is_connected_Ico : is_connected (Ico a b) :=
is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ico_iff hxy).2 ⟨hx.1, hy.2⟩

@[priority 100]
instance ordered_connected_space : connected_space α :=
⟨is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, subset_univ _⟩

/--Intermediate Value Theorem for continuous functions on closed intervals, case `f a ≤ t ≤ f b`.-/
lemma intermediate_value_Icc {a b : α} (hab : a ≤ b) {f : α → β} (hf : continuous_on f (Icc a b)) :
  Icc (f a) (f b) ⊆ f '' (Icc a b) :=
is_connected_Icc.intermediate_value (left_mem_Icc.2 hab) (right_mem_Icc.2 hab) hf

/--Intermediate Value Theorem for continuous functions on closed intervals, case `f a ≥ t ≥ f b`.-/
lemma intermediate_value_Icc' {a b : α} (hab : a ≤ b) {f : α → β} (hf : continuous_on f (Icc a b)) :
  Icc (f b) (f a) ⊆ f '' (Icc a b) :=
is_connected_Icc.intermediate_value (right_mem_Icc.2 hab) (left_mem_Icc.2 hab) hf

end densely_ordered

/-- The extreme value theorem: a continuous function realizes its minimum on a compact set -/
lemma compact.exists_forall_le {α : Type u} [topological_space α]
  {s : set α} (hs : compact s) (ne_s : s.nonempty) {f : α → β} (hf : continuous_on f s) :
  ∃x∈s, ∀y∈s, f x ≤ f y :=
begin
  have C : compact (f '' s) := hs.image_of_continuous_on hf,
  haveI := has_Inf_to_nonempty β,
  have B : bdd_below (f '' s) := bdd_below_of_compact C,
  have : Inf (f '' s) ∈ f '' s :=
    cInf_mem_of_is_closed (ne_s.image _) (closed_of_compact _ C) B,
  rcases (mem_image _ _ _).1 this with ⟨x, xs, hx⟩,
  exact ⟨x, xs, λ y hy, hx.symm ▸ cInf_le B ⟨_, hy, rfl⟩⟩
end

/-- The extreme value theorem: a continuous function realizes its maximum on a compact set -/
lemma compact.exists_forall_ge {α : Type u} [topological_space α]:
  ∀ {s : set α}, compact s → s.nonempty → ∀ {f : α → β}, continuous_on f s →
  ∃x∈s, ∀y∈s, f y ≤ f x :=
@compact.exists_forall_le (order_dual β) _ _ _ _ _

end conditionally_complete_linear_order


section liminf_limsup

section order_closed_topology
variables [semilattice_sup α] [topological_space α] [order_topology α]

lemma is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤) :=
match forall_le_or_exists_lt_sup a with
| or.inl h := ⟨a, eventually_of_forall _ h⟩
| or.inr ⟨b, hb⟩ := ⟨b, ge_mem_nhds hb⟩
end

lemma is_bounded_under_le_of_tendsto {f : filter β} {u : β → α} {a : α}
  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≤) u :=
is_bounded_of_le h (is_bounded_le_nhds a)

@[nolint] -- see Note [nolint_ge]
lemma is_cobounded_ge_nhds (a : α) : (𝓝 a).is_cobounded (≥) :=
is_cobounded_of_is_bounded nhds_ne_bot (is_bounded_le_nhds a)

@[nolint] -- see Note [nolint_ge]
lemma is_cobounded_under_ge_of_tendsto {f : filter β} {u : β → α} {a : α}
  (hf : f ≠ ⊥) (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≥) u :=
is_cobounded_of_is_bounded (map_ne_bot hf) (is_bounded_under_le_of_tendsto h)

end order_closed_topology

section order_closed_topology
variables [semilattice_inf α] [topological_space α] [order_topology α]

@[nolint] -- see Note [nolint_ge]
lemma is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥) :=
match forall_le_or_exists_lt_inf a with
| or.inl h := ⟨a, eventually_of_forall _ h⟩
| or.inr ⟨b, hb⟩ := ⟨b, le_mem_nhds hb⟩
end

@[nolint] -- see Note [nolint_ge]
lemma is_bounded_under_ge_of_tendsto {f : filter β} {u : β → α} {a : α}
  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≥) u :=
is_bounded_of_le h (is_bounded_ge_nhds a)

lemma is_cobounded_le_nhds (a : α) : (𝓝 a).is_cobounded (≤) :=
is_cobounded_of_is_bounded nhds_ne_bot (is_bounded_ge_nhds a)

lemma is_cobounded_under_le_of_tendsto {f : filter β} {u : β → α} {a : α}
  (hf : f ≠ ⊥) (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≤) u :=
is_cobounded_of_is_bounded (map_ne_bot hf) (is_bounded_under_ge_of_tendsto h)

end order_closed_topology

section conditionally_complete_linear_order
variables [conditionally_complete_linear_order α]

theorem lt_mem_sets_of_Limsup_lt {f : filter α} {b} (h : f.is_bounded (≤)) (l : f.Limsup < b) :
  ∀ᶠ a in f, a < b :=
let ⟨c, (h : ∀ᶠ a in f, a ≤ c), hcb⟩ := exists_lt_of_cInf_lt h l in
mem_sets_of_superset h $ assume a hac, lt_of_le_of_lt hac hcb

@[nolint] -- see Note [nolint_ge]
theorem gt_mem_sets_of_Liminf_gt : ∀ {f : filter α} {b}, f.is_bounded (≥) → f.Liminf > b →
  ∀ᶠ a in f, a > b :=
@lt_mem_sets_of_Limsup_lt (order_dual α) _

variables [topological_space α] [order_topology α]

/-- If the liminf and the limsup of a filter coincide, then this filter converges to
their common value, at least if the filter is eventually bounded above and below. -/
@[nolint] -- see Note [nolint_ge]
theorem le_nhds_of_Limsup_eq_Liminf {f : filter α} {a : α}
  (hl : f.is_bounded (≤)) (hg : f.is_bounded (≥)) (hs : f.Limsup = a) (hi : f.Liminf = a) :
  f ≤ 𝓝 a :=
tendsto_order.2 $ and.intro
  (assume b hb, gt_mem_sets_of_Liminf_gt hg $ hi.symm ▸ hb)
  (assume b hb, lt_mem_sets_of_Limsup_lt hl $ hs.symm ▸ hb)

theorem Limsup_nhds (a : α) : Limsup (𝓝 a) = a :=
cInf_intro (is_bounded_le_nhds a)
  (assume a' (h : {n : α | n ≤ a'} ∈ 𝓝 a), show a ≤ a', from @mem_of_nhds α _ a _ h)
  (assume b (hba : a < b), show ∃c (h : {n : α | n ≤ c} ∈ 𝓝 a), c < b, from
    match dense_or_discrete a b with
    | or.inl ⟨c, hac, hcb⟩ := ⟨c, ge_mem_nhds hac, hcb⟩
    | or.inr ⟨_, h⟩        := ⟨a, (𝓝 a).sets_of_superset (gt_mem_nhds hba) h, hba⟩
    end)

theorem Liminf_nhds : ∀ (a : α), Liminf (𝓝 a) = a :=
@Limsup_nhds (order_dual α) _ _ _

/-- If a filter is converging, its limsup coincides with its limit. -/
theorem Liminf_eq_of_le_nhds {f : filter α} {a : α} (hf : f ≠ ⊥) (h : f ≤ 𝓝 a) : f.Liminf = a :=
have hb_ge : is_bounded (≥) f, from is_bounded_of_le h (is_bounded_ge_nhds a),
have hb_le : is_bounded (≤) f, from is_bounded_of_le h (is_bounded_le_nhds a),
le_antisymm
  (calc f.Liminf ≤ f.Limsup : Liminf_le_Limsup hf hb_le hb_ge
    ... ≤ (𝓝 a).Limsup :
      Limsup_le_Limsup_of_le h (is_cobounded_of_is_bounded hf hb_ge) (is_bounded_le_nhds a)
    ... = a : Limsup_nhds a)
  (calc a = (𝓝 a).Liminf : (Liminf_nhds a).symm
    ... ≤ f.Liminf :
      Liminf_le_Liminf_of_le h (is_bounded_ge_nhds a) (is_cobounded_of_is_bounded hf hb_le))

/-- If a filter is converging, its liminf coincides with its limit. -/
theorem Limsup_eq_of_le_nhds : ∀ {f : filter α} {a : α}, f ≠ ⊥ → f ≤ 𝓝 a → f.Limsup = a :=
@Liminf_eq_of_le_nhds (order_dual α) _ _ _

end conditionally_complete_linear_order

section complete_linear_order
variables [complete_linear_order α] [topological_space α] [order_topology α]
-- In complete_linear_order, the above theorems take a simpler form

/-- If the liminf and the limsup of a function coincide, then the limit of the function
exists and has the same value -/
theorem tendsto_of_liminf_eq_limsup {f : filter β} {u : β → α} {a : α}
  (h : liminf f u = a ∧ limsup f u = a) : tendsto u f (𝓝 a) :=
  le_nhds_of_Limsup_eq_Liminf is_bounded_le_of_top is_bounded_ge_of_bot h.2 h.1

/-- If a function has a limit, then its limsup coincides with its limit-/
theorem limsup_eq_of_tendsto {f : filter β} {u : β → α} {a : α} (hf : f ≠ ⊥)
  (h : tendsto u f (𝓝 a)) : limsup f u = a :=
  Limsup_eq_of_le_nhds (map_ne_bot hf) h

/-- If a function has a limit, then its liminf coincides with its limit-/
theorem liminf_eq_of_tendsto {f : filter β} {u : β → α} {a : α} (hf : f ≠ ⊥)
  (h : tendsto u f (𝓝 a)) : liminf f u = a :=
  Liminf_eq_of_le_nhds (map_ne_bot hf) h

end complete_linear_order

end liminf_limsup

end order_topology

@[nolint] -- see Note [nolint_ge]
lemma order_topology_of_nhds_abs
  {α : Type*} [decidable_linear_ordered_comm_group α] [topological_space α]
  (h_nhds : ∀a:α, 𝓝 a = (⨅r>0, principal {b | abs (a - b) < r})) : order_topology α :=
order_topology.mk $ eq_of_nhds_eq_nhds $ assume a:α, le_antisymm_iff.mpr
begin
  simp [infi_and, topological_space.nhds_generate_from,
        h_nhds, le_infi_iff, -le_principal_iff, and_comm],
  refine ⟨λ s ha b hs, _, λ r hr, _⟩,
  { rcases hs with rfl | rfl,
    { refine infi_le_of_le (a - b)
        (infi_le_of_le (lt_sub_left_of_add_lt $ by simpa using ha) $
          principal_mono.mpr $ assume c (hc : abs (a - c) < a - b), _),
      have : a - c < a - b := lt_of_le_of_lt (le_abs_self _) hc,
      exact lt_of_neg_lt_neg (lt_of_add_lt_add_left this) },
    { refine infi_le_of_le (b - a)
        (infi_le_of_le (lt_sub_left_of_add_lt $ by simpa using ha) $
          principal_mono.mpr $ assume c (hc : abs (a - c) < b - a), _),
      have : abs (c - a) < b - a, {rw abs_sub; simpa using hc},
      have : c - a < b - a := lt_of_le_of_lt (le_abs_self _) this,
      exact lt_of_add_lt_add_right this } },
  { have h : {b | abs (a + -b) < r} = {b | a - r < b} ∩ {b | b < a + r},
      from set.ext (assume b,
        by simp [abs_lt, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm,
          sub_lt, lt_sub_iff_add_lt, and_comm, sub_lt_iff_lt_add']),
    rw [h, ← inf_principal],
    apply le_inf _ _,
    { exact infi_le_of_le {b : α | a - r < b} (infi_le_of_le (sub_lt_self a hr) $
        infi_le_of_le (a - r) $ infi_le _ (or.inl rfl)) },
    { exact infi_le_of_le {b : α | b < a + r} (infi_le_of_le (lt_add_of_pos_right _ hr) $
        infi_le_of_le (a + r) $ infi_le _ (or.inr rfl)) } }
end

lemma tendsto_at_top_supr_nat [topological_space α] [complete_linear_order α] [order_topology α]
  (f : ℕ → α) (hf : monotone f) : tendsto f at_top (𝓝 (⨆i, f i)) :=
tendsto_order.2 $ and.intro
  (assume a ha, let ⟨n, hn⟩ := lt_supr_iff.1 ha in
    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_lt_of_le hn (hf hi)⟩)
  (assume a ha, univ_mem_sets' (assume n, lt_of_le_of_lt (le_supr _ n) ha))

lemma tendsto_at_top_infi_nat [topological_space α] [complete_linear_order α] [order_topology α]
  (f : ℕ → α) (hf : ∀{n m}, n ≤ m → f m ≤ f n) : tendsto f at_top (𝓝 (⨅i, f i)) :=
@tendsto_at_top_supr_nat (order_dual α) _ _ _ _ @hf

lemma supr_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [order_topology α]
  {f : ℕ → α} {a : α} (hf : monotone f) : tendsto f at_top (𝓝 a) → supr f = a :=
tendsto_nhds_unique at_top_ne_bot (tendsto_at_top_supr_nat f hf)

lemma infi_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [order_topology α]
  {f : ℕ → α} {a : α} (hf : ∀n m, n ≤ m → f m ≤ f n) : tendsto f at_top (𝓝 a) → infi f = a :=
tendsto_nhds_unique at_top_ne_bot (tendsto_at_top_infi_nat f hf)

lemma tendsto_abs_at_top_at_top [decidable_linear_ordered_comm_group α] : tendsto (abs : α → α) at_top at_top :=
tendsto_at_top_mono _ (λ n, le_abs_self _) tendsto_id

local notation `|` x `|` := abs x

@[nolint] -- see Note [nolint_ge]
lemma decidable_linear_ordered_comm_group.tendsto_nhds
  [decidable_linear_ordered_comm_group α] [topological_space α] [order_topology α] {β : Type*}
  (f : β → α) (x : filter β) (a : α) :
  filter.tendsto f x (nhds a) ↔ ∀ ε > (0 : α), ∀ᶠ b in x, |f b - a| < ε :=
begin
  rw (show _, from @tendsto_order α), -- does not work without `show` for some reason
  split,
  { rintros ⟨hyp_lt_a, hyp_gt_a⟩ ε ε_pos,
    suffices : {b : β | f b - a < ε ∧ a - f b < ε} ∈ x, by simpa only [abs_sub_lt_iff],
    have set1 : {b : β | a - f b < ε} ∈ x,
    { have : {b : β | a - ε < f b} ∈ x, from hyp_lt_a (a - ε) (sub_lt_self a ε_pos),
      have : ∀ b, a - f b < ε ↔ a - ε < f b, by { intro _, exact sub_lt },
      simpa only [this] },
    have set2 : {b : β | f b - a < ε} ∈ x,
    { have : {b : β | a + ε > f b} ∈ x, from hyp_gt_a (a + ε) (lt_add_of_pos_right a ε_pos),
      have : ∀ b, f b - a < ε ↔ a + ε > f b, by { intro _, exact sub_lt_iff_lt_add' },
      simpa only [this] },
    exact (x.inter_sets set2 set1) },
  { assume hyp_ε_pos,
    split,
    { assume a' a'_lt_a,
      let ε := a - a',
      have : {b : β | |f b - a| < ε} ∈ x, from hyp_ε_pos ε (sub_pos.elim_right a'_lt_a),
      have : {b : β | f b - a < ε ∧ a - f b < ε} ∈ x, by simpa only [abs_sub_lt_iff] using this,
      have : {b : β | a - f b < ε} ∈ x, from x.sets_of_superset this (set.inter_subset_right _ _),
      have : ∀ b, a' < f b ↔ a - f b < ε, by {intro b, rw [sub_lt, sub_sub_self] },
      simpa only [this] },
    { assume a' a'_gt_a,
      let ε := a' - a,
      have : {b : β | |f b - a| < ε} ∈ x, from hyp_ε_pos ε (sub_pos.elim_right a'_gt_a),
      have : {b : β | f b - a < ε ∧ a - f b < ε} ∈ x, by simpa only [abs_sub_lt_iff] using this,
      have : {b : β | f b - a < ε} ∈ x, from x.sets_of_superset this (set.inter_subset_left _ _),
      have : ∀ b, f b < a' ↔ f b - a < ε, by { intro b, simp [lt_sub_iff_add_lt] },
      simpa only [this] }}
end