gc_floorDiv_smul — Mathlib

English

If a > 0, the maps x ↦ a ⋅ x and y ↦ y ⌊/⌋ a form an adjunction on β.

Русский

Если a > 0, отображения x ↦ a ⋅ x и y ↦ y ⌊/⌋ a образуют Галуа-связь на β.

LaTeX

$$$ ha > 0 \\\\Rightarrow \\\\text{GaloisConnection}(\\\\lambda x: a \\\\cdot x, \\\\lambda y: y \\\\ll floor / a \\\\rr).$$$

Lean4

theorem gc_floorDiv_smul (ha : 0 < a) : GaloisConnection (a • · : β → β) (· ⌊/⌋ a) :=
  FloorDiv.floorDiv_gc ha

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