Zulip Chat Archive

Stream: Is there code for X?

Topic: is_closed.graph


view this post on Zulip Adam Topaz (Apr 06 2021 at 13:23):

Suppose f:XYf : X \to Y is a continuous function between sufficiently nice topological spaces (I think t2 suffices). Do we know that the graph of ff, as a subset of X×YX \times Y, is a closed subset?

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:25):

Do we even have docs#function.graph?

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:25):

Apparently "yes", but as a rel :question:

view this post on Zulip Adam Topaz (Apr 06 2021 at 13:27):

Yeah, it's as a rel. So one would need an uncurried variant. But it's still possible to have is_closed { x | f x.1 = x.2} or something like that

view this post on Zulip Adam Topaz (Apr 06 2021 at 13:28):

I guess this actually has a name? :rofl:
https://en.wikipedia.org/wiki/Closed_graph_theorem

view this post on Zulip Adam Topaz (Apr 06 2021 at 14:26):

Golfing challenge!

lemma closed_graph {X Y : Type*} [topological_space X] [topological_space Y] [t2_space Y]
  (f : X  Y) (hf : continuous f) : is_closed { x : X × Y | f x.1 = x.2 } :=
begin
  rw  closure_subset_iff_is_closed,
  intros x hx,
  rw mem_closure_iff_ultrafilter at hx,
  rcases hx with U,h1,h2⟩,
  have h : t2_space Y, by apply_instance,
  rw t2_iff_ultrafilter at h,
  apply h (ultrafilter.map prod.snd U),
  { intros A hA,
    simp,
    rw mem_nhds_sets_iff at hA,
    rw le_nhds_iff at h2,
    rcases hA with T,hT,hT1,hT2⟩,
    have : is_open { x : X × Y | f x.fst  T },
    { have : {x : X × Y | f x.fst  T} = (λ t, f t.fst) ⁻¹' T, refl,
      rw this,
      apply is_open.preimage _ hT1,
      apply continuous.comp hf continuous_fst },
    specialize h2 _ hT2 this,
    have hh : { x : X × Y | f x.fst  T }  {x : X × Y | f x.fst = x.snd}  U,
      exact filter.inter_sets _ h2 h1,
    have : { x : X × Y | f x.fst  T }  {x : X × Y | f x.fst = x.snd}  {x : X × Y | x.snd  A},
    { rintro t hh1,hh2⟩,
      dsimp at hh1 hh2,
      dsimp,
      rw  hh2,
      apply hT,
      exact hh1 },
    apply filter.sets_of_superset _ hh this },
  { have hh : continuous (prod.snd : X × Y  Y) := continuous_snd,
    rw continuous_iff_ultrafilter at hh,
    refine hh _ _ h2 }
end

view this post on Zulip Sebastien Gouezel (Apr 06 2021 at 15:00):

lemma closed_graph {X Y : Type*} [topological_space X] [topological_space Y] [t2_space Y]
  (f : X  Y) (hf : continuous f) : is_closed { x : X × Y | f x.1 = x.2 } :=
is_closed_eq (by continuity) (by continuity)

view this post on Zulip Adam Topaz (Apr 06 2021 at 15:00):

is_closed_eq!

view this post on Zulip Sebastien Gouezel (Apr 06 2021 at 15:01):

Yes, I knew this one, so it was a little bit like cheating.

view this post on Zulip Adam Topaz (Apr 06 2021 at 15:01):

I also didn't really know about the continuity tactic

view this post on Zulip Sebastien Gouezel (Apr 06 2021 at 15:02):

In this case, it's a little bit overkill (direct proofs are easy with dot notation), but it's nicer like that!

view this post on Zulip Adam Topaz (Apr 06 2021 at 15:02):

And in any case the ridiculous proof I had above was a good reminder for me about (ultra)filters :)


Last updated: May 16 2021 at 05:21 UTC