English
If s is closed and f,g are continuous on s, then the set {x ∈ s | f(x) = g(x)} is closed.
Русский
Если s закрыто и f,g непрерывны на s, то множество {x ∈ s | f(x) = g(x)} закрыто.
LaTeX
$$$ \\text{IsClosed}(s) \\Rightarrow (\\text{ContinuousOn}(f,s) \\land \\text{ContinuousOn}(g,s)) \\Rightarrow IsClosed(\\{x\\in s\\mid f(x)=g(x)\\})$$$
Lean4
/-- If functions `f` and `g` are continuous on a closed set `s`,
then the set of points `x ∈ s` such that `f x = g x` is a closed set. -/
protected theorem isClosed_eq [T2Space Y] {f g : X → Y} {s : Set X} (hs : IsClosed s) (hf : ContinuousOn f s)
(hg : ContinuousOn g s) : IsClosed ({x ∈ s | f x = g x}) :=
(hf.prodMk hg).preimage_isClosed_of_isClosed hs isClosed_diagonal
