gc_smul_ceilDiv

Mathlib.Algebra.Order.Floor.Div

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

English

If a > 0, the maps b ↦ b ⌈/⌉ a and x ↦ a ⋅ x form an adjunction on β.

Русский

Если a > 0, отображения b ↦ b ⌈/⌉ a и x ↦ a ⋅ x образуют adjunction на β.

LaTeX

$$$ ha > 0 \\\\Rightarrow \\\\text{GaloisConnection}(\\\\lambda b: b \\\\lceil/ a \\\\rceil, \\\\lambda x: a \\\\cdot x).$$$

Lean4

theorem gc_smul_ceilDiv (ha : 0 < a) : GaloisConnection (· ⌈/⌉ a) (a • · : β → β) :=
  CeilDiv.ceilDiv_gc ha

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

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

Разделы

Аффилиация

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