gc_ceil_coe

Mathlib.Algebra.Order.Floor.Defs

URI: https://scilib.ai/kg/mathlib#Nat.gc_ceil_coe

English

The ceil function and the natural-inclusion map form a Galois connection: ceil(a) ≤ n if and only if a ≤ n.

Русский

Функции ceil и ввод из ℕ в α образуют связь Гало: ceil(a) ≤ n тогда и только если a ≤ n.

LaTeX

$$$\forall a \in \alpha, \forall n \in \mathbb{N}, \ ceil(a) \le n \iff a \le n$$$

Lean4

theorem gc_ceil_coe : GaloisConnection (ceil : α → ℕ) (↑) :=
  FloorSemiring.gc_ceil

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

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

Разделы

Аффилиация

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