le_of_forall_pos_le_add — Mathlib

English

If for all ε > 0 there holds b < ∞ and a ≤ b + ε, then a ≤ b.

Русский

Если для всех ε > 0 выполняется b < ∞ и a ≤ b + ε, тогда a ≤ b.

LaTeX

$$$ (h : \forall \varepsilon : \mathbb{R}_{\\ge 0}, 0 < \varepsilon \Rightarrow b < \infty \Rightarrow a \le b + \varepsilon) \Rightarrow a \le b $$$

Lean4

theorem le_of_forall_pos_le_add (h : ∀ ε : ℝ≥0, 0 < ε → b < ∞ → a ≤ b + ε) : a ≤ b :=
  by
  contrapose! h
  rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩
  exact ⟨r, hr0, h.trans_le le_top, hr⟩

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