Zulip Chat Archive

Stream: new members

Topic: Pasting lemma


view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 14:19):

I tried proving the pasting lemma from general topology and I succeeded, but I can't help but think that there should be a shorter way to prove this. This is my attempt at proving it. I also phrased the theorem myself, so it might also be that some of the difficulties can be resolved by phrasing the theorem better.

example {X Y : Type*} [topological_space X] [topological_space Y] {A B : set X} (A_closed : is_closed A) (B_closed : is_closed B)
    (XeqAB : A  B = univ) (f : X  Y) (g: X  Y) (f_cont : continuous_on f A) (g_cont : continuous_on g B)
    (feqg :  x  A  B, f x = g x) :
     (h : X  Y), ( (x  A), h x = f x)  ( (x  B), h x = g x)  continuous h :=
begin
    use λ (x : X), if xA : x  A then f x else g x,
    split,
    {
        intros x xA,
        rw dif_pos,
        assumption
    },
    split,
    {
        intros x xB,
        rcases dec_em (x  A) with xA | xnA,
        {
            rw dif_pos,
            exact feqg x (mem_inter xA xB),
            assumption
        },
        {   rw dif_neg, assumption  }
    },
    {
        rw continuous_iff_continuous_on_univ,
        rw  XeqAB,
        apply continuous_on_iff_is_closed.mpr,
        intros t t_closed,
        use (A  f⁻¹' t)  (B  g⁻¹' t),
        split,
        {
            apply is_closed_union,
            exact continuous_on.preimage_closed_of_closed f_cont A_closed t_closed,
            exact continuous_on.preimage_closed_of_closed g_cont B_closed t_closed
        },
        {
            rw XeqAB,
            rw [inter_univ, inter_univ],
            ext,
            split,
            {
                intros h,
                simp at h,
                rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t),
                rcases dec_em (x  A) with xA | xnA,
                {
                    rw dif_pos xA at h,
                    left,
                    apply mem_inter xA h
                },
                {
                    rw dif_neg xnA at h,
                    right,
                    apply mem_inter (exclusionAB XeqAB x xnA) h,
                    assumption
                }
            },
            {
                intros h,
                simp,
                rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t) at h,
                rcases dec_em (x  A) with xA | xnA,
                {
                    rw dif_pos xA,
                    rcases h with xAft | xBgt,
                    {   exact xAft.2    },
                    {
                        rw feqg x (mem_inter xA xBgt.1),
                        exact xBgt.2
                    }
                },
                {
                    rw dif_neg xnA,
                    rcases h with xAft | xBgt,
                    {   exfalso, exact xnA xAft.1   },
                    {   exact xBgt.2    }
                }
            }
        }
    },
end

ExclusionAB is used somewhere and has this code:

lemma exclusionBA {X Y : Type*} {A B : set X} (XeqAB : A  B = univ) :  (x : X), x  B  x  A :=
begin
    intro x,
    have xuniv := mem_univ x,
    rw  XeqAB at xuniv,
    cases xuniv,
    {   intro _, assumption },
    {   intro xnB, exfalso, exact xnB xuniv },
end

I know this is big chunk of code, but I have no idea how to structure this question better. Suggestions are welcome.

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 14:20):

You should make a #mwe -- one piece of code which contains all imports, opens, universes, definitions, and which someone can cut and paste and it will work on their machine without any extra stuff or thought. You're nearly there.

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 14:20):

You still need to put your two pieces of code into one and include all imports

view this post on Zulip Alex J. Best (Aug 21 2020 at 14:21):

I didn't run your code, but the tactic tactic#split_ifs is really useful for doing the sort of thing you are doing in the second set of braces.

view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 14:26):

I believe this is an #mwe

import topology.basic topology.bases topology.metric_space.basic topology.order topology.constructions
import topology.continuous_on
import data.set.function tactic

noncomputable theory

open_locale classical filter

open filter set topological_space function

lemma exclusionAB {X Y : Type*} {A B : set X} (XeqAB : A  B = univ) :  (x : X), x  A  x  B :=
begin
    intro x,
    have xuniv := mem_univ x,
    rw  XeqAB at xuniv,
    cases xuniv,
    {   intro xnA, exfalso, exact xnA xuniv },
    {   intro _, assumption },
end


example {X Y : Type*} [topological_space X] [topological_space Y] {A B : set X} (A_closed : is_closed A) (B_closed : is_closed B)
    (XeqAB : A  B = univ) (f : X  Y) (g: X  Y) (f_cont : continuous_on f A) (g_cont : continuous_on g B)
    (feqg :  x  A  B, f x = g x) :
     (h : X  Y), ( (x  A), h x = f x)  ( (x  B), h x = g x)  continuous h :=
begin
    use λ (x : X), if xA : x  A then f x else g x,
    split,
    {
        intros x xA,
        rw dif_pos,
        assumption
    },
    split,
    {
        intros x xB,
        rcases dec_em (x  A) with xA | xnA,
        {
            rw dif_pos,
            exact feqg x (mem_inter xA xB),
            assumption
        },
        {   rw dif_neg, assumption  }
    },
    {
        rw continuous_iff_continuous_on_univ,
        rw  XeqAB,
        apply continuous_on_iff_is_closed.mpr,
        intros t t_closed,
        use (A  f⁻¹' t)  (B  g⁻¹' t),
        split,
        {
            apply is_closed_union,
            exact continuous_on.preimage_closed_of_closed f_cont A_closed t_closed,
            exact continuous_on.preimage_closed_of_closed g_cont B_closed t_closed
        },
        {
            rw XeqAB,
            rw [inter_univ, inter_univ],
            ext,
            split,
            {
                intros h,
                simp at h,
                rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t),
                rcases dec_em (x  A) with xA | xnA,
                {
                    rw dif_pos xA at h,
                    left,
                    apply mem_inter xA h
                },
                {
                    rw dif_neg xnA at h,
                    right,
                    apply mem_inter (exclusionAB XeqAB x xnA) h,
                    assumption
                }
            },
            {
                intros h,
                simp,
                rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t) at h,
                rcases dec_em (x  A) with xA | xnA,
                {
                    rw dif_pos xA,
                    rcases h with xAft | xBgt,
                    {   exact xAft.2    },
                    {
                        rw feqg x (mem_inter xA xBgt.1),
                        exact xBgt.2
                    }
                },
                {
                    rw dif_neg xnA,
                    rcases h with xAft | xBgt,
                    {   exfalso, exact xnA xAft.1   },
                    {   exact xBgt.2    }
                }
            }
        }
    },
end

view this post on Zulip Reid Barton (Aug 21 2020 at 14:28):

So I think the main issue with this code is that you skipped a step--you wanted to talk about gluing continuous functions before developing a way to talk about gluing ordinary functions.

view this post on Zulip Reid Barton (Aug 21 2020 at 14:29):

I proved something basically equivalent (but with a whole lot of extra language) here; the file is split in two parts: first gluing in Set and then gluing in Top.

view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 14:30):

So, take pieces of the code and put it in another theorem that tells us there a glued function?

view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 14:32):

So, prove this first?

example {X Y : Type*} {A B : set X}
    (XeqAB : A  B = univ) (f : X  Y) (g: X  Y)
    (feqg :  x  A  B, f x = g x) :
     (h : X  Y), ( (x  A), h x = f x)  ( (x  B), h x = g x) :=
begin
    sorry
end

view this post on Zulip Reid Barton (Aug 21 2020 at 14:34):

First you could construct the glued function. Since it is unique you might as well make it a definition, and not have this statement. Then write lemmas saying that it restricts to the original functions.
Then, you can prove that if the inputs are continuous and the sets are closed, the output is continuous.

view this post on Zulip Reid Barton (Aug 21 2020 at 14:35):

The last part really only needs that the output restricts to the input functions on the two sets (after all, there's only one such function anyways). So you could first prove it in the form: a function whose restrictions to A and B are continuous is itself continuous. Then apply the lemmas from the Set part.

view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 14:44):

I am having some trouble defining the definition for the glued function, I have this

variables {X Y : Type*}
def glued : set X  (X  Y)  (X  Y)  (X  Y) := λ A f g (x : X), if xA : x  A then f x else g x

but I don't know how to include ∀ x ∈ A ∩ B, f x = g x.

view this post on Zulip Alex J. Best (Aug 21 2020 at 14:48):

The general principle is that you don't include that in the definition (though you could), as it makes the definition more verbose (for one).
Instead it should be an assumption for any lemmas you prove about this definition, as really the definition only makes sense when it holds.

view this post on Zulip Alex J. Best (Aug 21 2020 at 14:49):

Btw its fine to define a function with named arguments like:

def glued (A : set X) (f g : X  Y) (x : X) : Y := if xA : x  A then f x else g x

instead

view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 15:21):

I tried this, but it is not really shorter, it's just cut into pieces.

import topology.basic topology.bases topology.metric_space.basic topology.order topology.constructions
import topology.continuous_on
import data.set.function tactic

variables {α β : Type*} [inhabited α]

noncomputable theory

open_locale classical filter

open filter set topological_space function

lemma exclusionAB {X Y : Type*} {A B : set X} (XeqAB : A  B = univ) :  (x : X), x  A  x  B :=
begin
    intro x,
    have xuniv := mem_univ x,
    rw  XeqAB at xuniv,
    cases xuniv,
    {   intro xnA, exfalso, exact xnA xuniv },
    {   intro _, assumption },
end

def glued {X Y : Type*} (A : set X) (f g : X  Y) : (X  Y) := λ (x : X), if xA : x  A then f x else g x

lemma gluedAf {X Y : Type*} {A : set X} {x : X} (xA : x  A) (f g : X  Y) : glued A f g x = f x :=
by {unfold glued, rw dif_pos, assumption}

lemma gluednAf {X Y : Type*} {A : set X} {x : X} (xA : x  A) (f g : X  Y) : glued A f g x = g x :=
by {unfold glued, rw dif_neg, assumption}

lemma gluedABg {X Y : Type*} {A B : set X} {x : X} (xA : x  A) (xB : x  B) (f g : X  Y) (feqg :  x  A  B, f x = g x) :
    glued A f g x = g x :=
by { unfold glued, rw dif_pos, exact feqg x (mem_inter xA xB), assumption }

lemma gluedBg {X Y : Type*} {A B : set X} {x : X} (xB : x  B) (f g : X  Y) (feqg :  x  A  B, f x = g x) :
    glued A f g x = g x :=
by {
        rcases dec_em (x  A) with xA | xnA,
        {   exact gluedABg xA xB f g feqg},
        {   exact gluednAf xnA f g  }
    }

lemma gluing {X Y : Type*} {A B : set X} {f g : X  Y}
    (feqg :  x  A  B, f x = g x) :
    ( (x  A), glued A f g x = f x)   (x  B), glued A f g x = g x :=
begin
    split,
    {   exact λ (x : X) (xA : x  A), gluedAf xA f g    },
    {   exact λ x xB, gluedBg xB f g feqg   },
end

example {X Y : Type*} [topological_space X] [topological_space Y] {A B : set X} (A_closed : is_closed A) (B_closed : is_closed B)
    (XeqAB : A  B = univ) (f : X  Y) (g: X  Y) (f_cont : continuous_on f A) (g_cont : continuous_on g B)
    (feqg :  x  A  B, f x = g x) :
    (( (x  A), glued A f g x = f x)  ( (x  B), glued A f g x = g x))  continuous (glued A f g) :=
begin
    split,
    exact gluing feqg,
    {
        rw continuous_iff_continuous_on_univ,
        rw  XeqAB,
        apply continuous_on_iff_is_closed.mpr,
        intros t t_closed,
        use (A  f⁻¹' t)  (B  g⁻¹' t),
        split,
        {
            apply is_closed_union,
            exact continuous_on.preimage_closed_of_closed f_cont A_closed t_closed,
            exact continuous_on.preimage_closed_of_closed g_cont B_closed t_closed
        },
        {
            rw XeqAB,
            rw [inter_univ, inter_univ],
            ext,
            split,
            {
                intros h,
                simp at h,
                rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t),
                rcases dec_em (x  A) with xA | xnA,
                {
                    rw gluedAf xA at h,
                    left,
                    apply mem_inter xA h
                },
                {
                    rw gluednAf xnA at h,
                    right,
                    apply mem_inter (exclusionAB XeqAB x xnA) h,
                    assumption
                }
            },
            {
                intros h,
                simp,
                rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t) at h,
                rcases dec_em (x  A) with xA | xnA,
                {
                    rw gluedAf xA,
                    rcases h with xAft | xBgt,
                    {   exact xAft.2    },
                    {
                        rw feqg x (mem_inter xA xBgt.1),
                        exact xBgt.2
                    }
                },
                {
                    rw gluednAf xnA,
                    rcases h with xAft | xBgt,
                    {   exfalso, exact xnA xAft.1   },
                    {   exact xBgt.2    }
                }
            }
        }
    },
end

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:32):

Cutting things into smaller pieces is definite progress. Take a look at data.finset.basic .

view this post on Zulip Alex J. Best (Aug 21 2020 at 15:51):

Alex J. Best said:

I didn't run your code, but the tactic tactic#split_ifs is really useful for doing the sort of thing you are doing in the second set of braces.

@Emiel Lanckriet in case you missed it, this tactic will definitely make some of your proofs shorter

view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 15:57):

I tried the split_ifs, but all the goals are of the form if then else = something, so not of the pure form if then else. Or am I missing something?

view this post on Zulip Alex J. Best (Aug 21 2020 at 16:11):

Oh I see, thats what I get for not running the code!

view this post on Zulip Patrick Massot (Aug 21 2020 at 16:38):

This is your statement (without the preliminary lemma that I inlined). Please try to use mathlib indentation and line breaks, it makes everything much easier to read, especially on Zulip.

example {X Y : Type*} [topological_space X] [topological_space Y]
  {A B : set X} (A_closed : is_closed A) (B_closed : is_closed B)
  (XeqAB : A  B = univ) (f : X  Y) (g: X  Y) (f_cont : continuous_on f A) (g_cont : continuous_on g B)
  (feqg :  x  A  B, f x = g x) :
   (h : X  Y), ( (x  A), h x = f x)  ( (x  B), h x = g x)  continuous h :=
begin
  refine ⟨λ x, if x  A then f x else g x, λ _ h, by simp [h], _, _⟩,
  { intros x x_in,
    split_ifs,
    { exact feqg _ h, x_in },
    { refl } },
  rw continuous_iff_continuous_on_univ,
  have key : closure A  B,
  { rw  B_closed.closure_eq,
    apply closure_mono,
    rintros x (x_not_in : x  A),
    cases (show x  A  B, by simp [XeqAB]) ; tauto },
  apply continuous_on_if,
  { rintros x ⟨-, x_in,
    apply feqg,
    erw [frontier_eq_closure_inter_closure, A_closed.closure_eq] at x_in,
    cases x_in,
    split ; tauto },
  { simp [A_closed.closure_eq, f_cont] },
  { apply g_cont.mono,
    simpa only [univ_inter] using key },
end

view this post on Zulip Patrick Massot (Aug 21 2020 at 16:39):

Of course the key trick is to use docs#continuous_on_if

view this post on Zulip Emiel Lanckriet (Aug 21 2020 at 22:01):

Thanks a lot, I will take look at it and hopefully learn something about writing more elegant code in the future.

view this post on Zulip Patrick Massot (Aug 21 2020 at 22:04):

Again, the main point is I used a stronger theorem.

view this post on Zulip Patrick Massot (Aug 21 2020 at 22:05):

We could still have this version in mathlib, so feel free to PR this (but without the existential), with three lemmas stating the three properties of the explicit function.

view this post on Zulip Emiel Lanckriet (Aug 22 2020 at 12:25):

I tried to run the code, but it doesn't recognise continuous_on_if. I have imported topology.continuous_on and opened topology. How do I fix this? I ran leanproject upgrade-mathlib, but that was not the problem.

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:34):

#mwe?

view this post on Zulip Emiel Lanckriet (Aug 22 2020 at 12:41):

I just copied your code, so the #mwe is there already with these imports:

import topology.basic topology.bases topology.metric_space.basic topology.order topology.constructions
import topology.continuous_on
import data.set.function tactic

variables {α β : Type*} [inhabited α]

noncomputable theory

open_locale classical filter

open filter set topological_space function

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:43):

I'm sorry, I can't reproduce your issue.

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:43):

Are you using current mathlib master branch?

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:44):

That means commit 011a2622a83ba086a7c

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:44):

(but I'm not using anything brand new here).

view this post on Zulip Emiel Lanckriet (Aug 22 2020 at 12:44):

I don't know, I tried running leanproject upgrade-mathlib is that sufficient, or do I need something else.

view this post on Zulip Emiel Lanckriet (Aug 22 2020 at 12:46):

Maybe it helps to note that the rintros x (x_not_in : x ∉ A), line also fails with '«)»' expected as error.

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:51):

Upgrading mathlib like this should be enough indeed.

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:51):

Can you gou inside _target/deps/mathlib and run git log there to see what the latest commit?

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:52):

I forgot that I used this type ascription in rintros, that's a somewhat new feature.

view this post on Zulip Patrick Massot (Aug 22 2020 at 12:53):

Somewhat new as in: was merged yesterday.

view this post on Zulip Johan Commelin (Aug 22 2020 at 13:04):

The type ascriptions are already a couple of days old right? Yesterday was the - arguments for rintros

view this post on Zulip Patrick Massot (Aug 22 2020 at 13:08):

Oh yes, you're right. So I was right in the beginning, I used nothing new.

view this post on Zulip Emiel Lanckriet (Aug 23 2020 at 12:01):

I restarted everything and it worked.

view this post on Zulip Emiel Lanckriet (Aug 23 2020 at 12:26):

So, I got your example working and changed some stuff in my proof to the more elegant solutions in yours. You said something about PR'ing the solution I had, so two how do you PR and is this fit to be PR'ed?

import topology.basic topology.bases topology.metric_space.basic topology.order topology.constructions
import topology.continuous_on
import data.set.function tactic

variables {α β : Type*} [inhabited α]

noncomputable theory

open_locale classical filter

open filter set topological_space function

lemma glued_is_f_in_A {X Y : Type*} [topological_space X] [topological_space Y]
    {A B : set X} (f g : X  Y) :
     (x  A), (λ x, if x  A then f x else g x) x = f x :=
λ _ h, by simp [h]

lemma glued_is_g_in_B {X Y : Type*} [topological_space X] [topological_space Y] {A B : set X}
    (f g : X  Y) (feqg :  x  A  B, f x = g x) :
     (x  B), (λ x, if x  A then f x else g x) x = g x :=
begin
  intros x x_in,
  simp,
  split_ifs,
  { exact feqg _ h, x_in },
  { refl }
end

lemma pastingLemma {X Y : Type*} [topological_space X] [topological_space Y] {A B : set X} (A_closed : is_closed A) (B_closed : is_closed B)
    (XeqAB : A  B = univ) {f g : X  Y} (f_cont : continuous_on f A) (g_cont : continuous_on g B)
    (feqg :  x  A  B, f x = g x) :
    continuous (λ x, if x  A then f x else g x) :=
begin
    { rw continuous_iff_continuous_on_univ,
      rw  XeqAB,
      apply continuous_on_iff_is_closed.mpr,
      intros t t_closed,
      use (A  f⁻¹' t)  (B  g⁻¹' t),
      split,
      { apply is_closed_union,
        exact continuous_on.preimage_closed_of_closed f_cont A_closed t_closed,
        exact continuous_on.preimage_closed_of_closed g_cont B_closed t_closed },
        { rw XeqAB,
          rw [inter_univ, inter_univ],
          ext,
          split,
          { intros h,
            simp at h,
            rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t),
            rcases dec_em (x  A) with xA | xnA,
            { left,
              simp [xA] at h,
              split; assumption },
              { simp [xnA] at h,
                right,
                rcases (show x  A  B, by simp [XeqAB]) with xA | xB,
                { tauto },
                { exact xB, h } }
          },
          { intros h,
            simp,
            rw mem_union x (A  f⁻¹' t) (B  g⁻¹' t) at h,
            rcases dec_em (x  A) with xA | xnA,
            { simp [xA],
              rcases h with xAft | xBgt,
              { exact xAft.2 },
              { rw feqg x (mem_inter xA xBgt.1),
                exact xBgt.2 }
              },
              { simp [xnA],
                rcases h with xAft | xBgt,
                { exfalso, exact xnA xAft.1 },
                { exact xBgt.2 }
              }
          }
        }
    },
end

example {X Y : Type*} [topological_space X] [topological_space Y] {A B : set X} (A_closed : is_closed A) (B_closed : is_closed B)
    (XeqAB : A  B = univ) (f : X  Y) (g: X  Y) (f_cont : continuous_on f A) (g_cont : continuous_on g B)
    (feqg :  x  A  B, f x = g x) :
    (( (x  A), (λ x, if x  A then f x else g x) x = f x) 
     ( (x  B), (λ x, if x  A then f x else g x) x = g x)) 
     continuous (λ x, if x  A then f x else g x) :=
begin
    split,
    { refine ⟨λ _ h, by simp [h], _⟩,
      intros x x_in,
      simp,
      split_ifs,
      { exact feqg _ h, x_in },
      { refl } },
    apply pastingLemma A_closed B_closed XeqAB f_cont g_cont feqg,
end

view this post on Zulip Patrick Massot (Aug 23 2020 at 12:42):

I don't understand why the proof became more complicated than what I wrote.

view this post on Zulip Patrick Massot (Aug 23 2020 at 12:44):

glued_is_f_in_A's proof is so simple it doesn't really need to be stated. And the last lemma is uselessly repeating stuff, especially since you are not using the first two lemmas.

view this post on Zulip Patrick Massot (Aug 23 2020 at 12:45):

In the second lemma, you don't need that lambda, you can state ∀ x ∈ B, (if x ∈ A then f x else g x) = g x

view this post on Zulip Patrick Massot (Aug 23 2020 at 12:46):

And you shouldn't be using non-terminating simp, those make proofs harder to maintain.

view this post on Zulip Patrick Massot (Aug 23 2020 at 12:47):

As for the main lemma, you should first do a version where you don't assume A ∪ B = univ but conclude only continuous_on _ (A ∪ B).

view this post on Zulip Patrick Massot (Aug 23 2020 at 12:47):

See also https://leanprover-community.github.io/contribute/index.html

view this post on Zulip Emiel Lanckriet (Aug 23 2020 at 14:14):

Ah, ok, you meant PR'ing your version, I thought PR'ing my my attempt which did not use continuous_on_if, but thanks for the tips. I'll keep them in mind.


Last updated: May 14 2021 at 12:18 UTC