Zulip Chat Archive

Stream: Is there code for X?

Topic: Order topology


view this post on Zulip 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') },
          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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 05:54):

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

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 06:21):

/me should more carefully review PRs.

view this post on Zulip 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:

view this post on Zulip 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".

view this post on Zulip 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).

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 06:52):

I'll PR a better fix tonight.

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 07:42):

#3629 fixes I??_mem_nhds_within_I??.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 30 2020 at 12:34):

I just commented on that PR

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Aug 17 2020 at 18:57):

#3843


Last updated: May 07 2021 at 22:14 UTC