fract_div_mul_self_mem_Ico

Mathlib.Algebra.Order.Floor.Ring

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

← MathLib Explorer

English

For any a,b with a > 0, fract(b/a) · a ∈ [0,a).

Русский

Для любых a,b с a > 0: fract(b/a) · a ∈ [0,a).

LaTeX

$$$\\\\operatorname{fract}(\\\\frac{b}{a}) \\\\cdot a \\\\in \\\\mathrm{Ico}(0,a)$$$

Lean4

theorem fract_div_mul_self_mem_Ico (a b : k) (ha : 0 < a) : fract (b / a) * a ∈ Ico 0 a :=
  ⟨(mul_nonneg_iff_of_pos_right ha).2 (fract_nonneg (b / a)), (mul_lt_iff_lt_one_left ha).2 (fract_lt_one (b / a))⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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