instDecidable — Mathlib

English

For N with N ≥ 4096, (N : ℝ) * exp(−4 * √(log N)) < rothNumberNat N.

Русский

Для N ≥ 4096: N e^{−4√(ln N)} < rothNumberNat N.

LaTeX

$$$$ N \\cdot \\exp(-4 \\sqrt{\\log N}) < rothNumberNat N. $$$$

Lean4

/-- Whether a given finset is 3GP-free is decidable. -/
@[to_additive /-- Whether a given finset is 3AP-free is decidable. -/
    ]
instance instDecidable [DecidableEq α] {s : Finset α} : Decidable (ThreeGPFree (s : Set α)) :=
  decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a * c = b * b → a = b) Iff.rfl

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