Mathlib.Order.Antichain

Symmetric.compl theorem

(h : Symmetric r) : Symmetric rᶜ

Full source

protected theorem Symmetric.compl (h : Symmetric r) : Symmetric rᶜ := fun _ _ hr hr' =>
  hr <| h hr'

Complement of Symmetric Relation is Symmetric

Informal description

If a relation $r$ on a type $\alpha$ is symmetric, then its complement relation $r^c$ (defined by $a \, r^c \, b \leftrightarrow \neg (a \, r \, b)$) is also symmetric.

IsAntichain definition

(r : α → α → Prop) (s : Set α) : Prop

Full source

/-- An antichain is a set such that no two distinct elements are related. -/
def IsAntichain (r : α → α → Prop) (s : Set α) : Prop :=
  s.Pairwise rᶜ

Antichain with respect to a relation

Informal description

A set $s$ in a type $\alpha$ is called an *antichain* with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$ if no two distinct elements in $s$ are related by $r$. In other words, for any $x, y \in s$ with $x \neq y$, the relation $r(x, y)$ does not hold.

IsAntichain.subset theorem

(hs : IsAntichain r s) (h : t ⊆ s) : IsAntichain r t

Full source

protected theorem subset (hs : IsAntichain r s) (h : t ⊆ s) : IsAntichain r t :=
  hs.mono h

Subset of an Antichain is an Antichain

Informal description

Let $s$ be an antichain with respect to a relation $r$ on a type $\alpha$. If $t$ is a subset of $s$, then $t$ is also an antichain with respect to $r$.

IsAntichain.mono theorem

(hs : IsAntichain r₁ s) (h : r₂ ≤ r₁) : IsAntichain r₂ s

Full source

theorem mono (hs : IsAntichain r₁ s) (h : r₂ ≤ r₁) : IsAntichain r₂ s :=
  hs.mono' <| compl_le_compl h

Antichain Preservation Under Weaker Relation: $r_2 \leq r_1$ Implies $s$ is $r_2$-Antichain

Informal description

Let $s$ be an antichain with respect to a relation $r_1$ on a type $\alpha$. If $r_2$ is a weaker relation than $r_1$ (i.e., $r_2 \leq r_1$), then $s$ is also an antichain with respect to $r_2$.

IsAntichain.mono_on theorem

(hs : IsAntichain r₁ s) (h : s.Pairwise fun ⦃a b⦄ => r₂ a b → r₁ a b) : IsAntichain r₂ s

Full source

theorem mono_on (hs : IsAntichain r₁ s) (h : s.Pairwise fun ⦃a b⦄ => r₂ a b → r₁ a b) :
    IsAntichain r₂ s :=
  hs.imp_on <| h.imp fun _ _ h h₁ h₂ => h₁ <| h h₂

Antichain Preservation Under Weaker Relation

Informal description

Let $s$ be a set in a type $\alpha$ that is an antichain with respect to a relation $r_1$. If for any two distinct elements $a, b \in s$, the relation $r_2(a, b)$ implies $r_1(a, b)$, then $s$ is also an antichain with respect to $r_2$.

IsAntichain.eq theorem

(hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r a b) : a = b

Full source

protected theorem eq (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r a b) :
    a = b :=
  Set.Pairwise.eq hs ha hb <| not_not_intro h

Elements in an Antichain Related by $r$ Must Be Equal

Informal description

Let $s$ be an antichain with respect to a relation $r$ on a type $\alpha$. For any two elements $a, b \in s$ such that $r(a, b)$ holds, we have $a = b$.

IsAntichain.eq' theorem

(hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r b a) : a = b

Full source

protected theorem eq' (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r b a) :
    a = b :=
  (hs.eq hb ha h).symm

Elements in an Antichain Related by Reverse $r$ Must Be Equal

Informal description

Let $s$ be an antichain with respect to a relation $r$ on a type $\alpha$. For any two elements $a, b \in s$ such that $r(b, a)$ holds, we have $a = b$.

IsAntichain.isAntisymm theorem

(h : IsAntichain r univ) : IsAntisymm α r

Full source

protected theorem isAntisymm (h : IsAntichain r univ) : IsAntisymm α r :=
  ⟨fun _ _ ha _ => h.eq trivial trivial ha⟩

Antichain Universality Implies Antisymmetry of Relation

Informal description

If the universal set on a type $\alpha$ is an antichain with respect to a relation $r$, then $r$ is an antisymmetric relation on $\alpha$. That is, for any $x, y \in \alpha$, if $r(x, y)$ and $r(y, x)$ both hold, then $x = y$.

IsAntichain.subsingleton theorem

[IsTrichotomous α r] (h : IsAntichain r s) : s.Subsingleton

Full source

protected theorem subsingleton [IsTrichotomous α r] (h : IsAntichain r s) : s.Subsingleton := by
  rintro a ha b hb
  obtain hab | hab | hab := trichotomous_of r a b
  · exact h.eq ha hb hab
  · exact hab
  · exact h.eq' ha hb hab

Antichain in Trichotomous Relation is Subsingleton

Informal description

Let $\alpha$ be a type equipped with a trichotomous relation $r$ (meaning for any $x, y \in \alpha$, exactly one of $r(x, y)$, $x = y$, or $r(y, x)$ holds). If $s$ is an antichain with respect to $r$, then $s$ is a subsingleton (i.e., contains at most one element).

IsAntichain.flip theorem

(hs : IsAntichain r s) : IsAntichain (flip r) s

Full source

protected theorem flip (hs : IsAntichain r s) : IsAntichain (flip r) s := fun _ ha _ hb h =>
  hs hb ha h.symm

Antichain Property under Relation Flip

Informal description

If a set $s$ is an antichain with respect to a relation $r$ on a type $\alpha$, then $s$ is also an antichain with respect to the flipped relation $\text{flip } r$, where $\text{flip } r(x, y) := r(y, x)$ for all $x, y \in \alpha$.

IsAntichain.swap theorem

(hs : IsAntichain r s) : IsAntichain (swap r) s

Full source

theorem swap (hs : IsAntichain r s) : IsAntichain (swap r) s :=
  hs.flip

Antichain Property under Relation Swap

Informal description

If a set $s$ is an antichain with respect to a relation $r$ on a type $\alpha$, then $s$ is also an antichain with respect to the swapped relation $\operatorname{swap} r$, where $\operatorname{swap} r(x, y) := r(y, x)$ for all $x, y \in \alpha$.

IsAntichain.image theorem

(hs : IsAntichain r s) (f : α → β) (h : ∀ ⦃a b⦄, r' (f a) (f b) → r a b) : IsAntichain r' (f '' s)

Full source

theorem image (hs : IsAntichain r s) (f : α → β) (h : ∀ ⦃a b⦄, r' (f a) (f b) → r a b) :
    IsAntichain r' (f '' s) := by
  rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr
  exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)

Image of an Antichain under a Relation-Preserving Function is an Antichain

Informal description

Let $s$ be an antichain with respect to a relation $r$ on a type $\alpha$, and let $f : \alpha \to \beta$ be a function. If for any $a, b \in \alpha$, the relation $r'(f(a), f(b))$ implies $r(a, b)$, then the image $f(s)$ is an antichain with respect to $r'$ in $\beta$.

IsAntichain.preimage theorem

 (hs : IsAntichain r s) {f : β → α} (hf : Injective f) (h : ∀ ⦃a b⦄, r' a b → r (f a) (f b)) : IsAntichain r' (f ⁻¹' s)

Full source

theorem preimage (hs : IsAntichain r s) {f : β → α} (hf : Injective f)
    (h : ∀ ⦃a b⦄, r' a b → r (f a) (f b)) : IsAntichain r' (f ⁻¹' s) := fun _ hb _ hc hbc hr =>
  hs hb hc (hf.ne hbc) <| h hr

Preimage of an Antichain under an Injective Relation-Preserving Function is an Antichain

Informal description

Let $s$ be an antichain with respect to a relation $r$ on a type $\alpha$, and let $f : \beta \to \alpha$ be an injective function. If for any $a, b \in \beta$, the relation $r'(a, b)$ implies $r(f(a), f(b))$, then the preimage $f^{-1}(s)$ is an antichain with respect to $r'$ in $\beta$.

isAntichain_insert theorem

: IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b ∧ ¬r b a

Full source

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

Characterization of Antichain Insertion: $\text{IsAntichain}\, r\, (\{a\} \cup s) \leftrightarrow \text{IsAntichain}\, r\, s \land \forall b \in s, a \neq b \to \neg r(a, b) \land \neg r(b, a)$

Informal description

For a relation $r$ on a type $\alpha$, a set $s \subseteq \alpha$, and an element $a \in \alpha$, the set $\{a\} \cup s$ is an antichain with respect to $r$ if and only if: 1. $s$ is an antichain with respect to $r$, and 2. For every $b \in s$ with $a \neq b$, neither $r(a, b)$ nor $r(b, a)$ holds.

IsAntichain.insert theorem

 (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)

Full source

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⟩⟩

Insertion Preserves Antichain Property

Informal description

Let $s$ be an antichain with respect to a relation $r$ on a type $\alpha$, and let $a \in \alpha$. If for every $b \in s$ with $a \neq b$, neither $r(a, b)$ nor $r(b, a)$ holds, then the set $\{a\} \cup s$ is also an antichain with respect to $r$.

isAntichain_insert_of_symmetric theorem

(hr : Symmetric r) : IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b

Full source

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

Characterization of Antichain Insertion for Symmetric Relations

Informal description

Let $r$ be a symmetric relation on a type $\alpha$. For any element $a \in \alpha$ and set $s \subseteq \alpha$, the set $\{a\} \cup s$ is an antichain with respect to $r$ if and only if $s$ is an antichain with respect to $r$ and for every $b \in s$ with $a \neq b$, the relation $r(a, b)$ does not hold.

IsAntichain.insert_of_symmetric theorem

 (hs : IsAntichain r s) (hr : Symmetric r) (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b) : IsAntichain r (insert a s)

Full source

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⟩

Insertion Preserves Antichain Property for Symmetric Relations

Informal description

Let $r$ be a symmetric relation on a type $\alpha$, and let $s \subseteq \alpha$ be an antichain with respect to $r$. If for every $b \in s$ with $a \neq b$, the relation $r(a, b)$ does not hold, then the set $\{a\} \cup s$ is also an antichain with respect to $r$.

IsAntichain.image_relEmbedding theorem

(hs : IsAntichain r s) (φ : r ↪r r') : IsAntichain r' (φ '' s)

Full source

theorem image_relEmbedding (hs : IsAntichain r s) (φ : r ↪r r') : IsAntichain r' (φ '' s) := by
  intro b hb b' hb' h₁ h₂
  rw [Set.mem_image] at hb hb'
  obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
  exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)

Image of an Antichain under a Relation Embedding is an Antichain

Informal description

Let $r$ and $r'$ be relations on types $\alpha$ and $\beta$ respectively, and let $\phi : r \hookrightarrow r'$ be a relation embedding. For any antichain $s \subseteq \alpha$ with respect to $r$, the image $\phi(s)$ is an antichain in $\beta$ with respect to $r'$.

IsAntichain.preimage_relEmbedding theorem

{t : Set β} (ht : IsAntichain r' t) (φ : r ↪r r') : IsAntichain r (φ ⁻¹' t)

Full source

theorem preimage_relEmbedding {t : Set β} (ht : IsAntichain r' t) (φ : r ↪r r') :
    IsAntichain r (φ ⁻¹' t) := fun _ ha _s ha' hne hle =>
  ht ha ha' (fun h => hne (φ.injective h)) (φ.map_rel_iff.mpr hle)

Preimage of an Antichain under a Relation Embedding is an Antichain

Informal description

Let $r$ and $r'$ be relations on types $\alpha$ and $\beta$ respectively, and let $\phi : r \hookrightarrow r'$ be a relation embedding. For any antichain $t \subseteq \beta$ with respect to $r'$, the preimage $\phi^{-1}(t)$ is an antichain in $\alpha$ with respect to $r$.

IsAntichain.image_relIso theorem

(hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s)

Full source

theorem image_relIso (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) :=
  hs.image_relEmbedding φ.toRelEmbedding

Image of an Antichain under a Relation Isomorphism is an Antichain

Informal description

Let $r$ and $r'$ be relations on types $\alpha$ and $\beta$ respectively, and let $\phi : r \simeq r'$ be a relation isomorphism. For any antichain $s \subseteq \alpha$ with respect to $r$, the image $\phi(s)$ is an antichain in $\beta$ with respect to $r'$.

IsAntichain.preimage_relIso theorem

{t : Set β} (hs : IsAntichain r' t) (φ : r ≃r r') : IsAntichain r (φ ⁻¹' t)

Full source

theorem preimage_relIso {t : Set β} (hs : IsAntichain r' t) (φ : r ≃r r') :
    IsAntichain r (φ ⁻¹' t) :=
  hs.preimage_relEmbedding φ.toRelEmbedding

Preimage of an Antichain under a Relation Isomorphism is an Antichain

Informal description

Let $r$ and $r'$ be relations on types $\alpha$ and $\beta$ respectively, and let $\phi : r \simeq r'$ be a relation isomorphism. For any antichain $t \subseteq \beta$ with respect to $r'$, the preimage $\phi^{-1}(t)$ is an antichain in $\alpha$ with respect to $r$.

IsAntichain.image_relEmbedding_iff theorem

{φ : r ↪r r'} : IsAntichain r' (φ '' s) ↔ IsAntichain r s

Full source

theorem image_relEmbedding_iff {φ : r ↪r r'} : IsAntichainIsAntichain r' (φ '' s) ↔ IsAntichain r s :=
  ⟨fun h => (φ.injective.preimage_image s).subst (h.preimage_relEmbedding φ), fun h =>
    h.image_relEmbedding φ⟩

Antichain Image Characterization under Relation Embedding: $s$ is antichain iff $\phi(s)$ is antichain

Informal description

Let $r$ and $r'$ be relations on types $\alpha$ and $\beta$ respectively, and let $\phi : r \hookrightarrow r'$ be a relation embedding. A subset $s \subseteq \alpha$ is an antichain with respect to $r$ if and only if its image $\phi(s) \subseteq \beta$ is an antichain with respect to $r'$.

IsAntichain.image_relIso_iff theorem

{φ : r ≃r r'} : IsAntichain r' (φ '' s) ↔ IsAntichain r s

Full source

theorem image_relIso_iff {φ : r ≃r r'} : IsAntichainIsAntichain r' (φ '' s) ↔ IsAntichain r s :=
  @image_relEmbedding_iff _ _ _ _ _ (φ : r ↪r r')

Antichain Image Characterization under Relation Isomorphism: $s$ is antichain iff $\phi(s)$ is antichain

Informal description

Let $r$ and $r'$ be relations on types $\alpha$ and $\beta$ respectively, and let $\phi : r \simeq r'$ be a relation isomorphism. A subset $s \subseteq \alpha$ is an antichain with respect to $r$ if and only if its image $\phi(s) \subseteq \beta$ is an antichain with respect to $r'$.

IsAntichain.image_embedding theorem

[LE α] [LE β] (hs : IsAntichain (· ≤ ·) s) (φ : α ↪o β) : IsAntichain (· ≤ ·) (φ '' s)

Full source

theorem image_embedding [LE α] [LE β] (hs : IsAntichain (· ≤ ·) s) (φ : α ↪o β) :
    IsAntichain (· ≤ ·) (φ '' s) :=
  image_relEmbedding hs _

Image of an Antichain under an Order Embedding is an Antichain

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets, and let $s \subseteq \alpha$ be an antichain with respect to the order $\leq$ on $\alpha$. For any order embedding $\phi : \alpha \hookrightarrow \beta$, the image $\phi(s)$ is an antichain in $\beta$ with respect to the order $\leq$ on $\beta$.

IsAntichain.preimage_embedding theorem

[LE α] [LE β] {t : Set β} (ht : IsAntichain (· ≤ ·) t) (φ : α ↪o β) : IsAntichain (· ≤ ·) (φ ⁻¹' t)

Full source

theorem preimage_embedding [LE α] [LE β] {t : Set β} (ht : IsAntichain (· ≤ ·) t) (φ : α ↪o β) :
    IsAntichain (· ≤ ·) (φ ⁻¹' t) :=
  preimage_relEmbedding ht _

Preimage of an Antichain under an Order Embedding is an Antichain

Informal description

Let $\alpha$ and $\beta$ be types equipped with partial orders $\leq_\alpha$ and $\leq_\beta$ respectively. For any antichain $t \subseteq \beta$ with respect to $\leq_\beta$ and any order embedding $\phi : \alpha \hookrightarrow \beta$, the preimage $\phi^{-1}(t)$ is an antichain in $\alpha$ with respect to $\leq_\alpha$.

IsAntichain.image_embedding_iff theorem

[LE α] [LE β] {φ : α ↪o β} : IsAntichain (· ≤ ·) (φ '' s) ↔ IsAntichain (· ≤ ·) s

Full source

theorem image_embedding_iff [LE α] [LE β] {φ : α ↪o β} :
    IsAntichainIsAntichain (· ≤ ·) (φ '' s) ↔ IsAntichain (· ≤ ·) s :=
  image_relEmbedding_iff

Antichain Characterization under Order Embedding: $s$ is antichain iff $\phi(s)$ is antichain

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets, and let $\phi : \alpha \hookrightarrow \beta$ be an order embedding. A subset $s \subseteq \alpha$ is an antichain with respect to the order $\leq$ on $\alpha$ if and only if its image $\phi(s) \subseteq \beta$ is an antichain with respect to the order $\leq$ on $\beta$.

IsAntichain.image_iso theorem

[LE α] [LE β] (hs : IsAntichain (· ≤ ·) s) (φ : α ≃o β) : IsAntichain (· ≤ ·) (φ '' s)

Full source

theorem image_iso [LE α] [LE β] (hs : IsAntichain (· ≤ ·) s) (φ : α ≃o β) :
    IsAntichain (· ≤ ·) (φ '' s) :=
  image_relEmbedding hs _

Image of an Antichain under an Order Isomorphism is an Antichain

Informal description

Let $\alpha$ and $\beta$ be types equipped with preorders $\leq_\alpha$ and $\leq_\beta$ respectively. If $s \subseteq \alpha$ is an antichain with respect to $\leq_\alpha$ and $\phi : \alpha \simeq_o \beta$ is an order isomorphism, then the image $\phi(s)$ is an antichain in $\beta$ with respect to $\leq_\beta$.

IsAntichain.image_iso_iff theorem

[LE α] [LE β] {φ : α ≃o β} : IsAntichain (· ≤ ·) (φ '' s) ↔ IsAntichain (· ≤ ·) s

Full source

theorem image_iso_iff [LE α] [LE β] {φ : α ≃o β} :
    IsAntichainIsAntichain (· ≤ ·) (φ '' s) ↔ IsAntichain (· ≤ ·) s :=
  image_relEmbedding_iff

Antichain Image Characterization under Order Isomorphism

Informal description

Let $\alpha$ and $\beta$ be types equipped with preorders $\leq_\alpha$ and $\leq_\beta$ respectively, and let $\phi : \alpha \simeq_o \beta$ be an order isomorphism. A subset $s \subseteq \alpha$ is an antichain with respect to $\leq_\alpha$ if and only if its image $\phi(s) \subseteq \beta$ is an antichain with respect to $\leq_\beta$.

IsAntichain.preimage_iso theorem

[LE α] [LE β] {t : Set β} (ht : IsAntichain (· ≤ ·) t) (φ : α ≃o β) : IsAntichain (· ≤ ·) (φ ⁻¹' t)

Full source

theorem preimage_iso [LE α] [LE β] {t : Set β} (ht : IsAntichain (· ≤ ·) t) (φ : α ≃o β) :
    IsAntichain (· ≤ ·) (φ ⁻¹' t) :=
  preimage_relEmbedding ht _

Preimage of an Antichain under an Order Isomorphism is an Antichain

Informal description

Let $\alpha$ and $\beta$ be types equipped with preorders $\leq_\alpha$ and $\leq_\beta$ respectively. Given an antichain $t \subseteq \beta$ with respect to $\leq_\beta$ and an order isomorphism $\phi : \alpha \simeq_o \beta$, the preimage $\phi^{-1}(t)$ is an antichain in $\alpha$ with respect to $\leq_\alpha$.

IsAntichain.preimage_iso_iff theorem

[LE α] [LE β] {t : Set β} {φ : α ≃o β} : IsAntichain (· ≤ ·) (φ ⁻¹' t) ↔ IsAntichain (· ≤ ·) t

Full source

theorem preimage_iso_iff [LE α] [LE β] {t : Set β} {φ : α ≃o β} :
    IsAntichainIsAntichain (· ≤ ·) (φ ⁻¹' t) ↔ IsAntichain (· ≤ ·) t :=
  ⟨fun h => (φ.image_preimage t).subst (h.image_iso φ), fun h => h.preimage_iso _⟩

Equivalence of Antichain Conditions under Order Isomorphism Preimage

Informal description

Let $\alpha$ and $\beta$ be types equipped with preorders $\leq_\alpha$ and $\leq_\beta$ respectively. Given a subset $t \subseteq \beta$ and an order isomorphism $\phi : \alpha \simeq_o \beta$, the preimage $\phi^{-1}(t)$ is an antichain in $\alpha$ with respect to $\leq_\alpha$ if and only if $t$ is an antichain in $\beta$ with respect to $\leq_\beta$.

IsAntichain.to_dual theorem

[LE α] (hs : IsAntichain (· ≤ ·) s) : @IsAntichain αᵒᵈ (· ≤ ·) s

Full source

theorem to_dual [LE α] (hs : IsAntichain (· ≤ ·) s) : @IsAntichain αᵒᵈ (· ≤ ·) s :=
  fun _ ha _ hb hab => hs hb ha hab.symm

Antichain Preservation under Order Duality

Informal description

Let $\alpha$ be a type equipped with a preorder $\leq$. If a set $s \subseteq \alpha$ is an antichain with respect to $\leq$, then $s$ is also an antichain with respect to the dual order $\geq$ on the order dual $\alpha^{\text{op}}$.

IsAntichain.to_dual_iff theorem

[LE α] : IsAntichain (· ≤ ·) s ↔ @IsAntichain αᵒᵈ (· ≤ ·) s

Full source

theorem to_dual_iff [LE α] : IsAntichainIsAntichain (· ≤ ·) s ↔ @IsAntichain αᵒᵈ (· ≤ ·) s :=
  ⟨to_dual, to_dual⟩

Equivalence of Antichain Conditions under Order Duality

Informal description

Let $\alpha$ be a type equipped with a preorder $\leq$. A set $s \subseteq \alpha$ is an antichain with respect to $\leq$ if and only if it is an antichain with respect to the dual order $\geq$ on the order dual $\alpha^{\text{op}}$.

IsAntichain.image_compl theorem

[BooleanAlgebra α] (hs : IsAntichain (· ≤ ·) s) : IsAntichain (· ≤ ·) (compl '' s)

Full source

theorem image_compl [BooleanAlgebra α] (hs : IsAntichain (· ≤ ·) s) :
    IsAntichain (· ≤ ·) (complcompl '' s) :=
  (hs.image_embedding (OrderIso.compl α).toOrderEmbedding).flip

Complement Operation Preserves Antichain Property in Boolean Algebras

Informal description

Let $\alpha$ be a Boolean algebra and $s \subseteq \alpha$ be an antichain with respect to the order relation $\leq$. Then the image of $s$ under the complement operation, $\{x^\complement \mid x \in s\}$, is also an antichain with respect to $\leq$.

IsAntichain.preimage_compl theorem

[BooleanAlgebra α] (hs : IsAntichain (· ≤ ·) s) : IsAntichain (· ≤ ·) (compl ⁻¹' s)

Full source

theorem preimage_compl [BooleanAlgebra α] (hs : IsAntichain (· ≤ ·) s) :
    IsAntichain (· ≤ ·) (complcompl ⁻¹' s) := fun _ ha _ ha' hne hle =>
  hs ha' ha (fun h => hne (compl_inj_iff.mp h.symm)) (compl_le_compl hle)

Preimage of Antichain under Complement is Antichain in Boolean Algebra

Informal description

Let $\alpha$ be a Boolean algebra and $s \subseteq \alpha$ be an antichain with respect to the order relation $\leq$. Then the preimage of $s$ under the complement operation, $\{x \in \alpha \mid x^\complement \in s\}$, is also an antichain with respect to $\leq$.

isAntichain_singleton theorem

(a : α) (r : α → α → Prop) : IsAntichain r { a }

Full source

theorem isAntichain_singleton (a : α) (r : α → α → Prop) : IsAntichain r {a} :=
  pairwise_singleton _ _

Singleton Sets are Antichains

Informal description

For any element $a$ of type $\alpha$ and any binary relation $r$ on $\alpha$, the singleton set $\{a\}$ is an antichain with respect to $r$.

Set.Subsingleton.isAntichain theorem

(hs : s.Subsingleton) (r : α → α → Prop) : IsAntichain r s

Full source

theorem Set.Subsingleton.isAntichain (hs : s.Subsingleton) (r : α → α → Prop) : IsAntichain r s :=
  hs.pairwise _

Subsingleton Sets are Antichains

Informal description

For any set $s$ in a type $\alpha$ that is a subsingleton (i.e., contains at most one element) and any binary relation $r$ on $\alpha$, the set $s$ is an antichain with respect to $r$.

subsingleton_of_isChain_of_isAntichain theorem

(hs : IsChain r s) (ht : IsAntichain r s) : s.Subsingleton

Full source

/-- A set which is simultaneously a chain and antichain is subsingleton. -/
lemma subsingleton_of_isChain_of_isAntichain (hs : IsChain r s) (ht : IsAntichain r s) :
    s.Subsingleton := by
  intro x hx y hy
  by_contra! hne
  cases hs hx hy hne with
  | inl h => exact ht hx hy hne h
  | inr h => exact ht hy hx hne.symm h

A Chain and Antichain is a Subsingleton

Informal description

For any set $s$ in a type $\alpha$ with a relation $r$, if $s$ is both a chain and an antichain with respect to $r$, then $s$ is a subsingleton (i.e., contains at most one element).

isChain_and_isAntichain_iff_subsingleton theorem

: IsChain r s ∧ IsAntichain r s ↔ s.Subsingleton

Full source

lemma isChain_and_isAntichain_iff_subsingleton : IsChainIsChain r s ∧ IsAntichain r sIsChain r s ∧ IsAntichain r s ↔ s.Subsingleton :=
  ⟨fun h ↦ subsingleton_of_isChain_of_isAntichain h.1 h.2, fun h ↦ ⟨h.isChain, h.isAntichain _⟩⟩

Characterization of Chains and Antichains as Subsingletons: $\text{IsChain}(r, s) \land \text{IsAntichain}(r, s) \leftrightarrow \text{Subsingleton}(s)$

Informal description

For any set $s$ in a type $\alpha$ with a relation $r$, the following are equivalent: 1. $s$ is both a chain and an antichain with respect to $r$. 2. $s$ is a subsingleton (i.e., contains at most one element). In other words, $s$ is simultaneously a chain and an antichain if and only if $s$ has at most one element.

inter_subsingleton_of_isChain_of_isAntichain theorem

(hs : IsChain r s) (ht : IsAntichain r t) : (s ∩ t).Subsingleton

Full source

/-- The intersection of a chain and an antichain is subsingleton. -/
lemma inter_subsingleton_of_isChain_of_isAntichain (hs : IsChain r s) (ht : IsAntichain r t) :
    (s ∩ t).Subsingleton :=
  subsingleton_of_isChain_of_isAntichain (hs.mono (by simp)) (ht.subset (by simp))

Intersection of a Chain and an Antichain is a Subsingleton

Informal description

For any relation $r$ on a type $\alpha$, if $s$ is a chain and $t$ is an antichain with respect to $r$, then the intersection $s \cap t$ is a subsingleton (i.e., contains at most one element).

inter_subsingleton_of_isAntichain_of_isChain theorem

(hs : IsAntichain r s) (ht : IsChain r t) : (s ∩ t).Subsingleton

Full source

/-- The intersection of an antichain and a chain is subsingleton. -/
lemma inter_subsingleton_of_isAntichain_of_isChain (hs : IsAntichain r s) (ht : IsChain r t) :
    (s ∩ t).Subsingleton :=
  inter_comm _ _ ▸ inter_subsingleton_of_isChain_of_isAntichain ht hs

Intersection of an Antichain and a Chain is a Subsingleton

Informal description

For any relation $r$ on a type $\alpha$, if $s$ is an antichain and $t$ is a chain with respect to $r$, then the intersection $s \cap t$ is a subsingleton (i.e., contains at most one element).

IsAntichain.not_lt theorem

(hs : IsAntichain (· ≤ ·) s) (ha : a ∈ s) (hb : b ∈ s) : ¬a < b

Full source

theorem IsAntichain.not_lt (hs : IsAntichain (· ≤ ·) s) (ha : a ∈ s) (hb : b ∈ s) : ¬a < b :=
  fun h => hs ha hb h.ne h.le

No Strict Inequality in an Antichain

Informal description

Let $s$ be an antichain with respect to the relation $\leq$ on a type $\alpha$, and let $a, b \in s$ be two distinct elements. Then $a$ is not less than $b$, i.e., $\neg(a < b)$.

isAntichain_and_least_iff theorem

: IsAntichain (· ≤ ·) s ∧ IsLeast s a ↔ s = { a }

Full source

theorem isAntichain_and_least_iff : IsAntichainIsAntichain (· ≤ ·) s ∧ IsLeast s aIsAntichain (· ≤ ·) s ∧ IsLeast s a ↔ s = {a} :=
  ⟨fun h => eq_singleton_iff_unique_mem.2 ⟨h.2.1, fun _ hb => h.1.eq' hb h.2.1 (h.2.2 hb)⟩, by
    rintro rfl
    exact ⟨isAntichain_singleton _ _, isLeast_singleton⟩⟩

Antichain with Least Element is Singleton

Informal description

For a set $s$ in a partially ordered type $\alpha$, the following are equivalent: 1. $s$ is an antichain with respect to the order relation $\leq$ and has a least element $a$. 2. $s$ is the singleton set $\{a\}$.

isAntichain_and_greatest_iff theorem

: IsAntichain (· ≤ ·) s ∧ IsGreatest s a ↔ s = { a }

Full source

theorem isAntichain_and_greatest_iff : IsAntichainIsAntichain (· ≤ ·) s ∧ IsGreatest s aIsAntichain (· ≤ ·) s ∧ IsGreatest s a ↔ s = {a} :=
  ⟨fun h => eq_singleton_iff_unique_mem.2 ⟨h.2.1, fun _ hb => h.1.eq hb h.2.1 (h.2.2 hb)⟩, by
    rintro rfl
    exact ⟨isAntichain_singleton _ _, isGreatest_singleton⟩⟩

Antichain with Greatest Element is Singleton

Informal description

For a set $s$ in a partially ordered type $\alpha$, the following are equivalent: 1. $s$ is an antichain with respect to the order relation $\leq$ and has a greatest element $a$. 2. $s$ is the singleton set $\{a\}$.

IsAntichain.least_iff theorem

(hs : IsAntichain (· ≤ ·) s) : IsLeast s a ↔ s = { a }

Full source

theorem IsAntichain.least_iff (hs : IsAntichain (· ≤ ·) s) : IsLeastIsLeast s a ↔ s = {a} :=
  (and_iff_right hs).symm.trans isAntichain_and_least_iff

Least Element Characterization for Antichains

Informal description

For an antichain $s$ with respect to the order relation $\leq$ in a partially ordered type $\alpha$, the following are equivalent: 1. $s$ has a least element $a$. 2. $s$ is the singleton set $\{a\}$.

IsAntichain.greatest_iff theorem

(hs : IsAntichain (· ≤ ·) s) : IsGreatest s a ↔ s = { a }

Full source

theorem IsAntichain.greatest_iff (hs : IsAntichain (· ≤ ·) s) : IsGreatestIsGreatest s a ↔ s = {a} :=
  (and_iff_right hs).symm.trans isAntichain_and_greatest_iff

Greatest Element Characterization for Antichains

Informal description

For an antichain $s$ with respect to the order relation $\leq$ in a partially ordered type $\alpha$, the following are equivalent: 1. $s$ has a greatest element $a$. 2. $s$ is the singleton set $\{a\}$.

IsLeast.antichain_iff theorem

(hs : IsLeast s a) : IsAntichain (· ≤ ·) s ↔ s = { a }

Full source

theorem IsLeast.antichain_iff (hs : IsLeast s a) : IsAntichainIsAntichain (· ≤ ·) s ↔ s = {a} :=
  (and_iff_left hs).symm.trans isAntichain_and_least_iff

Antichain Characterization for Sets with Least Element

Informal description

For a set $s$ in a partially ordered type $\alpha$ with a least element $a$, the following are equivalent: 1. $s$ is an antichain with respect to the order relation $\leq$. 2. $s$ is the singleton set $\{a\}$.

IsGreatest.antichain_iff theorem

(hs : IsGreatest s a) : IsAntichain (· ≤ ·) s ↔ s = { a }

Full source

theorem IsGreatest.antichain_iff (hs : IsGreatest s a) : IsAntichainIsAntichain (· ≤ ·) s ↔ s = {a} :=
  (and_iff_left hs).symm.trans isAntichain_and_greatest_iff

Antichain Characterization for Sets with Greatest Element

Informal description

For a set $s$ in a partially ordered type $\alpha$ with a greatest element $a$, the following are equivalent: 1. $s$ is an antichain with respect to the order relation $\leq$. 2. $s$ is the singleton set $\{a\}$.

IsAntichain.bot_mem_iff theorem

[OrderBot α] (hs : IsAntichain (· ≤ ·) s) : ⊥ ∈ s ↔ s = {⊥}

Full source

theorem IsAntichain.bot_mem_iff [OrderBot α] (hs : IsAntichain (· ≤ ·) s) : ⊥⊥ ∈ s⊥ ∈ s ↔ s = {⊥} :=
  isLeast_bot_iff.symm.trans hs.least_iff

Characterization of Antichains Containing the Bottom Element: $\bot \in s \leftrightarrow s = \{\bot\}$

Informal description

Let $\alpha$ be a partially ordered type with a least element $\bot$. For any antichain $s \subseteq \alpha$ with respect to the order relation $\leq$, the following are equivalent: 1. The least element $\bot$ belongs to $s$. 2. The set $s$ is the singleton $\{\bot\}$.

IsAntichain.top_mem_iff theorem

[OrderTop α] (hs : IsAntichain (· ≤ ·) s) : ⊤ ∈ s ↔ s = {⊤}

Full source

theorem IsAntichain.top_mem_iff [OrderTop α] (hs : IsAntichain (· ≤ ·) s) : ⊤⊤ ∈ s⊤ ∈ s ↔ s = {⊤} :=
  isGreatest_top_iff.symm.trans hs.greatest_iff

Characterization of Antichains Containing the Top Element: $\top \in s \leftrightarrow s = \{\top\}$

Informal description

Let $\alpha$ be a partially ordered type with a greatest element $\top$. For any antichain $s \subseteq \alpha$ with respect to the order relation $\leq$, the following are equivalent: 1. The greatest element $\top$ belongs to $s$. 2. The set $s$ is the singleton $\{\top\}$.

isAntichain_iff_forall_not_lt theorem

: IsAntichain (· ≤ ·) s ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ¬a < b

Full source

theorem isAntichain_iff_forall_not_lt :
    IsAntichainIsAntichain (· ≤ ·) s ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ¬a < b :=
  ⟨fun hs _ ha _ => hs.not_lt ha, fun hs _ ha _ hb h h' => hs ha hb <| h'.lt_of_ne h⟩

Characterization of Antichains via Strict Inequalities

Informal description

A set $s$ in a partially ordered type $\alpha$ is an antichain with respect to the order relation $\leq$ if and only if for any two elements $a, b \in s$, the strict inequality $a < b$ does not hold.

IsStrongAntichain definition

(r : α → α → Prop) (s : Set α) : Prop

Full source

/-- A strong (upward) antichain is a set such that no two distinct elements are related to a common
element. -/
def IsStrongAntichain (r : α → α → Prop) (s : Set α) : Prop :=
  s.Pairwise fun a b => ∀ c, ¬r a c¬r a c ∨ ¬r b c

Strong Antichain

Informal description

A set $s$ in a type $\alpha$ is called a *strong antichain* with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$ if for any two distinct elements $a, b \in s$, there is no common element $c$ such that both $r(a, c)$ and $r(b, c)$ hold. In other words, for all $a, b \in s$ with $a \neq b$, and for all $c \in \alpha$, either $\neg r(a, c)$ or $\neg r(b, c)$.

IsStrongAntichain.subset theorem

(hs : IsStrongAntichain r s) (h : t ⊆ s) : IsStrongAntichain r t

Full source

protected theorem subset (hs : IsStrongAntichain r s) (h : t ⊆ s) : IsStrongAntichain r t :=
  hs.mono h

Subset of a Strong Antichain is a Strong Antichain

Informal description

Let $s$ be a strong antichain with respect to a relation $r$ on a type $\alpha$. If $t$ is a subset of $s$, then $t$ is also a strong antichain with respect to $r$.

IsStrongAntichain.mono theorem

(hs : IsStrongAntichain r₁ s) (h : r₂ ≤ r₁) : IsStrongAntichain r₂ s

Full source

theorem mono (hs : IsStrongAntichain r₁ s) (h : r₂ ≤ r₁) : IsStrongAntichain r₂ s :=
  hs.mono' fun _ _ hab c => (hab c).imp (compl_le_compl h _ _) (compl_le_compl h _ _)

Monotonicity of Strong Antichains: Weaker Relation Preserves Strong Antichain Property

Informal description

Let $r_1$ and $r_2$ be binary relations on a type $\alpha$ such that $r_2 \leq r_1$ (i.e., $r_2(x,y) \to r_1(x,y)$ for all $x,y \in \alpha$). If $s$ is a strong antichain with respect to $r_1$, then $s$ is also a strong antichain with respect to $r_2$.

IsStrongAntichain.eq theorem

(hs : IsStrongAntichain r s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hac : r a c) (hbc : r b c) : a = b

Full source

theorem eq (hs : IsStrongAntichain r s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hac : r a c)
    (hbc : r b c) : a = b :=
  (Set.Pairwise.eq hs ha hb) fun h =>
    False.elim <| (h c).elim (not_not_intro hac) (not_not_intro hbc)

Equality in Strong Antichain under Common Relation

Informal description

Let $s$ be a strong antichain with respect to a relation $r$ on a type $\alpha$. For any elements $a, b \in s$ and any $c \in \alpha$, if both $r(a, c)$ and $r(b, c)$ hold, then $a = b$.

IsStrongAntichain.isAntichain theorem

[IsRefl α r] (h : IsStrongAntichain r s) : IsAntichain r s

Full source

protected theorem isAntichain [IsRefl α r] (h : IsStrongAntichain r s) : IsAntichain r s :=
  h.imp fun _ b hab => (hab b).resolve_right (not_not_intro <| refl _)

Strong Antichain Implies Antichain for Reflexive Relations

Informal description

Let $r$ be a reflexive relation on a type $\alpha$. If $s$ is a strong antichain with respect to $r$, then $s$ is also an antichain with respect to $r$. That is, for any two distinct elements $a, b \in s$, neither $r(a, b)$ nor $r(b, a)$ holds.

IsStrongAntichain.subsingleton theorem

[IsDirected α r] (h : IsStrongAntichain r s) : s.Subsingleton

Full source

protected theorem subsingleton [IsDirected α r] (h : IsStrongAntichain r s) : s.Subsingleton :=
  fun a ha b hb =>
  let ⟨_, hac, hbc⟩ := directed_of r a b
  h.eq ha hb hac hbc

Strong Antichains in Directed Relations are Subsingletons

Informal description

Let $\alpha$ be a type with a directed relation $r$. If $s \subseteq \alpha$ is a strong antichain with respect to $r$, then $s$ is a subsingleton (i.e., $s$ contains at most one element).

IsStrongAntichain.flip theorem

[IsSymm α r] (hs : IsStrongAntichain r s) : IsStrongAntichain (flip r) s

Full source

protected theorem flip [IsSymm α r] (hs : IsStrongAntichain r s) : IsStrongAntichain (flip r) s :=
  fun _ ha _ hb h c => (hs ha hb h c).imp (mt <| symm_of r) (mt <| symm_of r)

Strong Antichain Property under Relation Flip

Informal description

Let $r$ be a symmetric relation on a type $\alpha$. If $s$ is a strong antichain with respect to $r$, then $s$ is also a strong antichain with respect to the flipped relation $\text{flip}(r)$, where $\text{flip}(r)(a, b) := r(b, a)$.

IsStrongAntichain.swap theorem

[IsSymm α r] (hs : IsStrongAntichain r s) : IsStrongAntichain (swap r) s

Full source

theorem swap [IsSymm α r] (hs : IsStrongAntichain r s) : IsStrongAntichain (swap r) s :=
  hs.flip

Strong Antichain Property under Relation Swap

Informal description

Let $r$ be a symmetric relation on a type $\alpha$. If $s \subseteq \alpha$ is a strong antichain with respect to $r$, then $s$ is also a strong antichain with respect to the swapped relation $\operatorname{swap}(r)$, where $\operatorname{swap}(r)(a, b) = r(b, a)$ for all $a, b \in \alpha$.

IsStrongAntichain.image theorem

 (hs : IsStrongAntichain r s) {f : α → β} (hf : Surjective f) (h : ∀ a b, r' (f a) (f b) → r a b) :
  IsStrongAntichain r' (f '' s)

Full source

theorem image (hs : IsStrongAntichain r s) {f : α → β} (hf : Surjective f)
    (h : ∀ a b, r' (f a) (f b) → r a b) : IsStrongAntichain r' (f '' s) := by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
  obtain ⟨c, rfl⟩ := hf c
  exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)

Image of a Strong Antichain under a Surjective Function is a Strong Antichain

Informal description

Let $s \subseteq \alpha$ be a strong antichain with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$. If $f : \alpha \to \beta$ is a surjective function and $r' : \beta \to \beta \to \text{Prop}$ is a relation such that $r'(f(a), f(b))$ implies $r(a, b)$ for all $a, b \in \alpha$, then the image $f(s) \subseteq \beta$ is a strong antichain with respect to $r'$.

IsStrongAntichain.preimage theorem

 (hs : IsStrongAntichain r s) {f : β → α} (hf : Injective f) (h : ∀ a b, r' a b → r (f a) (f b)) :
  IsStrongAntichain r' (f ⁻¹' s)

Full source

theorem preimage (hs : IsStrongAntichain r s) {f : β → α} (hf : Injective f)
    (h : ∀ a b, r' a b → r (f a) (f b)) : IsStrongAntichain r' (f ⁻¹' s) := fun _ ha _ hb hab _ =>
  (hs ha hb (hf.ne hab) _).imp (mt <| h _ _) (mt <| h _ _)

Preimage of a Strong Antichain under an Injective Function is a Strong Antichain

Informal description

Let $s \subseteq \alpha$ be a strong antichain with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$. Given an injective function $f : \beta \to \alpha$ and a relation $r' : \beta \to \beta \to \text{Prop}$ such that $r'(a, b)$ implies $r(f(a), f(b))$ for all $a, b \in \beta$, then the preimage $f^{-1}(s) \subseteq \beta$ is a strong antichain with respect to $r'$.

isStrongAntichain_insert theorem

 : IsStrongAntichain r (insert a s) ↔ IsStrongAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c ∨ ¬r b c

Full source

theorem _root_.isStrongAntichain_insert :
    IsStrongAntichainIsStrongAntichain r (insert a s) ↔
      IsStrongAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c ∨ ¬r b c :=
  Set.pairwise_insert_of_symmetric fun _ _ h c => (h c).symm

Characterization of Strong Antichain Insertion: $\text{IsStrongAntichain}\, r\, (\{a\} \cup s) \leftrightarrow \text{IsStrongAntichain}\, r\, s \land \forall b \in s, a \neq b \to \forall c, \neg r(a, c) \lor \neg r(b, c)$

Informal description

For any relation $r$ on a type $\alpha$, a set $\{a\} \cup s$ is a strong antichain with respect to $r$ if and only if $s$ is a strong antichain with respect to $r$ and for every $b \in s$ with $a \neq b$, there is no common element $c$ such that both $r(a, c)$ and $r(b, c)$ hold.

IsStrongAntichain.insert theorem

 (hs : IsStrongAntichain r s) (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c ∨ ¬r b c) : IsStrongAntichain r (insert a s)

Full source

protected theorem insert (hs : IsStrongAntichain r s)
    (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c¬r a c ∨ ¬r b c) : IsStrongAntichain r (insert a s) :=
  isStrongAntichain_insert.2 ⟨hs, h⟩

Insertion Preserves Strong Antichain Property

Informal description

Let $s$ be a strong antichain with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$. If for every $b \in s$ with $a \neq b$ and for every $c \in \alpha$, either $\neg r(a, c)$ or $\neg r(b, c)$ holds, then the set $\{a\} \cup s$ is also a strong antichain with respect to $r$.

Set.Subsingleton.isStrongAntichain theorem

(hs : s.Subsingleton) (r : α → α → Prop) : IsStrongAntichain r s

Full source

theorem Set.Subsingleton.isStrongAntichain (hs : s.Subsingleton) (r : α → α → Prop) :
    IsStrongAntichain r s :=
  hs.pairwise _

Subsingleton Sets are Strong Antichains

Informal description

For any subsingleton set $s$ (i.e., a set containing at most one element) and any binary relation $r$ on elements of $s$, the set $s$ forms a strong antichain with respect to $r$.

IsAntichain.of_strictMonoOn_antitoneOn theorem

(hf : StrictMonoOn f s) (hf' : AntitoneOn f s) : IsAntichain (· ≤ ·) s

Full source

lemma IsAntichain.of_strictMonoOn_antitoneOn (hf : StrictMonoOn f s) (hf' : AntitoneOn f s) :
    IsAntichain (· ≤ ·) s :=
  fun _a ha _b hb hab' hab ↦ (hf ha hb <| hab.lt_of_ne hab').not_le (hf' ha hb hab)

Strictly Monotone and Antitone Functions Preserve Antichains

Informal description

Let $s$ be a set in a partially ordered set and $f$ a function defined on $s$. If $f$ is strictly monotone on $s$ and antitone on $s$, then $s$ is an antichain with respect to the order relation $\leq$.

IsAntichain.of_monotoneOn_strictAntiOn theorem

(hf : MonotoneOn f s) (hf' : StrictAntiOn f s) : IsAntichain (· ≤ ·) s

Full source

lemma IsAntichain.of_monotoneOn_strictAntiOn (hf : MonotoneOn f s) (hf' : StrictAntiOn f s) :
    IsAntichain (· ≤ ·) s :=
  fun _a ha _b hb hab' hab ↦ (hf ha hb hab).not_lt (hf' ha hb <| hab.lt_of_ne hab')

Monotone and Strictly Antitone Functions Preserve Antichains

Informal description

Let $s$ be a set in a partially ordered set and $f$ a function defined on $s$. If $f$ is monotone on $s$ and strictly antitone on $s$, then $s$ is an antichain with respect to the order relation $\leq$.

IsWeakAntichain definition

(s : Set (∀ i, α i)) : Prop

Full source

/-- A weak antichain in `Π i, α i` is a set such that no two distinct elements are strongly less
than each other. -/
def IsWeakAntichain (s : Set (∀ i, α i)) : Prop :=
  IsAntichain (· ≺ ·) s

Weak antichain of functions

Informal description

A set $s$ of functions in $\prod_{i} \alpha_i$ is called a *weak antichain* if no two distinct elements in $s$ are strongly less than each other. That is, for any $a, b \in s$ with $a \neq b$, the relation $a \prec b$ does not hold, where $a \prec b$ means $a(i) < b(i)$ for all $i$.

IsWeakAntichain.subset theorem

(hs : IsWeakAntichain s) : t ⊆ s → IsWeakAntichain t

Full source

protected theorem subset (hs : IsWeakAntichain s) : t ⊆ s → IsWeakAntichain t :=
  IsAntichain.subset hs

Subset of a Weak Antichain is a Weak Antichain

Informal description

If $s$ is a weak antichain of functions in $\prod_{i} \alpha_i$ and $t$ is a subset of $s$, then $t$ is also a weak antichain.

IsWeakAntichain.eq theorem

(hs : IsWeakAntichain s) : a ∈ s → b ∈ s → a ≺ b → a = b

Full source

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

Equality of Functions in a Weak Antichain under Strong Ordering

Informal description

Let $s$ be a weak antichain of functions in $\prod_{i} \alpha_i$. For any two functions $a, b \in s$ such that $a \prec b$ (i.e., $a(i) < b(i)$ for all $i$), it follows that $a = b$.

IsWeakAntichain.insert theorem

 (hs : IsWeakAntichain s) :
  (∀ ⦃b⦄, b ∈ s → a ≠ b → ¬b ≺ a) → (∀ ⦃b⦄, b ∈ s → a ≠ b → ¬a ≺ b) → IsWeakAntichain (insert a s)

Full source

protected theorem insert (hs : IsWeakAntichain s) :
    (∀ ⦃b⦄, b ∈ s → a ≠ b → ¬b ≺ a) →
      (∀ ⦃b⦄, b ∈ s → a ≠ b → ¬a ≺ b) → IsWeakAntichain (insert a s) :=
  IsAntichain.insert hs

Insertion Preserves Weak Antichain Property

Informal description

Let $s$ be a weak antichain of functions in $\prod_{i} \alpha_i$, and let $a$ be a function in $\prod_{i} \alpha_i$. If for every $b \in s$ with $a \neq b$, neither $a \prec b$ nor $b \prec a$ holds (where $a \prec b$ means $a(i) < b(i)$ for all $i$), then the set $\{a\} \cup s$ is also a weak antichain.

isWeakAntichain_insert theorem

: IsWeakAntichain (insert a s) ↔ IsWeakAntichain s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬a ≺ b ∧ ¬b ≺ a

Full source

theorem _root_.isWeakAntichain_insert :
    IsWeakAntichainIsWeakAntichain (insert a s) ↔ IsWeakAntichain s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬a ≺ b ∧ ¬b ≺ a :=
  isAntichain_insert

Characterization of Weak Antichain Insertion: $\text{IsWeakAntichain}\, (\{a\} \cup s) \leftrightarrow \text{IsWeakAntichain}\, s \land \forall b \in s, a \neq b \to \neg (a \prec b) \land \neg (b \prec a)$

Informal description

For a family of types $\{\alpha_i\}_{i \in I}$ each equipped with a less-than relation $<$, a set $s$ of functions in $\prod_{i} \alpha_i$, and a function $a \in \prod_{i} \alpha_i$, the set $\{a\} \cup s$ is a weak antichain if and only if: 1. $s$ is a weak antichain, and 2. For every $b \in s$ with $a \neq b$, neither $a \prec b$ nor $b \prec a$ holds, where $a \prec b$ means $a(i) < b(i)$ for all $i \in I$.

IsAntichain.isWeakAntichain theorem

(hs : IsAntichain (· ≤ ·) s) : IsWeakAntichain s

Full source

protected theorem IsAntichain.isWeakAntichain (hs : IsAntichain (· ≤ ·) s) : IsWeakAntichain s :=
  hs.mono fun _ _ => le_of_strongLT

Antichain in Pointwise Order Implies Weak Antichain in Strong Order

Informal description

For any set $s$ of functions in $\prod_{i} \alpha_i$ (where each $\alpha_i$ is equipped with a preorder $\leq_i$), if $s$ is an antichain with respect to the pointwise order $\leq$ (i.e., for any distinct $a, b \in s$, neither $a \leq b$ nor $b \leq a$ holds), then $s$ is also a weak antichain (i.e., for any distinct $a, b \in s$, neither $a \prec b$ nor $b \prec a$ holds, where $a \prec b$ means $a(i) < b(i)$ for all $i$).

Set.Subsingleton.isWeakAntichain theorem

(hs : s.Subsingleton) : IsWeakAntichain s

Full source

theorem Set.Subsingleton.isWeakAntichain (hs : s.Subsingleton) : IsWeakAntichain s :=
  hs.isAntichain _

Subsingleton Sets are Weak Antichains

Informal description

For any set $s$ of functions in $\prod_{i} \alpha_i$ that is a subsingleton (i.e., contains at most one element), $s$ is a weak antichain.

Definitions