not_lt

Mathlib.Order.Antichain

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

English

If s is an antichain in a preorder, then for any a,b ∈ s one cannot have a < b.

Русский

Если s — антицепочкой в предфиксированном порядке, то для любых a,b ∈ s нельзя иметь a < b.

LaTeX

$$¬(a < b) whenever a,b ∈ s and s is an antichain$$

Lean4

theorem not_lt (hs : IsAntichain (· ≤ ·) s) (ha : a ∈ s) (hb : b ∈ s) : ¬a < b := fun h => hs ha hb h.ne h.le

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

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

Разделы

Аффилиация

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