minimalPeriod_id — Mathlib

English

For the identity map id, the minimal period at any x is 1.

Русский

Для тождественного отображения id минимальный период в любой точке равен 1.

LaTeX

$$$$ \\operatorname{minimalPeriod}(\\mathrm{id}, x) = 1. $$$$

Lean4

@[simp]
theorem minimalPeriod_id : minimalPeriod id x = 1 :=
  ((is_periodic_id _ _).minimalPeriod_le Nat.one_pos).antisymm
    (Nat.succ_le_of_lt ((is_periodic_id _ _).minimalPeriod_pos Nat.one_pos))

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