le_floor_iff' — Mathlib

English

For any x ∈ R, 1 ≤ floor(x) ⇔ 1 ≤ x.

Русский

Для любого x ∈ R верно: 1 ≤ ⌊x⌋₊ ⇔ 1 ≤ x.

LaTeX

$$$1 \le \lfloor x \rfloor_+ \ \Leftrightarrow \ 1 \le x$$$

Lean4

theorem le_floor_iff' (hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ (n : R) ≤ a :=
  by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact
      iff_of_false (Nat.pos_of_ne_zero hn).not_ge (not_le_of_gt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)
  · exact le_floor_iff ha

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