map_ceil — Mathlib

English

If f is strictly monotone and preserves integers, then ⌈f(a)⌉ = ⌈a⌉ for all a.

Русский

Если f строго возрастает и сохраняет целые, то ⌈f(a)⌉ = ⌈a⌉.

LaTeX

$$$\\text{If } f: R \\to S \\text{ is strictly monotone and preserves integers, then } \\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_intCast f, hf.le_iff_le]

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