isOpen_ne_fun — Mathlib

English

As above: the set {y | f(y) ≠ g(y)} is open when f,g are continuous and X is Hausdorff.

Русский

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

LaTeX

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

Lean4

theorem isOpen_ne_fun [T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) : IsOpen {y : Y | f y ≠ g y} :=
  isOpen_compl_iff.mpr <| isClosed_eq hf hg

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