lt_translationNumber_of_forall_add_lt

English

For any f and x, τ(f) ≤ ⌈f(x) − x⌉.

Русский

Для любого f и x, τ(f) ≤ ⌈f(x) − x⌉.

LaTeX

$$$$ \\forall f, \\forall x \\in \\mathbb{R}, \\tau f \\le \\lceil f(x) - x \\rceil. $$$$

Lean4

theorem lt_translationNumber_of_forall_add_lt (hf : Continuous f) {z : ℝ} (hz : ∀ x, x + z < f x) : z < τ f :=
  by
  obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
  refine lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) ?_
  apply le_translationNumber_of_add_le
  simp only [← le_sub_iff_add_le']
  exact f.forall_map_sub_of_Icc _ hx

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