eq'

Mathlib.Order.Antichain

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

English

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

Русский

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

LaTeX

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

Lean4

protected theorem eq' (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r b a) : a = b :=
  (hs.eq hb ha h).symm

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

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

Разделы

Аффилиация

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