isAntichain_insert_of_symmetric — Mathlib

English

If r is symmetric, then inserting a into s yields an antichain iff s is an antichain and a is not related to any element of s.

Русский

Если r симметрично, то вставка a в s дает антицепь тогда и только тогда, когда s — антицепь и a не связано с ни одним элементом s.

LaTeX

$$$IsAntichain(r, \text{insert } a s) \iff IsAntichain(r,s) \land \forall b\in s, a \neq b \rightarrow \neg r(a,b)$$$

Lean4

theorem _root_.isAntichain_insert_of_symmetric (hr : Symmetric r) :
    IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b :=
  pairwise_insert_of_symmetric hr.compl

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