minimalPeriod_eq_one_iff_isFixedPt

English

Let f: X → X be a map. For any x ∈ X, the minimal period of x under f equals 1 if and only if x is a fixed point of f (i.e., f(x) = x).

Русский

Пусть f: X → X. Для любого x ∈ X минимальный период x относительно f равен 1 тогда и только тогда, когда x фиксирован точкой f (то есть f(x) = x).

LaTeX

$$$\\operatorname{minimalPeriod}(f,x) = 1 \\iff f(x) = x$$$

Lean4

@[simp]
theorem minimalPeriod_eq_one_iff_isFixedPt : minimalPeriod f x = 1 ↔ IsFixedPt f x :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← iterate_one f]
    refine Function.IsPeriodicPt.isFixedPt ?_
    rw [← h]
    exact isPeriodicPt_minimalPeriod f x
  ·
    exact
      ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
        (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

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