le_iff_forall_one_lt_le_mul₀ — Mathlib

English

Let a, b be nonnegative with a function b? between, then a ≤ b iff for all ε > 1, a ≤ b ε.

Русский

Пусть a, b ≥ 0; тогда a ≤ b тогда и только тогда, когда для всех ε > 1 выполняется a ≤ b ε.

LaTeX

$$$0 \le b \Rightarrow (a \le b) \iff \forall \varepsilon > 1, a \le b \varepsilon$$$

Lean4

theorem le_iff_forall_one_lt_le_mul₀ {α : Type*} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α}
    (hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε :=
  by
  refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩
  obtain rfl | hb := hb.eq_or_lt
  · simp_rw [zero_mul] at h
    exact h 2 one_lt_two
  refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_
  convert h (x / b) ((one_lt_div hb).mpr hbx)
  rw [mul_div_cancel₀ _ hb.ne']

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