bound_aux' — Mathlib

English

Same as 82758: on the box set {x : Fin n → ℕ | ∀ i, x i < d}, map(d) is injective.

Русский

Та же формула, что и в пункте 82758: на множестве коробки x: Fin n → ℕ, удовлетворяющем ∀i x(i) < d, отображение map(d) инъективно.

LaTeX

$$$ {x : Fin n → ℕ \\mid \\forall i, x i < d}.InjOn (map d) $$$

Lean4

theorem bound_aux' (n d : ℕ) : ((d ^ n :) / (n * d ^ 2 :) : ℝ) ≤ rothNumberNat ((2 * d - 1) ^ n) :=
  let ⟨_, h⟩ := exists_large_sphere n d
  h.trans <| cast_le.2 <| card_sphere_le_rothNumberNat _ _ _

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