decidable

Mathlib.Dynamics.FixedPoints.Basic

URI: https://scilib.ai/kg/mathlib#Function.fixedPoints.decidable

English

If x is fixed by e, then x is fixed by e^n for all n ∈ ℕ.

Русский

Если x фиксирована e, то x фиксирована для e^n при всех n ∈ ℕ.

LaTeX

$$$IsFixedPt e x \rightarrow \forall n:\mathbb{N}, IsFixedPt (e^n) x$$$

Lean4

instance decidable [DecidableEq α] (f : α → α) (x : α) : Decidable (x ∈ fixedPoints f) :=
  IsFixedPt.decidable

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

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

Разделы

Аффилиация

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