translationNumber_eq_rat_iff — Mathlib

English

For a continuous f, τ(f) = m/n with m ∈ ℤ, n ∈ ℕ, n > 0 if and only if ∃ x, (f^n)(x) = x + m.

Русский

Для непрерывного f, τ(f) = m/n (m ∈ ℤ, n ∈ ℕ, n > 0) тогда и только тогда, когда существует x с (f^n)(x) = x + m.

LaTeX

$$$$ \\forall f, \\text{Continuous}(f) \\Rightarrow \\forall m \\in \\mathbb{Z}, \\forall n \\in \\mathbb{N}, n>0:\\tau f = \\frac{m}{n} \\iff \\exists x\\in \\mathbb{R}, (f^n)(x)=x+m. $$$$

Lean4

theorem translationNumber_eq_rat_iff (hf : Continuous f) {m : ℤ} {n : ℕ} (hn : 0 < n) :
    τ f = m / n ↔ ∃ x, (f ^ n) x = x + m :=
  by
  rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]
  exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)

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