floor_lt

Mathlib.Algebra.Order.Floor.Defs

URI: https://scilib.ai/kg/mathlib#Int.floor_lt

English

For any a ∈ α and z ∈ ℤ, ⌊a⌋ < z if and only if a < z (embedded).

Русский

Для любых a ∈ α и z ∈ ℤ выполняется ⌊a⌋ < z тогда и только тогда, когда a < z (включая внедрение z в α).

LaTeX

$$$\forall a \in \alpha, \forall z \in \mathbb{Z},\; \lfloor a \rfloor < z \iff a < z.$$$

Lean4

theorem floor_lt : ⌊a⌋ < z ↔ a < z :=
  lt_iff_lt_of_le_iff_le le_floor

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

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

Разделы

Аффилиация

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