singleton

Mathlib.Order.Antichain

URI: https://scilib.ai/kg/mathlib#IsAntichain.singleton

English

A singleton set {a} is an antichain with respect to any relation r.

Русский

Множество-одиночка {a} является антицепью относительно любого отношения r.

LaTeX

$$$IsAntichain(r, \{a\})$$$

Lean4

@[simp]
protected theorem singleton : IsAntichain r { a } :=
  pairwise_singleton _ _

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

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

Разделы

Аффилиация

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