insert_of_symmetric — Mathlib

English

From insert_of_symmetric and IsAntichain, conclude IsAntichain after symmetric conditions.

Русский

Из insert_of_symmetric и условий симметрии получаем антицепь после вставки.

LaTeX

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

Lean4

theorem insert_of_symmetric (hs : IsAntichain r s) (hr : Symmetric r) (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b) :
    IsAntichain r (insert a s) :=
  (isAntichain_insert_of_symmetric hr).2 ⟨hs, h⟩

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