gc_coe_floor — Mathlib

English

There is a Galois connection between the integer embedding and the floor function: ⌊a⌋ and the inclusion of ℤ into α form a Galois connection.

Русский

Существует галуа-сопоставление между внедрением ℤ в α и функцией floor: ⌊a⌋ и вложение ℤ образуют галуа-сопоставление.

LaTeX

$$$\text{GaloisConnection}(\uparrow, \text{floor})$ between $\mathbb{Z}$ and $\alpha$.$$

Lean4

theorem gc_coe_floor : GaloisConnection ((↑) : ℤ → α) floor :=
  FloorRing.gc_coe_floor

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