delta_lt_false — Mathlib

English

There are no natural numbers a,b with delta·a < b and delta·b < a; such a pair leads to a contradiction.

Русский

Не существует натуральных a,b таких, что delta·a < b и delta·b < a; такое сочетание приводит к противоречию.

LaTeX

$$$\\forall a,b:\\ \\mathbb{N},\\ delta a < b \\land delta b < a \\Rightarrow \\mathrm{False}$$$

Lean4

theorem delta_lt_false {a b : ℕ} (h₁ : delta * a < b) (h₂ : delta * b < a) : False :=
  not_le_of_gt (lt_trans (mul_lt_mul_of_pos_left h₁ <| by decide) h₂) <| by
    simpa [mul_assoc] using Nat.mul_le_mul_right a (by decide : 1 ≤ delta * delta)

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