threeGPFree

Mathlib.Combinatorics.Additive.AP.Three.Defs

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.threeGPFree

English

If s is a singleton or sub singleton, then s is ThreeGPFree.

Русский

Если s — подмножество или множество из одной точки, тогда оно 3GPFree.

LaTeX

$$$$ \\text{ThreeGPFree}(s) \\quad\\text{если } s \\text{ является subsingleton.} $$$$

Lean4

@[to_additive]
theorem threeGPFree (hs : s.Subsingleton) : ThreeGPFree s := fun _ ha _ hb _ _ _ ↦ hs ha hb

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

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

Разделы

Аффилиация

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