fixedPoints_id — Mathlib

English

The membership relation between an element and the fixed point set equals the fixed-point predicate.

Русский

Принадлежность элемента к множеству фиксированных точек совпадает с фиксацией предиката фиксированной точки.

LaTeX

$$$x \in fixedPoints f \iff IsFixedPt f x$$$

Lean4

@[simp]
theorem fixedPoints_id : fixedPoints (@id α) = Set.univ :=
  Set.ext fun _ => by simpa using isFixedPt_id _

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