map_floor — Mathlib

English

If f is a structure-preserving map with hf strictly monotone, then ⌊f(a)⌋ = ⌊a⌋ for all a.

Русский

Пусть f — строго монотонное отображение, сохраняющее целые числа; тогда для всех a выполняется ⌊f(a)⌋ = ⌊a⌋.

LaTeX

$$$\\text{If } f: R \\to S \\text{ is strictly monotone and preserves integers, then } \\lfloor f(a) \\rfloor = \\lfloor a \\rfloor$$$

Lean4

theorem map_floor (f : F) (hf : StrictMono f) (a : R) : ⌊f a⌋ = ⌊a⌋ :=
  floor_congr fun n => by rw [← map_intCast f, hf.le_iff_le]

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