import data.set.intervals.pi

import data.set.pointwise.interval

import order.filter.interval

import topology.support

import topology.algebra.order.left_right

open set filter topological_space

open function

open order_dual (to_dual of_dual)

open_locale topology classical filter

universes u v w

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

class order_closed_topology (α : Type*) [topological_space α] [preorder α] : Prop :=

(is_closed_le' : is_closed {p : α × α | p.1 ≤ p.2})

instance [topological_space α] [h : first_countable_topology α] : first_countable_topology αᵒᵈ := h

instance [topological_space α] [h : second_countable_topology α] : second_countable_topology αᵒᵈ :=

h

lemma dense.order_dual [topological_space α] {s : set α} (hs : dense s) :

dense (order_dual.of_dual ⁻¹' s) := hs

section order_closed_topology

section preorder

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

include t

namespace subtype

instance {p : α → Prop} : order_closed_topology (subtype p) :=

have this : continuous (λ (p : (subtype p) × (subtype p)), ((p.fst : α), (p.snd : α))) :=

(continuous_subtype_coe.comp continuous_fst).prod_mk

(continuous_subtype_coe.comp continuous_snd),

order_closed_topology.mk (t.is_closed_le'.preimage this)

end subtype

lemma is_closed_le_prod : is_closed {p : α × α | p.1 ≤ p.2} :=

t.is_closed_le'

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) _ is_closed_le_prod

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_closed_topology.is_closed_le' α _ _ _).preimage continuous_swap⟩

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

is_closed.inter is_closed_Ici is_closed_Iic

@[simp] lemma closure_Icc (a b : α) : closure (Icc a b) = Icc a b :=

is_closed_Icc.closure_eq

@[simp] lemma closure_Iic (a : α) : closure (Iic a) = Iic a :=

is_closed_Iic.closure_eq

@[simp] lemma closure_Ici (a : α) : closure (Ici a) = Ici a :=

is_closed_Ici.closure_eq

lemma le_of_tendsto_of_tendsto {f g : β → α} {b : filter β} {a₁ a₂ : α} [ne_bot b]

(hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) (h : f ≤ᶠ[b] g) :

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 t.is_closed_le'.mem_of_tendsto this h

alias le_of_tendsto_of_tendsto ← tendsto_le_of_eventually_le

lemma le_of_tendsto_of_tendsto' {f g : β → α} {b : filter β} {a₁ a₂ : α} [ne_bot b]

(hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) :

a₁ ≤ a₂ :=

le_of_tendsto_of_tendsto hf hg (eventually_of_forall h)

lemma le_of_tendsto {f : β → α} {a b : α} {x : filter β}

[ne_bot x] (lim : tendsto f x (𝓝 a)) (h : ∀ᶠ c in x, f c ≤ b) : a ≤ b :=

le_of_tendsto_of_tendsto lim tendsto_const_nhds h

lemma le_of_tendsto' {f : β → α} {a b : α} {x : filter β}

[ne_bot x] (lim : tendsto f x (𝓝 a)) (h : ∀ c, f c ≤ b) : a ≤ b :=

le_of_tendsto lim (eventually_of_forall h)

lemma ge_of_tendsto {f : β → α} {a b : α} {x : filter β} [ne_bot x]

(lim : tendsto f x (𝓝 a)) (h : ∀ᶠ c in x, b ≤ f c) : b ≤ a :=

le_of_tendsto_of_tendsto tendsto_const_nhds lim h

lemma ge_of_tendsto' {f : β → α} {a b : α} {x : filter β} [ne_bot x]

(lim : tendsto f x (𝓝 a)) (h : ∀ c, b ≤ f c) : b ≤ a :=

ge_of_tendsto lim (eventually_of_forall h)

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} :=

(is_closed_le hf hg).closure_eq

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} :=

closure_minimal (λ x, le_of_lt) $ is_closed_le hf hg

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 :=

show (f x, g x) ∈ {p : α × α | p.1 ≤ p.2},

from order_closed_topology.is_closed_le'.closure_subset ((hf.prod hg).mem_closure hx h)

lemma is_closed.is_closed_le [topological_space β] {f g : β → α} {s : set β} (hs : is_closed s)

(hf : continuous_on f s) (hg : continuous_on g s) :

is_closed {x ∈ s | f x ≤ g x} :=

(hf.prod hg).preimage_closed_of_closed hs order_closed_topology.is_closed_le'

lemma le_on_closure [topological_space β] {f g : β → α} {s : set β} (h : ∀ x ∈ s, f x ≤ g x)

(hf : continuous_on f (closure s)) (hg : continuous_on g (closure s)) ⦃x⦄ (hx : x ∈ closure s) :

f x ≤ g x :=

have s ⊆ {y ∈ closure s | f y ≤ g y}, from λ y hy, ⟨subset_closure hy, h y hy⟩,

(closure_minimal this (is_closed_closure.is_closed_le hf hg) hx).2

lemma is_closed.epigraph [topological_space β] {f : β → α} {s : set β}

(hs : is_closed s) (hf : continuous_on f s) :

is_closed {p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2} :=

(hs.preimage continuous_fst).is_closed_le (hf.comp continuous_on_fst subset.rfl) continuous_on_snd

lemma is_closed.hypograph [topological_space β] {f : β → α} {s : set β}

(hs : is_closed s) (hf : continuous_on f s) :

is_closed {p : β × α | p.1 ∈ s ∧ p.2 ≤ f p.1} :=

(hs.preimage continuous_fst).is_closed_le continuous_on_snd (hf.comp continuous_on_fst subset.rfl)

omit t

lemma nhds_within_Ici_ne_bot {a b : α} (H₂ : a ≤ b) :

ne_bot (𝓝[Ici a] b) :=

nhds_within_ne_bot_of_mem H₂

@[instance] lemma nhds_within_Ici_self_ne_bot (a : α) :

ne_bot (𝓝[≥] a) :=

nhds_within_Ici_ne_bot (le_refl a)

lemma nhds_within_Iic_ne_bot {a b : α} (H : a ≤ b) :

ne_bot (𝓝[Iic b] a) :=

nhds_within_ne_bot_of_mem H

@[instance] lemma nhds_within_Iic_self_ne_bot (a : α) :

ne_bot (𝓝[≤] a) :=

nhds_within_Iic_ne_bot (le_refl a)

end preorder

section partial_order

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

include t

@[priority 90] -- see Note [lower instance priority]

instance order_closed_topology.to_t2_space : t2_space α :=

t2_iff_is_closed_diagonal.2 $ by simpa only [diagonal, le_antisymm_iff] using

t.is_closed_le'.inter (is_closed_le continuous_snd continuous_fst)

end partial_order

section linear_order

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

lemma is_open_lt_prod : is_open {p : α × α | p.1 < p.2} :=

by { simp_rw [← is_closed_compl_iff, compl_set_of, not_lt],

exact is_closed_le continuous_snd continuous_fst }

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).is_open_compl

variables {a b : α}

lemma is_open_Iio : is_open (Iio a) :=

is_open_lt continuous_id continuous_const

lemma is_open_Ioi : is_open (Ioi a) :=

is_open_lt continuous_const continuous_id

lemma is_open_Ioo : is_open (Ioo a b) :=

is_open.inter is_open_Ioi is_open_Iio

@[simp] lemma interior_Ioi : interior (Ioi a) = Ioi a :=

is_open_Ioi.interior_eq

@[simp] lemma interior_Iio : interior (Iio a) = Iio a :=

is_open_Iio.interior_eq

@[simp] lemma interior_Ioo : interior (Ioo a b) = Ioo a b :=

is_open_Ioo.interior_eq

lemma Ioo_subset_closure_interior : Ioo a b ⊆ closure (interior (Ioo a b)) :=

by simp only [interior_Ioo, subset_closure]

lemma Iio_mem_nhds {a b : α} (h : a < b) : Iio b ∈ 𝓝 a :=

is_open.mem_nhds is_open_Iio h

lemma Ioi_mem_nhds {a b : α} (h : a < b) : Ioi a ∈ 𝓝 b :=

is_open.mem_nhds is_open_Ioi h

lemma Iic_mem_nhds {a b : α} (h : a < b) : Iic b ∈ 𝓝 a :=

mem_of_superset (Iio_mem_nhds h) Iio_subset_Iic_self

lemma Ici_mem_nhds {a b : α} (h : a < b) : Ici a ∈ 𝓝 b :=

mem_of_superset (Ioi_mem_nhds h) Ioi_subset_Ici_self

lemma Ioo_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioo a b ∈ 𝓝 x :=

is_open.mem_nhds is_open_Ioo ⟨ha, hb⟩

lemma Ioc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioc a b ∈ 𝓝 x :=

mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ioc_self

lemma Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x :=

mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ico_self

lemma Icc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Icc a b ∈ 𝓝 x :=

mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self

lemma eventually_lt_of_tendsto_lt {l : filter γ} {f : γ → α} {u v : α} (hv : v < u)

(h : filter.tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a < u :=

tendsto_nhds.1 h (< u) is_open_Iio hv

lemma eventually_gt_of_tendsto_gt {l : filter γ} {f : γ → α} {u v : α} (hv : u < v)

(h : filter.tendsto f l (𝓝 v)) : ∀ᶠ a in l, u < f a :=

tendsto_nhds.1 h (> u) is_open_Ioi hv

lemma eventually_le_of_tendsto_lt {l : filter γ} {f : γ → α} {u v : α} (hv : v < u)

(h : tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a ≤ u :=

(eventually_lt_of_tendsto_lt hv h).mono (λ v, le_of_lt)

lemma eventually_ge_of_tendsto_gt {l : filter γ} {f : γ → α} {u v : α} (hv : u < v)

(h : tendsto f l (𝓝 v)) : ∀ᶠ a in l, u ≤ f a :=

(eventually_gt_of_tendsto_gt hv h).mono (λ v, le_of_lt)

variables [topological_space γ]

lemma Ioo_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) :

Ioo a c ∈ 𝓝[>] b :=

mem_nhds_within.2 ⟨Iio c, is_open_Iio, H.2,

by rw [inter_comm, Ioi_inter_Iio]; exact Ioo_subset_Ioo_left H.1⟩

lemma Ioc_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) :

Ioc a c ∈ 𝓝[>] b :=

mem_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 ∈ 𝓝[>] b :=

mem_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 ∈ 𝓝[>] b :=

mem_of_superset (Ioo_mem_nhds_within_Ioi H) Ioo_subset_Icc_self

@[simp] lemma nhds_within_Ioc_eq_nhds_within_Ioi {a b : α} (h : a < b) :

𝓝[Ioc a b] a = 𝓝[>] a :=

le_antisymm (nhds_within_mono _ Ioc_subset_Ioi_self) $

nhds_within_le_of_mem $ Ioc_mem_nhds_within_Ioi $ left_mem_Ico.2 h

@[simp] lemma nhds_within_Ioo_eq_nhds_within_Ioi {a b : α} (h : a < b) :

𝓝[Ioo a b] a = 𝓝[>] a :=

le_antisymm (nhds_within_mono _ Ioo_subset_Ioi_self) $

nhds_within_le_of_mem $ Ioo_mem_nhds_within_Ioi $ left_mem_Ico.2 h

lemma continuous_within_at_Ioc_iff_Ioi [topological_space β] {a b : α} {f : α → β} (h : a < b) :

continuous_within_at f (Ioc a b) a ↔ continuous_within_at f (Ioi a) a :=

by simp only [continuous_within_at, nhds_within_Ioc_eq_nhds_within_Ioi h]

lemma continuous_within_at_Ioo_iff_Ioi [topological_space β] {a b : α} {f : α → β} (h : a < b) :

continuous_within_at f (Ioo a b) a ↔ continuous_within_at f (Ioi a) a :=

by simp only [continuous_within_at, nhds_within_Ioo_eq_nhds_within_Ioi h]

lemma Ioo_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) :

Ioo a c ∈ 𝓝[<] b :=

by simpa only [dual_Ioo] using Ioo_mem_nhds_within_Ioi

(show to_dual b ∈ Ico (to_dual c) (to_dual a), from H.symm)

lemma Ico_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) :

Ico a c ∈ 𝓝[<] b :=

mem_of_superset (Ioo_mem_nhds_within_Iio H) Ioo_subset_Ico_self

lemma Ioc_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) :

Ioc a c ∈ 𝓝[<] b :=

mem_of_superset (Ioo_mem_nhds_within_Iio H) Ioo_subset_Ioc_self

lemma Icc_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) :

Icc a c ∈ 𝓝[<] b :=

mem_of_superset (Ioo_mem_nhds_within_Iio H) Ioo_subset_Icc_self

@[simp] lemma nhds_within_Ico_eq_nhds_within_Iio {a b : α} (h : a < b) :

𝓝[Ico a b] b = 𝓝[<] b :=

by simpa only [dual_Ioc] using nhds_within_Ioc_eq_nhds_within_Ioi h.dual

@[simp] lemma nhds_within_Ioo_eq_nhds_within_Iio {a b : α} (h : a < b) :

𝓝[Ioo a b] b = 𝓝[<] b :=

by simpa only [dual_Ioo] using nhds_within_Ioo_eq_nhds_within_Ioi h.dual

@[simp] lemma continuous_within_at_Ico_iff_Iio {a b : α} {f : α → γ} (h : a < b) :

continuous_within_at f (Ico a b) b ↔ continuous_within_at f (Iio b) b :=

by simp only [continuous_within_at, nhds_within_Ico_eq_nhds_within_Iio h]

@[simp] lemma continuous_within_at_Ioo_iff_Iio {a b : α} {f : α → γ} (h : a < b) :

continuous_within_at f (Ioo a b) b ↔ continuous_within_at f (Iio b) b :=

by simp only [continuous_within_at, nhds_within_Ioo_eq_nhds_within_Iio h]

lemma Ioo_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ioo a c) :

Ioo a c ∈ 𝓝[≥] b :=

mem_nhds_within_of_mem_nhds $ is_open.mem_nhds is_open_Ioo H

lemma Ioc_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ioo a c) :

Ioc a c ∈ 𝓝[≥] b :=

mem_of_superset (Ioo_mem_nhds_within_Ici H) Ioo_subset_Ioc_self

lemma Ico_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ico a c) :

Ico a c ∈ 𝓝[≥] b :=

mem_nhds_within.2 ⟨Iio c, is_open_Iio, H.2,

by simp only [inter_comm, Ici_inter_Iio, Ico_subset_Ico_left H.1]⟩

lemma Icc_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ico a c) :

Icc a c ∈ 𝓝[≥] b :=

mem_of_superset (Ico_mem_nhds_within_Ici H) Ico_subset_Icc_self

@[simp] lemma nhds_within_Icc_eq_nhds_within_Ici {a b : α} (h : a < b) :

𝓝[Icc a b] a = 𝓝[≥] a :=

le_antisymm (nhds_within_mono _ Icc_subset_Ici_self) $

nhds_within_le_of_mem $ Icc_mem_nhds_within_Ici $ left_mem_Ico.2 h

@[simp] lemma nhds_within_Ico_eq_nhds_within_Ici {a b : α} (h : a < b) :

𝓝[Ico a b] a = 𝓝[≥] a :=

le_antisymm (nhds_within_mono _ (λ x, and.left)) $

nhds_within_le_of_mem $ Ico_mem_nhds_within_Ici $ left_mem_Ico.2 h

lemma continuous_within_at_Icc_iff_Ici [topological_space β] {a b : α} {f : α → β} (h : a < b) :

continuous_within_at f (Icc a b) a ↔ continuous_within_at f (Ici a) a :=

by simp only [continuous_within_at, nhds_within_Icc_eq_nhds_within_Ici h]

lemma continuous_within_at_Ico_iff_Ici [topological_space β] {a b : α} {f : α → β} (h : a < b) :

continuous_within_at f (Ico a b) a ↔ continuous_within_at f (Ici a) a :=

by simp only [continuous_within_at, nhds_within_Ico_eq_nhds_within_Ici h]

lemma Ioo_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioo a c) :

Ioo a c ∈ 𝓝[≤] b :=

mem_nhds_within_of_mem_nhds $ is_open.mem_nhds is_open_Ioo H

lemma Ico_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioo a c) :

Ico a c ∈ 𝓝[≤] b :=

mem_of_superset (Ioo_mem_nhds_within_Iic H) Ioo_subset_Ico_self

lemma Ioc_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioc a c) :

Ioc a c ∈ 𝓝[≤] b :=

by simpa only [dual_Ico] using Ico_mem_nhds_within_Ici

(show to_dual b ∈ Ico (to_dual c) (to_dual a), from H.symm)

lemma Icc_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioc a c) :

Icc a c ∈ 𝓝[≤] b :=

mem_of_superset (Ioc_mem_nhds_within_Iic H) Ioc_subset_Icc_self

@[simp] lemma nhds_within_Icc_eq_nhds_within_Iic {a b : α} (h : a < b) :

𝓝[Icc a b] b = 𝓝[≤] b :=

by simpa only [dual_Icc] using nhds_within_Icc_eq_nhds_within_Ici h.dual

@[simp] lemma nhds_within_Ioc_eq_nhds_within_Iic {a b : α} (h : a < b) :

𝓝[Ioc a b] b = 𝓝[≤] b :=

by simpa only [dual_Ico] using nhds_within_Ico_eq_nhds_within_Ici h.dual

lemma continuous_within_at_Icc_iff_Iic [topological_space β] {a b : α} {f : α → β} (h : a < b) :

continuous_within_at f (Icc a b) b ↔ continuous_within_at f (Iic b) b :=

by simp only [continuous_within_at, nhds_within_Icc_eq_nhds_within_Iic h]

lemma continuous_within_at_Ioc_iff_Iic [topological_space β] {a b : α} {f : α → β} (h : a < b) :

continuous_within_at f (Ioc a b) b ↔ continuous_within_at f (Iic b) b :=

by simp only [continuous_within_at, nhds_within_Ioc_eq_nhds_within_Iic h]

end linear_order

section linear_order

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

variables [topological_space β]

lemma lt_subset_interior_le (hf : continuous f) (hg : continuous g) :

{b | f b < g b} ⊆ interior {b | f b ≤ g b} :=

interior_maximal (λ p, le_of_lt) $ is_open_lt hf hg

lemma frontier_le_subset_eq (hf : continuous f) (hg : continuous g) :

frontier {b | f b ≤ g b} ⊆ {b | f b = g b} :=

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

lemma frontier_Iic_subset (a : α) : frontier (Iic a) ⊆ {a} :=

frontier_le_subset_eq (@continuous_id α _) continuous_const

lemma frontier_Ici_subset (a : α) : frontier (Ici a) ⊆ {a} := @frontier_Iic_subset αᵒᵈ _ _ _ _

lemma frontier_lt_subset_eq (hf : continuous f) (hg : continuous g) :

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_if_le [topological_space γ] [Π x, decidable (f x ≤ g x)]

{f' g' : β → γ} (hf : continuous f) (hg : continuous g)

(hf' : continuous_on f' {x | f x ≤ g x}) (hg' : continuous_on g' {x | g x ≤ f x})

(hfg : ∀ x, f x = g x → f' x = g' x) :

continuous (λ x, if f x ≤ g x then f' x else g' x) :=

refine continuous_if (λ a ha, hfg _ (frontier_le_subset_eq hf hg ha)) _ (hg'.mono _),

{ rwa [(is_closed_le hf hg).closure_eq] },

{ simp only [not_le], exact closure_lt_subset_le hg hf }

lemma continuous.if_le [topological_space γ] [Π x, decidable (f x ≤ g x)] {f' g' : β → γ}

(hf' : continuous f') (hg' : continuous g') (hf : continuous f) (hg : continuous g)

(hfg : ∀ x, f x = g x → f' x = g' x) :

continuous (λ x, if f x ≤ g x then f' x else g' x) :=

continuous_if_le hf hg hf'.continuous_on hg'.continuous_on hfg

lemma tendsto.eventually_lt {l : filter γ} {f g : γ → α} {y z : α}

(hf : tendsto f l (𝓝 y)) (hg : tendsto g l (𝓝 z)) (hyz : y < z) : ∀ᶠ x in l, f x < g x :=

by_cases h : y ⋖ z,

{ filter_upwards [hf (Iio_mem_nhds hyz), hg (Ioi_mem_nhds hyz)],

rw [h.Iio_eq],

exact λ x hfx hgx, lt_of_le_of_lt hfx hgx },

{ obtain ⟨w, hyw, hwz⟩ := (not_covby_iff hyz).mp h,

filter_upwards [hf (Iio_mem_nhds hyw), hg (Ioi_mem_nhds hwz)],

exact λ x, lt_trans },

lemma continuous_at.eventually_lt {x₀ : β} (hf : continuous_at f x₀)

(hg : continuous_at g x₀) (hfg : f x₀ < g x₀) : ∀ᶠ x in 𝓝 x₀, f x < g x :=

tendsto.eventually_lt hf hg hfg

@[continuity] lemma continuous.min (hf : continuous f) (hg : continuous g) :

continuous (λb, min (f b) (g b)) :=

by { simp only [min_def], exact hf.if_le hg hf hg (λ x, id) }

@[continuity] lemma continuous.max (hf : continuous f) (hg : continuous g) :

continuous (λb, max (f b) (g b)) :=

@continuous.min αᵒᵈ _ _ _ _ _ _ _ hf hg

lemma continuous_min : continuous (λ p : α × α, min p.1 p.2) := continuous_fst.min continuous_snd

lemma continuous_max : continuous (λ p : α × α, max p.1 p.2) := continuous_fst.max continuous_snd

lemma filter.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₂)) :=

(continuous_max.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg)

lemma filter.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₂)) :=

(continuous_min.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg)

lemma filter.tendsto.max_right {l : filter β} {a : α} (h : tendsto f l (𝓝 a)) :

tendsto (λ i, max a (f i)) l (𝓝 a) :=

by { convert ((continuous_max.comp (@continuous.prod.mk α α _ _ a)).tendsto a).comp h, simp, }

lemma filter.tendsto.max_left {l : filter β} {a : α} (h : tendsto f l (𝓝 a)) :

tendsto (λ i, max (f i) a) l (𝓝 a) :=

by { simp_rw max_comm _ a, exact h.max_right, }

lemma filter.tendsto_nhds_max_right {l : filter β} {a : α} (h : tendsto f l (𝓝[>] a)) :

tendsto (λ i, max a (f i)) l (𝓝[>] a) :=

obtain ⟨h₁ : tendsto f l (𝓝 a), h₂ : ∀ᶠ i in l, f i ∈ Ioi a⟩ := tendsto_nhds_within_iff.mp h,

exact tendsto_nhds_within_iff.mpr ⟨h₁.max_right, h₂.mono $ λ i hi, lt_max_of_lt_right hi⟩,

lemma filter.tendsto_nhds_max_left {l : filter β} {a : α} (h : tendsto f l (𝓝[>] a)) :

tendsto (λ i, max (f i) a) l (𝓝[>] a) :=

by { simp_rw max_comm _ a, exact filter.tendsto_nhds_max_right h, }

lemma filter.tendsto.min_right {l : filter β} {a : α} (h : tendsto f l (𝓝 a)) :

tendsto (λ i, min a (f i)) l (𝓝 a) :=

@filter.tendsto.max_right αᵒᵈ β _ _ _ f l a h

lemma filter.tendsto.min_left {l : filter β} {a : α} (h : tendsto f l (𝓝 a)) :

tendsto (λ i, min (f i) a) l (𝓝 a) :=

@filter.tendsto.max_left αᵒᵈ β _ _ _ f l a h

lemma filter.tendsto_nhds_min_right {l : filter β} {a : α} (h : tendsto f l (𝓝[<] a)) :

tendsto (λ i, min a (f i)) l (𝓝[<] a) :=

@filter.tendsto_nhds_max_right αᵒᵈ β _ _ _ f l a h

lemma filter.tendsto_nhds_min_left {l : filter β} {a : α} (h : tendsto f l (𝓝[<] a)) :

tendsto (λ i, min (f i) a) l (𝓝[<] a) :=

@filter.tendsto_nhds_max_left αᵒᵈ β _ _ _ f l a h

lemma dense.exists_lt [no_min_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, y < x :=

hs.exists_mem_open is_open_Iio (exists_lt x)

lemma dense.exists_gt [no_max_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, x < y :=

hs.order_dual.exists_lt x

lemma dense.exists_le [no_min_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, y ≤ x :=

(hs.exists_lt x).imp $ λ y hy, ⟨hy.fst, hy.snd.le⟩

lemma dense.exists_ge [no_max_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, x ≤ y :=

hs.order_dual.exists_le x

lemma dense.exists_le' {s : set α} (hs : dense s) (hbot : ∀ x, is_bot x → x ∈ s) (x : α) :

∃ y ∈ s, y ≤ x :=

by_cases hx : is_bot x,

{ exact ⟨x, hbot x hx, le_rfl⟩ },

{ simp only [is_bot, not_forall, not_le] at hx,

rcases hs.exists_mem_open is_open_Iio hx with ⟨y, hys, hy : y < x⟩,

exact ⟨y, hys, hy.le⟩ }

lemma dense.exists_ge' {s : set α} (hs : dense s) (htop : ∀ x, is_top x → x ∈ s) (x : α) :

∃ y ∈ s, x ≤ y :=

hs.order_dual.exists_le' htop x

lemma dense.exists_between [densely_ordered α] {s : set α} (hs : dense s) {x y : α} (h : x < y) :

∃ z ∈ s, z ∈ Ioo x y :=

hs.exists_mem_open is_open_Ioo (nonempty_Ioo.2 h)

end linear_order

end order_closed_topology

instance [preorder α] [topological_space α] [order_closed_topology α]

[preorder β] [topological_space β] [order_closed_topology β] :

order_closed_topology (α × β) :=

⟨(is_closed_le (continuous_fst.comp continuous_fst) (continuous_fst.comp continuous_snd)).inter

(is_closed_le (continuous_snd.comp continuous_fst) (continuous_snd.comp continuous_snd))⟩

instance {ι : Type*} {α : ι → Type*} [Π i, preorder (α i)] [Π i, topological_space (α i)]

[Π i, order_closed_topology (α i)] : order_closed_topology (Π i, α i) :=

constructor,

simp only [pi.le_def, set_of_forall],

exact is_closed_Inter (λ i, is_closed_le ((continuous_apply i).comp continuous_fst)

((continuous_apply i).comp continuous_snd))

instance pi.order_closed_topology' [preorder β] [topological_space β]

[order_closed_topology β] : order_closed_topology (α → β) :=

pi.order_closed_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})

def preorder.topology (α : Type*) [preorder α] : topological_space α :=

generate_from {s : set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α | b < a}}

section order_topology

section preorder

variables [topological_space α] [preorder α] [t : order_topology α]

include t

instance : order_topology αᵒᵈ :=

⟨by convert @order_topology.topology_eq_generate_intervals α _ _ _;

conv in (_ ∨ _) { rw or.comm }; refl⟩

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 :=

is_open.mem_nhds (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 :=

is_open.mem_nhds (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, 𝓟 (Ioi b)) ⊓ (⨅ b ∈ Ioi a, 𝓟 (Iio b)) :=

by rw [t.topology_eq_generate_intervals, nhds_generate_from];

from le_antisymm

(le_inf

(le_infi₂ $ assume b hb, infi_le_of_le {c : α | b < c} $ infi_le _ ⟨hb, b, or.inl rfl⟩)

(le_infi₂ $ assume b 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_of_left_le $ infi_le_of_le b $ infi_le _ h

| _, h, (or.inr rfl) := inf_le_of_right_le $ infi_le_of_le b $ infi_le _ h

end)

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]

instance tendsto_Icc_class_nhds (a : α) : tendsto_Ixx_class Icc (𝓝 a) (𝓝 a) :=

simp only [nhds_eq_order, infi_subtype'],

refine ((has_basis_infi_principal_finite _).inf

(has_basis_infi_principal_finite _)).tendsto_Ixx_class (λ s hs, _),

refine ((ord_connected_bInter _).inter (ord_connected_bInter _)).out; intros _ _,

exacts [ord_connected_Ioi, ord_connected_Iio]

instance tendsto_Ico_class_nhds (a : α) : tendsto_Ixx_class Ico (𝓝 a) (𝓝 a) :=

tendsto_Ixx_class_of_subset (λ _ _, Ico_subset_Icc_self)

instance tendsto_Ioc_class_nhds (a : α) : tendsto_Ixx_class Ioc (𝓝 a) (𝓝 a) :=

tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self)

instance tendsto_Ioo_class_nhds (a : α) : tendsto_Ixx_class Ioo (𝓝 a) (𝓝 a) :=

tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Icc_self)

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) :=

(hg.Icc hh).of_small_sets $ hgf.and hfh

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 : g ≤ f) (hfh : f ≤ h) :

tendsto f b (𝓝 a) :=

tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh

(eventually_of_forall hgf) (eventually_of_forall hfh)

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)) :=

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) :

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 preorder

instance tendsto_Ixx_nhds_within {α : Type*} [preorder α] [topological_space α]

(a : α) {s t : set α} {Ixx}

[tendsto_Ixx_class Ixx (𝓝 a) (𝓝 a)] [tendsto_Ixx_class Ixx (𝓟 s) (𝓟 t)]:

tendsto_Ixx_class Ixx (𝓝[s] a) (𝓝[t] a) :=

filter.tendsto_Ixx_class_inf

instance tendsto_Icc_class_nhds_pi {ι : Type*} {α : ι → Type*}

[Π i, preorder (α i)] [Π i, topological_space (α i)] [∀ i, order_topology (α i)]

(f : Π i, α i) :

tendsto_Ixx_class Icc (𝓝 f) (𝓝 f) :=

constructor,

conv in ((𝓝 f).small_sets) { rw [nhds_pi, filter.pi] },

simp only [small_sets_infi, small_sets_comap, tendsto_infi, tendsto_lift', (∘), mem_powerset_iff],

intros i s hs,

have : tendsto (λ g : Π i, α i, g i) (𝓝 f) (𝓝 (f i)) := ((continuous_apply i).tendsto f),

refine (tendsto_lift'.1 ((this.comp tendsto_fst).Icc (this.comp tendsto_snd)) s hs).mono _,

exact λ p hp g hg, hp ⟨hg.1 _, hg.2 _⟩

theorem induced_order_topology' {α : Type u} {β : Type v}

[preorder α] [ta : topological_space β] [preorder β] [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) _ :=

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.2 ⟨{x | f b < x},

mem_inf_of_left $ mem_infi_of_mem _ $ mem_infi_of_mem (hf.2 ab) $ mem_principal_self _,

λ x, hf.1⟩ },

{ exact mem_comap.2 ⟨{x | x < f b},

mem_inf_of_right $ mem_infi_of_mem _ $ mem_infi_of_mem (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_of_mem _ (mem_infi_of_mem ⟨ab, b, or.inl rfl⟩ (mem_principal.2 _)),

exact λ c hc, lt_of_le_of_lt xb (hf.2 hc) },

{ rcases H₂ h with ⟨b, ab, xb⟩,

refine mem_infi_of_mem _ (mem_infi_of_mem ⟨ab, b, or.inr rfl⟩ (mem_principal.2 _)),

exact λ c hc, lt_of_lt_of_le (hf.2 hc) xb } },

theorem induced_order_topology {α : Type u} {β : Type v}

[preorder α] [ta : topological_space β] [preorder β] [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⟩)

instance order_topology_of_ord_connected {α : Type u}

[ta : topological_space α] [linear_order α] [order_topology α]

{t : set α} [ht : ord_connected t] :

order_topology t :=

letI := induced (coe : t → α) ta,

refine ⟨eq_of_nhds_eq_nhds (λ a, _)⟩,

rw [nhds_induced, nhds_generate_from, nhds_eq_order (a : α)],

apply le_antisymm,

{ refine le_infi (λ s, le_infi $ λ hs, le_principal_iff.2 _),

rcases hs with ⟨ab, b, rfl|rfl⟩,

{ refine ⟨Ioi b, _, λ _, id⟩,

refine mem_inf_of_left (mem_infi_of_mem b _),

exact mem_infi_of_mem ab (mem_principal_self (Ioi ↑b)) },

{ refine ⟨Iio b, _, λ _, id⟩,

refine mem_inf_of_right (mem_infi_of_mem b _),

exact mem_infi_of_mem ab (mem_principal_self (Iio b)) } },

{ rw [← map_le_iff_le_comap],

refine le_inf _ _,

{ refine le_infi (λ x, le_infi $ λ h, le_principal_iff.2 _),

by_cases hx : x ∈ t,

{ refine mem_infi_of_mem (Ioi ⟨x, hx⟩) (mem_infi_of_mem ⟨h, ⟨⟨x, hx⟩, or.inl rfl⟩⟩ _),

exact λ _, id },

simp only [set_coe.exists, mem_set_of_eq, mem_map'],

convert univ_sets _,

suffices hx' : ∀ (y : t), ↑y ∈ Ioi x,

{ simp [hx'] },

intros y,

revert hx,

contrapose!,

-- here we use the `ord_connected` hypothesis

exact λ hx, ht.out y.2 a.2 ⟨le_of_not_gt hx, le_of_lt h⟩ },

{ refine le_infi (λ x, le_infi $ λ h, le_principal_iff.2 _),

by_cases hx : x ∈ t,

{ refine mem_infi_of_mem (Iio ⟨x, hx⟩) (mem_infi_of_mem ⟨h, ⟨⟨x, hx⟩, or.inr rfl⟩⟩ _),

exact λ _, id },

simp only [set_coe.exists, mem_set_of_eq, mem_map'],

convert univ_sets _,

suffices hx' : ∀ (y : t), ↑y ∈ Iio x,

{ simp [hx'] },

intros y,

revert hx,

contrapose!,

-- here we use the `ord_connected` hypothesis

exact λ hx, ht.out a.2 y.2 ⟨le_of_lt h, le_of_not_gt hx⟩ } }

lemma nhds_within_Ici_eq'' [topological_space α] [preorder α] [order_topology α] (a : α) :

𝓝[≥] a = (⨅ u (hu : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) :=

rw [nhds_within, nhds_eq_order],

refine le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf _ inf_le_left) inf_le_right),

exact inf_le_right.trans (le_infi₂ $ λ l hl, principal_mono.2 $ Ici_subset_Ioi.2 hl)

lemma nhds_within_Iic_eq'' [topological_space α] [preorder α] [order_topology α] (a : α) :

𝓝[≤] a = (⨅ l < a, 𝓟 (Ioi l)) ⊓ 𝓟 (Iic a) :=

nhds_within_Ici_eq'' (to_dual a)

lemma nhds_within_Ici_eq' [topological_space α] [preorder α] [order_topology α] {a : α}

(ha : ∃ u, a < u) :

𝓝[≥] a = ⨅ u (hu : a < u), 𝓟 (Ico a u) :=

by simp only [nhds_within_Ici_eq'', binfi_inf ha, inf_principal, Iio_inter_Ici]

lemma nhds_within_Iic_eq' [topological_space α] [preorder α] [order_topology α] {a : α}

(ha : ∃ l, l < a) :

𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a) :=

by simp only [nhds_within_Iic_eq'', binfi_inf ha, inf_principal, Ioi_inter_Iic]

lemma nhds_within_Ici_basis' [topological_space α] [linear_order α] [order_topology α] {a : α}

(ha : ∃ u, a < u) : (𝓝[≥] a).has_basis (λ u, a < u) (λ u, Ico a u) :=

(nhds_within_Ici_eq' ha).symm ▸ has_basis_binfi_principal (λ b hb c hc,

⟨min b c, lt_min hb hc, Ico_subset_Ico_right (min_le_left _ _),

Ico_subset_Ico_right (min_le_right _ _)⟩) ha

lemma nhds_within_Iic_basis' [topological_space α] [linear_order α] [order_topology α] {a : α}

(ha : ∃ l, l < a) : (𝓝[≤] a).has_basis (λ l, l < a) (λ l, Ioc l a) :=

by { convert @nhds_within_Ici_basis' αᵒᵈ _ _ _ (to_dual a) ha,

exact funext (λ x, (@dual_Ico _ _ _ _).symm) }

lemma nhds_within_Ici_basis [topological_space α] [linear_order α] [order_topology α]

[no_max_order α] (a : α) : (𝓝[≥] a).has_basis (λ u, a < u) (λ u, Ico a u) :=

nhds_within_Ici_basis' (exists_gt a)

lemma nhds_within_Iic_basis [topological_space α] [linear_order α] [order_topology α]

[no_min_order α] (a : α) : (𝓝[≤] a).has_basis (λ l, l < a) (λ l, Ioc l a) :=

nhds_within_Iic_basis' (exists_lt a)

lemma nhds_top_order [topological_space α] [preorder α] [order_top α] [order_topology α] :

𝓝 (⊤:α) = (⨅l (h₂ : l < ⊤), 𝓟 (Ioi l)) :=

by simp [nhds_eq_order (⊤:α)]

lemma nhds_bot_order [topological_space α] [preorder α] [order_bot α] [order_topology α] :

𝓝 (⊥:α) = (⨅l (h₂ : ⊥ < l), 𝓟 (Iio l)) :=

by simp [nhds_eq_order (⊥:α)]

lemma nhds_top_basis [topological_space α] [linear_order α] [order_top α] [order_topology α]

[nontrivial α] :

(𝓝 ⊤).has_basis (λ a : α, a < ⊤) (λ a : α, Ioi a) :=

have ∃ x : α, x < ⊤, from (exists_ne ⊤).imp $ λ x hx, hx.lt_top,

by simpa only [Iic_top, nhds_within_univ, Ioc_top] using nhds_within_Iic_basis' this

lemma nhds_bot_basis [topological_space α] [linear_order α] [order_bot α] [order_topology α]

[nontrivial α] :

(𝓝 ⊥).has_basis (λ a : α, ⊥ < a) (λ a : α, Iio a) :=

@nhds_top_basis αᵒᵈ _ _ _ _ _

lemma nhds_top_basis_Ici [topological_space α] [linear_order α] [order_top α] [order_topology α]

[nontrivial α] [densely_ordered α] :

(𝓝 ⊤).has_basis (λ a : α, a < ⊤) Ici :=

nhds_top_basis.to_has_basis

(λ a ha, let ⟨b, hab, hb⟩ := exists_between ha in ⟨b, hb, Ici_subset_Ioi.mpr hab⟩)

(λ a ha, ⟨a, ha, Ioi_subset_Ici_self⟩)

lemma nhds_bot_basis_Iic [topological_space α] [linear_order α] [order_bot α] [order_topology α]

[nontrivial α] [densely_ordered α] :

(𝓝 ⊥).has_basis (λ a : α, ⊥ < a) Iic :=

@nhds_top_basis_Ici αᵒᵈ _ _ _ _ _ _

lemma tendsto_nhds_top_mono [topological_space β] [preorder β] [order_top β] [order_topology β]

{l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊤)) (hg : f ≤ᶠ[l] g) :

tendsto g l (𝓝 ⊤) :=

simp only [nhds_top_order, tendsto_infi, tendsto_principal] at hf ⊢,

intros x hx,

filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le,

lemma tendsto_nhds_bot_mono [topological_space β] [preorder β] [order_bot β] [order_topology β]

{l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊥)) (hg : g ≤ᶠ[l] f) :

tendsto g l (𝓝 ⊥) :=

@tendsto_nhds_top_mono α βᵒᵈ _ _ _ _ _ _ _ hf hg

lemma tendsto_nhds_top_mono' [topological_space β] [preorder β] [order_top β]

[order_topology β] {l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊤)) (hg : f ≤ g) :

tendsto g l (𝓝 ⊤) :=

tendsto_nhds_top_mono hf (eventually_of_forall hg)

lemma tendsto_nhds_bot_mono' [topological_space β] [preorder β] [order_bot β]

[order_topology β] {l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊥)) (hg : g ≤ f) :

tendsto g l (𝓝 ⊥) :=

tendsto_nhds_bot_mono hf (eventually_of_forall hg)

section linear_order

variables [topological_space α] [linear_order α]

section order_closed_topology

variables [order_closed_topology α] {a b : α}

lemma eventually_le_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b :=

eventually_iff.mpr (mem_nhds_iff.mpr ⟨Iio b, Iio_subset_Iic_self, is_open_Iio, hab⟩)

lemma eventually_lt_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x < b :=

eventually_iff.mpr (mem_nhds_iff.mpr ⟨Iio b, rfl.subset, is_open_Iio, hab⟩)