exists_eq_add_translationNumber — Mathlib

English

If f is a continuous monotone map ℝ → ℝ and f(x+1) = f(x) + 1, then there exists x with f(x) = x + τ(f).

Русский

Если f непрерывно монотонно отображает ℝ в ℝ и выполняет f(x+1) = f(x) + 1, то существует x, такое что f(x) = x + τ(f).

LaTeX

$$$$ \\text{If } hf:\\text{Continuous } f, \\text{ and } f(x+1)=f(x)+1,\\ exists\\ x\\in \\mathbb{R},\\ f(x)=x+\\tau f. $$$$

Lean4

/-- If `f` is a continuous monotone map `ℝ → ℝ`, `f (x + 1) = f x + 1`, then there exists `x`
such that `f x = x + τ f`. -/
theorem exists_eq_add_translationNumber (hf : Continuous f) : ∃ x, f x = x + τ f :=
  by
  obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by
    by_contra! H
    exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
  obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by
    by_contra! H
    exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)
  exact intermediate_value_univ₂ hf (continuous_id.add continuous_const) ha hb

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