mem_fixedPoints_iff — Mathlib

English

If f is injective, then IsFixedPt f (f x) is equivalent to IsFixedPt f x; i.e., fixed-point-ness is preserved under applying f when f is injective.

Русский

Если f инъективна, то IsFixedPt f (f x) эквивалентно IsFixedPt f x; т.е. фиксированность сохраняется после применения f.

LaTeX

$$@[simp] IsFixedPt f (f x) ↔ IsFixedPt f x$$

Lean4

theorem mem_fixedPoints_iff {α : Type*} {f : α → α} {x : α} : x ∈ fixedPoints f ↔ f x = x := by rfl

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