sphere_subset_box — Mathlib

English

Let n, d, k be natural numbers and x a function from Fin n to the naturals. If x lies in Behrend's sphere n d k, then x lies in Behrend's box n d. In particular, the sphere is contained in the box.

Русский

Пусть n, d, k — натуральные числа, и x: Fin n → ℕ. Если x принадлежит сфере Behrend с параметрами n d k, тогда x принадлежит коробке Behrend с параметрами n d. Иначе говоря, сфера содержится в коробке.

LaTeX

$$$ sphere\\, n\\, d\\, k \\subseteq box\\, n\\, d $$$

Lean4

theorem sphere_subset_box : sphere n d k ⊆ box n d :=
  filter_subset _ _

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