## Stream: Is there code for X?

### Topic: Order topology

#### Heather Macbeth (Jul 29 2020 at 20:50):

I suspect I am missing some tricks in using the order topology library. Here's my lemma:

lemma continuous_of_monotone_surjective  {ι α : Type*}
[topological_space ι] [linear_order ι] [order_topology ι]
[topological_space α] [decidable_linear_order α] [order_topology α]
{f : ι → α} {a b : ι} (hab : a ≤ b)
(h_mono : strict_mono_incr_on f (Icc a b)) (h_surj : surj_on f (Icc a b) (Icc (f a) (f b))) :
continuous_on f (Icc a b)


And here is my voluminous proof:

def monotone_incr_on [has_le α] [has_le β] (f : α → β) (t : set α) : Prop :=
∀ (x ∈ t) (y ∈ t), x ≤ y → f x ≤ f y

lemma strict_mono_incr_on.monotone_incr_on
[partial_order α] [preorder β] {f : α → β} {t : set α} (H : strict_mono_incr_on f t) :
monotone_incr_on f t :=
begin
intros a ha b hb hab,
by_cases hab' : a = b,
{ rw hab' },
{ exact le_of_lt (H a ha b hb (lt_of_le_of_ne hab hab')) }
end

lemma Ioc_mem_nhds_within_Icc {ι : Type*} [topological_space ι] [linear_order ι] [order_topology ι]
{a b x y : ι} (hxy : y < x) :
Ioc y b ∈ nhds_within x (Icc a b) :=
mem_nhds_within.mpr ⟨Ioi y, is_open_Ioi, hxy, λ _ hz, ⟨hz.1, hz.2.2⟩⟩

lemma continuous_of_monotone_surjective  {ι α : Type*}
[topological_space ι] [linear_order ι] [order_topology ι]
[topological_space α] [decidable_linear_order α] [order_topology α]
{f : ι → α} {a b : ι} (hab : a ≤ b)
(h_mono : strict_mono_incr_on f (Icc a b)) (h_surj : surj_on f (Icc a b) (Icc (f a) (f b))) :
continuous_on f (Icc a b) :=
begin
have ha : a ∈ Icc a b := left_mem_Icc.mpr hab,
have hb : b ∈ Icc a b := right_mem_Icc.mpr hab,
simp only [continuous_on, continuous_within_at, tendsto_order],
intros x hx,
split,
{ intros p hp,
by_cases hx' : x = a,
{ refine ⟨univ, (𝓝 x).univ_sets, Icc a b, mem_principal_self (Icc a b), _⟩,
intros y hy,
rw hx' at hp,
exact lt_of_lt_of_le hp (h_mono.monotone_incr_on a ha y hy.2 hy.2.1) },
{ have hmax : (max p (f a)) ∈ Icc (f a) (f b),
{ simp only [max_le_iff, le_max_iff, mem_Icc],
refine ⟨or.inr (le_refl (f a)), _, h_mono.monotone_incr_on a ha b hb hab⟩,
refine le_of_lt (lt_of_lt_of_le hp _),
exact h_mono.monotone_incr_on x hx b hb hx.2 },
rcases h_surj hmax with ⟨y, ⟨hy, hfy⟩⟩,
simp only [filter.eventually_iff_exists_mem],
refine ⟨Ioc y b, _, _⟩,
{ refine Ioc_mem_nhds_within_Icc _,
{ have : f y < f x,
{ rw hfy,
refine max_lt hp (h_mono a ha x hx _),
exact lt_of_le_of_ne hx.1 (ne.symm hx') },
have : ¬ (f y < f x) := not_lt.mpr (h_mono.monotone_incr_on x hx y hy (not_lt.mp hxy)),
{ intros z hz'',
have hz' : a < z := (lt_of_le_of_lt hy.1 hz''.1),
have hz : z ∈ Icc a b := ⟨le_of_lt hz', hz''.2⟩,
by_cases hp : p < f a,
{ refine lt_trans hp _,
exact h_mono a ha z hz hz' },
{ push_neg at hp,
rw [← max_eq_left hp, ← hfy],
exact h_mono y hy z hz hz''.1 } } } },
{ -- the same again, but with opposite inequalities!
sorry }
end


Can someone suggest some hints for golfing?

#### Heather Macbeth (Jul 30 2020 at 04:26):

Perhaps in particular, how do I use order_dual to flip all the inequalities in a lemma?

#### Johan Commelin (Jul 30 2020 at 05:48):

Heather Macbeth said:

-- the same again, but with opposite inequalities!


I think this means that you need to factor out a lemma which you can then apply to \a and order_dual \a.

#### Yury G. Kudryashov (Jul 30 2020 at 05:53):

BTW, you don't need a ≤ b in this lemma. Otherwise Icc a b is empty, and every function is continuous on the empty set.

#### Yury G. Kudryashov (Jul 30 2020 at 05:54):

I'll try to golf the proof in a few minutes.

#### Yury G. Kudryashov (Jul 30 2020 at 06:21):

/me should more carefully review PRs.

#### Yury G. Kudryashov (Jul 30 2020 at 06:38):

Try this:

import topology.algebra.ordered

variables {ι α β : Type*}

open set filter
open_locale classical

def mono_incr_on [has_le α] [has_le β] (f : α → β) (t : set α) : Prop :=
∀ (x ∈ t) (y ∈ t), x ≤ y → f x ≤ f y

lemma strict_mono_incr_on.mono_incr_on [partial_order α] [preorder β] {f : α → β} {s : set α}
(h : strict_mono_incr_on f s) :
mono_incr_on f s :=
λ x hx y hy hxy, (eq_or_lt_of_le hxy).elim (λ h, h ▸ le_refl _) (λ hxy, le_of_lt $h x hx y hy hxy) variables [topological_space ι] [linear_order ι] [order_topology ι] [topological_space α] [decidable_linear_order α] [order_topology α] lemma continuous_right_of_strict_mono_surjective {f : ι → α} {a b : ι} (hab : a < b) (h_mono : strict_mono_incr_on f (Icc a b)) (h_surj : surj_on f (Icc a b) (Icc (f a) (f b))) : tendsto f (nhds_within a (Ici a)) (nhds_within (f a) (Ici$ f a)) :=
begin
have hab' : a ≤ b := le_of_lt hab,
have ha : a ∈ Icc a b := left_mem_Icc.2 hab',
have hb : b ∈ Icc a b := right_mem_Icc.2 hab',
have hfab : f a < f b := h_mono a ha b hb hab,
intros s hs,
obtain ⟨y, hy, hys⟩ : ∃ y ∈ Ioc (f a) (f b), Ico (f a) y ⊆ s :=
(mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset hfab).1 hs,
refine mem_sets_of_superset (mem_map.2 _) hys,
rcases h_surj (Ioc_subset_Icc_self hy) with ⟨x, hx, rfl⟩,
rcases eq_or_lt_of_le hx.1 with rfl|hax, { exact (lt_irrefl _ hy.1).elim },
refine mem_sets_of_superset (Ico_mem_nhds_within_Ici (left_mem_Ico.2 hax)) _,
intros z hz,
have hz' : z ∈ Icc a b := ⟨hz.1, le_trans (le_of_lt hz.2) hx.2⟩,
exact ⟨h_mono.mono_incr_on _ ha _ hz' hz.1, h_mono _ hz' _ hx hz.2⟩
end

lemma continuous_left_of_strict_mono_surjective {f : ι → α} {a b : ι} (hab : a < b)
(h_mono : strict_mono_incr_on f (Icc a b)) (h_surj : surj_on f (Icc a b) (Icc (f a) (f b))) :
tendsto f (nhds_within b (Iic b)) (nhds_within (f b) (Iic \$ f b)) :=
begin
apply @continuous_right_of_strict_mono_surjective (order_dual ι) (order_dual α),
{ exact hab, },
{ simp only [dual_Icc],
exact λ x hx y hy hxy, h_mono y hy x hx hxy },
{ simpa only [dual_Icc] }
end


it needs a fix to src/topology/algebra/ordered.lean:

@@ -1111,13 +1111,13 @@ lemma Ioc_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ioo a c) :
Ioc a c ∈ nhds_within b (Ici b) :=
mem_sets_of_superset (Ioo_mem_nhds_within_Ici H) Ioo_subset_Ioc_self

-lemma Ico_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ioo a c) :
+lemma Ico_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ico a c) :
Ico a c ∈ nhds_within b (Ici b) :=
-mem_sets_of_superset (Ioo_mem_nhds_within_Ici H) Ioo_subset_Ico_self
+(mem_nhds_within_Ici_iff_exists_Ico_subset' H.2).2 ⟨c, H.2, Ico_subset_Ico_left H.1⟩

-lemma Icc_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ioo a c) :
+lemma Icc_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ico a c) :
Icc a c ∈ nhds_within b (Ici b) :=
-mem_sets_of_superset (Ioo_mem_nhds_within_Ici H) Ioo_subset_Icc_self
+mem_sets_of_superset (Ico_mem_nhds_within_Ici H) Ico_subset_Icc_self

/-- The following statements are equivalent:




#### Yury G. Kudryashov (Jul 30 2020 at 06:41):

You still need to consider cases x = a, a < x < b, and x = b in the main statement. In case a < x < b you'll also need a statement "continuous on the left → continuous on the right → continuous at".

#### Yury G. Kudryashov (Jul 30 2020 at 06:42):

I remember reviewing a PR with something similar very recently (as a preparation to l'Hopital's rule).

#### Yury G. Kudryashov (Jul 30 2020 at 06:52):

I'll PR a better fix tonight.

#### Yury G. Kudryashov (Jul 30 2020 at 07:42):

#3629 fixes I??_mem_nhds_within_I??.

#### Anatole Dedecker (Jul 30 2020 at 12:21):

Yury G. Kudryashov said:

you'll also need a statement "continuous on the left → continuous on the right → continuous at".

https://github.com/leanprover-community/mathlib/pull/3590/files#diff-69913e770559c1df859d4767801aa0e0R2221

#### Patrick Massot (Jul 30 2020 at 12:34):

I just commented on that PR

#### Heather Macbeth (Jul 30 2020 at 14:03):

Thank you very much @Yury G. Kudryashov, I learned a lot from this. I'll PR it with you as co-author after @Anatole Dedecker's lemma is merged.

#### Yury G. Kudryashov (Jul 30 2020 at 14:06):

BTW, a fact I'd love to have in mathlib (and it should easily follow from your lemmas): for two conditionally_complete_linear_orders, order_iso is a homeomorph, and a homeomorph is either an order-preserving or an order-reversing order_iso.

#### Heather Macbeth (Jul 30 2020 at 14:07):

Yep. My goal with this was a related lemma: between closed intervals in the reals (or probably, a conditionally_complete_linear_order once I look up the definition), a continuous strictly increasing function has a continuous inverse.

#### Heather Macbeth (Aug 17 2020 at 18:57):

#3843

Last updated: May 07 2021 at 22:14 UTC