le_of_forall_lt_one_mul_le — Mathlib

English

If for all a < 1 we have a x ≤ y, then x ≤ y.

Русский

Если для всех a < 1 верно a x ≤ y, то x ≤ y.

LaTeX

$$$\forall x,y \in \mathbb{R}_{\ge 0},\ (\forall a < 1,\ a x \le y)\Rightarrow x \le y$$$

Lean4

theorem le_of_forall_lt_one_mul_le {x y : ℝ≥0} (h : ∀ a < 1, a * x ≤ y) : x ≤ y :=
  le_of_forall_lt_imp_le_of_dense fun a ha =>
    by
    have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha)
    have hx' : x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]
    have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
    have : a * x⁻¹ * x ≤ y := h _ this
    rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this

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