isInt_intCeil — Mathlib

English

Let R be a ring with linear order, IsStrictOrderedRing, FloorRing. If r is an integer m, then ⌈r⌉ is an integer m as well; i.e. IsInt r m → IsInt ⌈r⌉ m.

Русский

Пусть R — кольцо с линейным порядком, IsStrictOrderedRing и FloorRing. Если r целое m, то ⌈r⌉ целое m.

LaTeX

$$$$ \\text{IsInt } r\, m \\rightarrow \\text{IsInt } \\lceil r \\rceil\, m. $$$$

Lean4

theorem isInt_intCeil {R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : ℤ) :
    IsInt r m → IsInt ⌈r⌉ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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