restricted set of equality points is closed

Stream: Is there code for X?

[Bhavik Mehta]

lemma is_closed_sep_eq {α β : Type*} [topological_space α] [topological_space β] [t2_space α]
  {f g : β → α} {s : set β} (hs : is_closed s)
  (hf : continuous_on f s) (hg : continuous_on g s) : is_closed {x ∈ s | f x = g x} :=

is this in mathlib somewhere? I have a proof (using docs#is_closed_eq), but it's pretty unpleasant:

lemma is_closed_sep_eq {α β : Type*} [topological_space α] [topological_space β] [t2_space α]
  {f g : β → α} {s : set β} (hs : is_closed s)
  (hf : continuous_on f s) (hg : continuous_on g s) : is_closed {x ∈ s | f x = g x} :=
begin
  have := is_closed_eq
    (continuous_on_iff_continuous_restrict.1 hf) (continuous_on_iff_continuous_restrict.1 hg),
  obtain ⟨u, hu, hu'⟩ := is_closed_induced_iff.1 this,
  have : s ∩ u = {x ∈ s | f x = g x},
  { ext i,
    apply and_congr_right,
    rw set.ext_iff at hu',
    simp only [mem_preimage, restrict_apply, mem_set_of_eq, set_coe.forall, subtype.coe_mk] at hu',
    exact hu' _ },
  rw ←this,
  apply is_closed.inter hs hu,
end

[Anatole Dedecker]

import topology.separation

open set

lemma is_closed_sep_eq {α β : Type*} [topological_space α] [topological_space β] [t2_space α]
  {f g : β → α} {s : set β} (hs : is_closed s)
  (hf : continuous_on f s) (hg : continuous_on g s) : is_closed {x ∈ s | f x = g x} :=
begin
  change is_closed (s ∩ {x | f x = g x}),
  rw continuous_on_iff_continuous_restrict at hf hg,
  rw [inter_comm, ← subtype.image_preimage_coe],
  exact (closed_embedding_subtype_coe hs).is_closed_map _ (is_closed_eq hf hg),
end

[Anatole Dedecker]

The key is docs#closed_embedding_subtype_coe

[Ruben Van de Velde]

Anatole Dedecker said:

  change is_closed (s ∩ {x | f x = g x}),

I hope there's a lemma for that :)

[Yaël Dillies]

docs#set.sep_mem_eq?

[Yaël Dillies]

Hmm.. it would rather be set.inter_set_of, but that doesn't exist.

[Anatole Dedecker]

Ruben Van de Velde said:

Anatole Dedecker said:

  change is_closed (s ∩ {x | f x = g x}),

I hope there's a lemma for that :)

I couldn't find it :(

[Anatole Dedecker]

Yaël Dillies said:

Hmm.. it would rather be set.inter_set_of, but that doesn't exist.

I would say set.sep_set_of but that doesn't exist either...

[Yaël Dillies]

There's never the sep of a set_of in your context, right?

[Anatole Dedecker]

Oh yeah forget it :face_palm: