ceil_congr — Mathlib

English

If a and b satisfy that for all natural n, a ≤ n ↔ b ≤ n, then ⌈a⌉ = ⌈b⌉.

Русский

Если для всех натуральных n выполняется a ≤ n ↔ b ≤ n, то ⌈a⌉ = ⌈b⌉.

LaTeX

$$$$ \\forall n, (a \\le n) \\iff (b \\le n) \\Rightarrow \\lceil a \\rceil = \\lceil b \\rceil $$$$

Lean4

theorem ceil_congr (h : ∀ n : ℕ, a ≤ n ↔ b ≤ n) : ⌈a⌉₊ = ⌈b⌉₊ :=
  (ceil_le.2 <| (h _).2 <| le_ceil _).antisymm <| ceil_le.2 <| (h _).1 <| le_ceil _

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