le_of_forall_pos_nnreal_lt — Mathlib

English

If every NNReal r with r > 0 that is less than x also satisfies r ≤ y, then x ≤ y.

Русский

Если для каждого NNReal r > 0, который меньше x, выполнено r ≤ y, то x ≤ y.

LaTeX

$$$\\forall r \\in \\mathbb{NNReal},\\; 0 < r \\Rightarrow (r < x \\Rightarrow r \\le y) \\Rightarrow x \\le y$$$

Lean4

theorem le_of_forall_pos_nnreal_lt {x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, 0 < r → ↑r < x → ↑r ≤ y) : x ≤ y :=
  le_of_forall_nnreal_lt fun r hr => (zero_le r).eq_or_lt.elim (fun h => h ▸ zero_le _) fun h0 => h r h0 hr

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