eq

Mathlib.Order.Antichain

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

English

If s is an antichain and a,b ∈ s with r a b, then a = b.

Русский

Если s — антицепь и a,b ∈ s с r a b, то a = b.

LaTeX

$$$IsAntichain(r,s) \Rightarrow (a \in s) \land (b \in s) \land r(a,b) \Rightarrow a=b$$$

Lean4

protected theorem eq (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r a b) : a = b :=
  Set.Pairwise.eq hs ha hb <| not_not_intro h

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

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

Разделы

Аффилиация

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