gc_ceil_coe — Mathlib

English

There is a Galois connection between ceil and the integer embedding: ceil and Int.cast form a Galois connection.

Русский

Существует галуа-сопоставление между ceil и внедрением целых: ceil и Int.cast образуют галуа-сопоставление.

LaTeX

$$$\text{GaloisConnection}(\text{ceil}, (\uparrow): \mathbb{Z} \to \alpha).$$$

Lean4

theorem gc_ceil_coe : GaloisConnection ceil ((↑) : ℤ → α) :=
  FloorRing.gc_ceil_coe

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