is_closed.graph

Stream: Is there code for X?

[Adam Topaz]

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

[Johan Commelin]

Do we even have docs#function.graph?

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Sebastien Gouezel]

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)

[Adam Topaz]

is_closed_eq!

[Sebastien Gouezel]

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

[Adam Topaz]

I also didn't really know about the continuity tactic

[Sebastien Gouezel]

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

[Adam Topaz]

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