isAntichain_insert — Mathlib

English

IsAntichain r (insert a s) holds iff IsAntichain r s holds and a is incomparable to every b ∈ s (in both directions).

Русский

IsAntichain r (insert a s) эквивалентно IsAntichain r s и для каждого b ∈ s верно, что a не сопоставимо с b в обе стороны.

LaTeX

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

Lean4

theorem _root_.isAntichain_insert :
    IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b ∧ ¬r b a :=
  Set.pairwise_insert

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