toIocDiv_eq_of_sub_zsmul_mem_Ioc

Mathlib.Algebra.Order.ToIntervalMod

URI: https://scilib.ai/kg/mathlib#toIocDiv_eq_of_sub_zsmul_mem_Ioc

← MathLib Explorer

English

If b − n·p ∈ Ioc a (a+p], then toIocDiv hp a b = n.

Русский

Если b − n·p ∈ Ioc a (a+p], то toIocDiv hp a b = n.

LaTeX

$$$ b - n p \in (a, a+p] \Rightarrow \mathrm{toIocDiv}(hp,a,b) = n $$$

Lean4

theorem toIocDiv_eq_of_sub_zsmul_mem_Ioc (h : b - n • p ∈ Set.Ioc a (a + p)) : toIocDiv hp a b = n :=
  ((existsUnique_sub_zsmul_mem_Ioc hp b a).choose_spec.2 _ h).symm

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

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

Разделы

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

Аффилиация

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