le_of_forall_nnreal_lt — Mathlib

English

For ENNReal, equivalences between multiplying by a and dividing by its inverse under suitable conditions.

Русский

Для ENNReal эквивалентности между умножением на число и делением на его обратное при подходящих условиях.

LaTeX

$$$\\text{(conditions)} \\Rightarrow (a b \\le c \\iff a \\le b^{-1} c)$$$

Lean4

theorem le_of_forall_nnreal_lt {x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, ↑r < x → ↑r ≤ y) : x ≤ y :=
  by
  refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
  lift r to ℝ≥0 using ne_top_of_lt hr
  exact h r hr

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