map_ceil

Mathlib.Algebra.Order.Floor.Semiring

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

English

If f is strictly monotone and preserves structure, then ceil of f(a) equals ceil of a: ⌈f(a)⌉ = ⌈a⌉.

Русский

Если f строго монотонен и сохраняет структуру, то ⌈f(a)⌉ = ⌈a⌉.

LaTeX

$$$$ \\lceil f(a) \\rceil = \\lceil a \\rceil $$$$

Lean4

theorem map_ceil (f : F) (hf : StrictMono f) (a : R) : ⌈f a⌉₊ = ⌈a⌉₊ :=
  ceil_congr fun n => by rw [← map_natCast f, hf.le_iff_le]

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

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

Разделы

Аффилиация

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