Order topology

Stream: Is there code for X?

[Heather Macbeth]

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') },
          by_contradiction hxy,
          have : ¬ (f y < f x) := not_lt.mpr (h_mono.monotone_incr_on x hx y hy (not_lt.mp hxy)),
          contradiction } },
      { 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]

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

[Johan Commelin]

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]

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]

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

[Yury G. Kudryashov]

/me should more carefully review PRs.

[Yury G. Kudryashov]

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]

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]

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

[Yury G. Kudryashov]

I'll PR a better fix tonight.

[Yury G. Kudryashov]

#3629 fixes I??_mem_nhds_within_I??.

[Anatole Dedecker]

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]

I just commented on that PR

[Heather Macbeth]

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]

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]

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]

#3843