## Stream: Is there code for X?

### Topic: is_closed.graph

#### Adam Topaz (Apr 06 2021 at 13:23):

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 (Apr 06 2021 at 13:25):

Do we even have docs#function.graph?

#### Johan Commelin (Apr 06 2021 at 13:25):

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

#### 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

#### Adam Topaz (Apr 06 2021 at 13:28):

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

#### 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


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


is_closed_eq!

#### Sebastien Gouezel (Apr 06 2021 at 15:01):

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

#### Adam Topaz (Apr 06 2021 at 15:01):

I also didn't really know about the continuity tactic

#### 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!

#### 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