Pasting lemma

Stream: new members

[Emiel Lanckriet]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Alex J. Best]

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]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Emiel Lanckriet]

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

[Emiel Lanckriet]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Emiel Lanckriet]

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.

[Alex J. Best]

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.

[Alex J. Best]

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

[Emiel Lanckriet]

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

[Kevin Buzzard]

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

[Alex J. Best]

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

[Emiel Lanckriet]

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?

[Alex J. Best]

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

[Patrick Massot]

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

[Patrick Massot]

Of course the key trick is to use docs#continuous_on_if

[Emiel Lanckriet]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Emiel Lanckriet]

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.

[Patrick Massot]

#mwe?

[Emiel Lanckriet]

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

[Patrick Massot]

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

[Patrick Massot]

Are you using current mathlib master branch?

[Patrick Massot]

That means commit 011a2622a83ba086a7c

[Patrick Massot]

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

[Emiel Lanckriet]

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

[Emiel Lanckriet]

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

[Patrick Massot]

Upgrading mathlib like this should be enough indeed.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

Somewhat new as in: was merged yesterday.

[Johan Commelin]

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

[Patrick Massot]

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

[Emiel Lanckriet]

I restarted everything and it worked.

[Emiel Lanckriet]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Emiel Lanckriet]

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.