abs_le_floor_nnreal_iff — Mathlib

English

For z ∈ ℤ and c ∈ ℝ≥0, |z| ≤ ⌊c⌋₊ if and only if ∥z∥₊ ≤ c.

Русский

Для z ∈ ℤ и c ∈ ℝ≥0 выполняется |z| ≤ ⌊c⌋₊ тогда и только тогда, когда ∥z∥₊ ≤ c.

LaTeX

$$$|z| \le \lfloor c \rfloor_{+} \ \\Leftrightarrow \\ \|z\|_{+} \le c$$$

Lean4

theorem abs_le_floor_nnreal_iff (z : ℤ) (c : ℝ≥0) : |z| ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c := by
  rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff (zero_le c), NNReal.natCast_natAbs z]

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