eq

Mathlib.Order.Antichain

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

English

If s is a weak antichain, then for any a,b ∈ s, if a ≺ b, then a = b.

Русский

Если s является слабой антицепью, то для любых a,b ∈ s, если a ≺ b, то a = b.

LaTeX

$$$\\text{IsWeakAntichain}(s) \\Rightarrow \\forall a \\in s, \\forall b \\in s, a \\prec b \\Rightarrow a = b$$$

Lean4

protected theorem eq (hs : IsWeakAntichain s) : a ∈ s → b ∈ s → a ≺ b → a = b :=
  IsAntichain.eq hs

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

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

Разделы

Аффилиация

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