isClosed_eq — Mathlib

English

If X is Hausdorff, the set {y | f(y) ≠ g(y)} is open whenever f,g are continuous.

Русский

Если X Хаусдорфово, множество {y | f(y) ≠ g(y)} открыто, когда f,g непрерывны.

LaTeX

$$$ \\forall X\\,Y\\,[TopologicalSpace X][TopologicalSpace Y], [T2Space X], \\{f,g:Y\\to X\\},\\ hf: Continuous f, hg: Continuous g \\Rightarrow IsOpen(\\{y\\in Y\\mid f(y) \\neq g(y)\\})$$$

Lean4

theorem isClosed_eq [T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) : IsClosed {y : Y | f y = g y} :=
  continuous_iff_isClosed.mp (hf.prodMk hg) _ isClosed_diagonal

Похожие утверждения