ceil_eq_floor_add_one_iff_notMem — Mathlib

English

For any real a, ⌈a⌉ = ⌊a⌋ + 1 if and only if a is not an integer.

Русский

Для любого вещественного a верно: ⌈a⌉ = ⌊a⌋ + 1 тогда и только тогда, когда a не целое.

LaTeX

$$$\\lceil a \\rceil = \\lfloor a \\rfloor + 1 \\iff a \\notin \\mathbb{Z}$$$

Lean4

theorem ceil_eq_floor_add_one_iff_notMem (a : R) : ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast :=
  by
  refine ⟨fun h ht => ?_, fun h => ?_⟩
  · have := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
    linarith [Int.cast_inj.mp this]
  · apply le_antisymm (Int.ceil_le_floor_add_one _)
    rw [Int.add_one_le_ceil_iff]
    exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))

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