floor_eq_iff' — Mathlib

English

For n ≠ 0, ⌊a⌋₊ = n iff (n : R) ≤ a and a < (n : R) + 1.

Русский

Для n ≠ 0, ⌊a⌋₊ = n тогда и только тогда, когда (n : R) ≤ a и a < (n : R) + 1.

LaTeX

$$hn \neq 0 \Rightarrow (\lfloor a \rfloor_+ = n \iff (n : R) \le a \wedge a < (n : R) + 1)$$

Lean4

theorem floor_eq_iff' (hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 := by
  rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]

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