ofDist_aux — Mathlib

English

For any ε > 0 there exists δ > 0 such that for all x<δ and y<δ, x+y<ε.

Русский

Для любого ε>0 существует δ>0 такое, что для всех x<δ и y<δ выполняется x+y<ε.

LaTeX

$$$\exists \delta>0, \forall x<\delta, \forall y<\delta, x+y<\varepsilon$$$

Lean4

theorem ofDist_aux (ε : ℝ) (hε : 0 < ε) : ∃ δ > (0 : ℝ), ∀ x < δ, ∀ y < δ, x + y < ε :=
  ⟨ε / 2, half_pos hε, fun _x hx _y hy => add_halves ε ▸ add_lt_add hx hy⟩

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