le_of_forall_lt_one_mul_le — Mathlib

English

Let x, y be elements of the extended nonnegative reals. If for every a with 0 ≤ a < 1 we have a · x ≤ y, then x ≤ y.

Русский

Пусть x, y принадлежатрасширенным неотрицательным вещественным числам. Если для каждого a с 0 ≤ a < 1 выполняется a · x ≤ y, то x ≤ y.

LaTeX

$$$\\left(\\forall a \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\ a < 1 \\Rightarrow a \\cdot x \\le y\\right) \\Rightarrow x \\le y.$$$

Lean4

theorem le_of_forall_lt_one_mul_le {x y : ℝ≥0∞} (h : ∀ a < 1, a * x ≤ y) : x ≤ y :=
  by
  have : Tendsto (· * x) (𝓝[<] 1) (𝓝 (1 * x)) :=
    (ENNReal.continuousAt_mul_const (Or.inr one_ne_zero)).mono_left inf_le_left
  rw [one_mul] at this
  exact le_of_tendsto this (eventually_nhdsWithin_iff.2 <| Eventually.of_forall h)

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