insert — Mathlib

English

If hs is an antichain and a is incomparable to every b ∈ s, then inserting a preserves the antichain property.

Русский

Если hs — антицепь и a несопоставимо с каждым b ∈ s, то добавление a сохраняет антицепь.

LaTeX

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

Lean4

protected theorem insert (hs : IsAntichain r s) (hl : ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r b a)
    (hr : ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b) : IsAntichain r (insert a s) :=
  isAntichain_insert.2 ⟨hs, fun _ hb hab => ⟨hr hb hab, hl hb hab⟩⟩

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