sphere_zero_right

Mathlib.Combinatorics.Additive.AP.Three.Behrend

URI: https://scilib.ai/kg/mathlib#Behrend.sphere_zero_right

English

For any n,k, the sphere in dimension n+1 with radius parameter r = 0 is empty: sphere(n+1,0,k) = ∅.

Русский

Для любой размерности n+1 сфера с радиусом r = 0 пуста: sphere(n+1,0,k) = ∅.

LaTeX

$$$$ \mathrm{sphere}(n+1,0,k) = \emptyset $$$$

Lean4

@[simp]
theorem sphere_zero_right (n k : ℕ) : sphere (n + 1) 0 k = ∅ := by simp [sphere]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru