not_isCorner_empty

Mathlib.Combinatorics.Additive.Corner.Defs

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

English

There are no corners in the empty set: IsCorner ∅ x1 y1 x2 y2 is false for all x1,y1,x2,y2.

Русский

В пустом множестве нет углов: IsCorner ∅ x1 y1 x2 y2 ложно для любых x1,y1,x2,y2.

LaTeX

$$¬ IsCorner (∅) x1 y1 x2 y2$$

Lean4

@[simp]
theorem not_isCorner_empty : ¬IsCorner ∅ x₁ y₁ x₂ y₂ := by simp [isCorner_iff]

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

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

Разделы

Аффилиация

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