floor_congr — Mathlib

English

If ∀ n ∈ ℤ, (n ≤ a) ⇔ (n ≤ b), then ⌊a⌋ = ⌊b⌋.

Русский

Если для всех n ∈ ℤ выполняется n ≤ a ⇔ n ≤ b, то ⌊a⌋ = ⌊b⌋.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; (n \\le a) \\iff (n \\le b) \\Rightarrow \\lfloor a \\rfloor = \\lfloor b \\rfloor$$$

Lean4

theorem floor_congr (h : ∀ n : ℤ, (n : R) ≤ a ↔ (n : S) ≤ b) : ⌊a⌋ = ⌊b⌋ :=
  (le_floor.2 <| (h _).1 <| floor_le _).antisymm <| le_floor.2 <| (h _).2 <| floor_le _

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