le_floor_iff

Mathlib.Algebra.Order.Floor.Defs

URI: https://scilib.ai/kg/mathlib#Nat.le_floor_iff

English

For any a ∈ α with a ≥ 0, n ≤ ⌊a⌋₊ is equivalent to n ≤ a (as elements of α).

Русский

Для a ∈ α с a ≥ 0 верно: n ≤ ⌊a⌋₊ эквивалентно n ≤ a (в α).

LaTeX

$$$\forall a \in \alpha,\ a \ge 0 \Rightarrow (n \le \lfloor a \rfloor_{+} \iff n \le a)$$$

Lean4

theorem le_floor_iff (ha : 0 ≤ a) : n ≤ ⌊a⌋₊ ↔ (n : α) ≤ a :=
  FloorSemiring.gc_floor ha

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru