isClosed_fixedPoints — Mathlib

English

Let α be a Hausdorff topological space and f: α → α be continuous. Then the set of fixed points Fix(f) = {x ∈ α | f(x) = x} is closed in α.

Русский

Пусть α — топологическое пространство Хаусдорфа и f: α → α непрерывна. Тогда множество неподвижных точек Fix(f) = {x ∈ α | f(x) = x} замкнуто в α.

LaTeX

$$$\operatorname{IsClosed}\bigl(\{ x \in \alpha \mid f(x) = x \} \bigr)$$$

Lean4

/-- The set of fixed points of a continuous map is a closed set. -/
theorem isClosed_fixedPoints (hf : Continuous f) : IsClosed (fixedPoints f) :=
  isClosed_eq hf continuous_id

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