floor_of_nonpos

Mathlib.Algebra.Order.Floor.Semiring

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

English

For a fixed a ∈ R and n ∈ ℕ with n ≠ 0, n ≤ ⌊a⌋₊ iff (n : R) ≤ a.

Русский

Для данного a и n ≠ 0 выполняется: n ≤ ⌊a⌋₊ ⇔ (n : R) ≤ a.

LaTeX

$$$n \neq 0 \Rightarrow (n \le \lfloor a \rfloor_+ \leftrightarrow (n : R) \le a)$$$

Lean4

theorem floor_of_nonpos (ha : a ≤ 0) : ⌊a⌋₊ = 0 :=
  ha.lt_or_eq.elim FloorSemiring.floor_of_neg <| by
    rintro rfl
    exact floor_zero

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

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

Разделы

Аффилиация

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