isNat_intCeil — Mathlib

English

Let R be a ring with linear order, IsStrictOrderedRing, and FloorRing. If r is a natural number m, then ⌈r⌉ is also m; i.e. IsNat r m → IsNat ⌈r⌉ m.

Русский

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

LaTeX

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

Lean4

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

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