exists_forall_sphere_dist_add_le_two_sub

English

In a uniformly convex space, for any ε>0 there exists δ>0 such that for unit vectors x,y with ‖x−y‖≥ε, we have ‖x+y‖≤2−δ.

Русский

В равномерно выпуклом пространстве для любого ε>0 существует δ>0 такой, что для любых единичных векторов x,y с ‖x−y‖≥ε выполняется ‖x+y‖≤2−δ.

LaTeX

$$∃δ>0, ∀ x,y: ‖x‖=‖y‖=1 ⇒ ‖x−y‖≥ε ⇒ ‖x+y‖≤2−δ$$

Lean4

theorem exists_forall_sphere_dist_add_le_two_sub (hε : 0 < ε) :
    ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ :=
  UniformConvexSpace.uniform_convex hε

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