mem_fixedPoints

Mathlib.Dynamics.FixedPoints.Basic

URI: https://scilib.ai/kg/mathlib#Function.mem_fixedPoints

English

If x is a fixed point of f, then f(x) is also a fixed point of f; i.e., fixed points are stable under f.

Русский

Если x фиксирована для f, то f(x) также фиксирована для f; то есть фиксированные точки устойчивы относительно f.

LaTeX

$$$IsFixedPt f x \rightarrow IsFixedPt f (f x)$$$

Lean4

@[simp]
theorem mem_fixedPoints : x ∈ fixedPoints f ↔ IsFixedPt f x :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru