ceil_le_two_mul

Mathlib.Algebra.Order.Floor.Semifield

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

English

For a ∈ K and n ≥ 2 (i.e., n.AtLeastTwo), ⌊a / ofNat(n)⌋_+ = ⌊a⌋_+ / ofNat(n).

Русский

Для a ∈ K и n≥2: ⌊a / n⌋_+ = ⌊a⌋_+ / n.

LaTeX

$$$$ \lfloor a / \operatorname{ofNat}(n) \rfloor_+ = \lfloor a \rfloor_+ / \operatorname{ofNat}(n) $$$$

Lean4

theorem ceil_le_two_mul (ha : 2⁻¹ ≤ a) : ⌈a⌉₊ ≤ 2 * a :=
  ceil_le_mul one_lt_two (by norm_num at ha ⊢; exact ha)

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

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

Разделы

Аффилиация

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