forall_map_sub_of_Icc — Mathlib

English

For continuous f, τ(f) equals an integer m if and only if there exists x with f(x) = x + m.

Русский

Пусть f непрерывно. Тогда τ(f) равно целому m тогда и только тогда, когда существует x с f(x) = x + m.

LaTeX

$$$$ \\forall f \\ (hf : Continuous f), \\forall m \\in \\mathbb{Z},\\; \\tau f = m \\;\\Leftrightarrow \\; \\exists x \\in \\mathbb{R},\\; f(x) = x + m. $$$$

Lean4

/-- If a predicate depends only on `f x - x` and holds for all `0 ≤ x ≤ 1`,
then it holds for all `x`. -/
theorem forall_map_sub_of_Icc (P : ℝ → Prop) (h : ∀ x ∈ Icc (0 : ℝ) 1, P (f x - x)) (x : ℝ) : P (f x - x) :=
  f.map_fract_sub_fract_eq x ▸ h _ ⟨fract_nonneg _, le_of_lt (fract_lt_one _)⟩

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