isCornerFree_empty

Mathlib.Combinatorics.Additive.Corner.Defs

URI: https://scilib.ai/kg/mathlib#isCornerFree_empty

English

The empty set is corner-free.

Русский

Пустое множество является угольно-безопасным.

LaTeX

$$IsCornerFree (∅ : Set (G × G))$$

Lean4

theorem isCornerFree_empty : IsCornerFree (∅ : Set (G × G)) :=
  subsingleton_empty.isCornerFree

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

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

Разделы

Аффилиация

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