empty

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#IsChain.empty

English

The empty set is a chain with respect to any relation r.

Русский

Пустое множество является цепью относительно любой связи r.

LaTeX

$$$\operatorname{IsChain}(r, \emptyset)$$$

Lean4

@[simp]
theorem empty : IsChain r ∅ :=
  pairwise_empty _

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

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

Разделы

Аффилиация

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