Documentation

Mathlib.Order.Antichain

Antichains #

This file defines antichains. An antichain is a set where any two distinct elements are not related. If the relation is (≤), this corresponds to incomparability and usual order antichains. If the relation is G.Adj for G : SimpleGraph α, this corresponds to independent sets of G.

Definitions #

IsAntichain r s: Any two elements of s : Set α are unrelated by r : α → α → Prop.
IsStrongAntichain r s: Any two elements of s : Set α are not related by r : α → α → Prop to a common element.

theorem Symmetric.compl {α : Type u_1} {r : α → α → Prop} (h : Symmetric r) :

def IsAntichain {α : Type u_1} (r : α → α → Prop) (s : Set α) :

An antichain is a set such that no two distinct elements are related.

Equations

IsAntichain r s = s.Pairwise rᶜ

Instances For

@[simp]

theorem IsAntichain.empty {α : Type u_1} {r : α → α → Prop} :

IsAntichain r ∅

@[simp]

theorem IsAntichain.singleton {α : Type u_1} {r : α → α → Prop} {a : α} :

IsAntichain r {a}

theorem IsAntichain.subset {α : Type u_1} {r : α → α → Prop} {s t : Set α} (hs : IsAntichain r s) (h : t ⊆ s) :

IsAntichain r t

theorem IsAntichain.mono {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : Set α} (hs : IsAntichain r₁ s) (h : r₂ ≤ r₁) :

IsAntichain r₂ s

theorem IsAntichain.mono_on {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : Set α} (hs : IsAntichain r₁ s) (h : s.Pairwise fun ⦃a b : α⦄ => r₂ a b → r₁ a b) :

IsAntichain r₂ s

theorem IsAntichain.eq {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r a b) :

a = b

theorem IsAntichain.eq' {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r b a) :

a = b

theorem IsAntichain.isAntisymm {α : Type u_1} {r : α → α → Prop} (h : IsAntichain r Set.univ) :

IsAntisymm α r

theorem IsAntichain.subsingleton {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsTrichotomous α r] (h : IsAntichain r s) :

theorem IsAntichain.flip {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsAntichain r s) :

IsAntichain (flip r) s

theorem IsAntichain.swap {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsAntichain r s) :

IsAntichain (Function.swap r) s

theorem IsAntichain.image {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsAntichain r s) (f : α → β) (h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b) :

IsAntichain r' (f '' s)

theorem IsAntichain.preimage {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsAntichain r s) {f : β → α} (hf : Function.Injective f) (h : ∀ ⦃a b : β⦄, r' a b → r (f a) (f b)) :

IsAntichain r' (f ⁻¹' s)

theorem isAntichain_insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} :

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

theorem IsAntichain.insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (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)

theorem isAntichain_insert_of_symmetric {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hr : Symmetric r) :

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

theorem IsAntichain.insert_of_symmetric {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hs : IsAntichain r s) (hr : Symmetric r) (h : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b) :

IsAntichain r (insert a s)

theorem IsAntichain.image_relEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsAntichain r s) (φ : r ↪r r') :

IsAntichain r' (⇑φ '' s)

theorem IsAntichain.preimage_relEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β} (ht : IsAntichain r' t) (φ : r ↪r r') :

IsAntichain r (⇑φ ⁻¹' t)

theorem IsAntichain.image_relIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsAntichain r s) (φ : r ≃r r') :

IsAntichain r' (⇑φ '' s)

theorem IsAntichain.preimage_relIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β} (hs : IsAntichain r' t) (φ : r ≃r r') :

IsAntichain r (⇑φ ⁻¹' t)

theorem IsAntichain.image_relEmbedding_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ↪r r'} :

IsAntichain r' (⇑φ '' s) ↔ IsAntichain r s

theorem IsAntichain.image_relIso_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ≃r r'} :

IsAntichain r' (⇑φ '' s) ↔ IsAntichain r s

theorem IsAntichain.image_embedding {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) (φ : α ↪o β) :

IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s)

theorem IsAntichain.preimage_embedding {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} (ht : IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) t) (φ : α ↪o β) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (⇑φ ⁻¹' t)

theorem IsAntichain.image_embedding_iff {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] {φ : α ↪o β} :

IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s) ↔ IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s

theorem IsAntichain.image_iso {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) (φ : α ≃o β) :

IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s)

theorem IsAntichain.image_iso_iff {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] {φ : α ≃o β} :

IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s) ↔ IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s

theorem IsAntichain.preimage_iso {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} (ht : IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) t) (φ : α ≃o β) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (⇑φ ⁻¹' t)

theorem IsAntichain.preimage_iso_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} {φ : α ≃o β} :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (⇑φ ⁻¹' t) ↔ IsAntichain (fun (x1 x2 : β) => x1 ≤ x2) t

theorem IsAntichain.to_dual {α : Type u_1} {s : Set α} [LE α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

IsAntichain (fun (x1 x2 : αᵒᵈ) => x1 ≤ x2) s

theorem IsAntichain.to_dual_iff {α : Type u_1} {s : Set α} [LE α] :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s ↔ IsAntichain (fun (x1 x2 : αᵒᵈ) => x1 ≤ x2) s

theorem IsAntichain.image_compl {α : Type u_1} {s : Set α} [BooleanAlgebra α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (compl '' s)

theorem IsAntichain.preimage_compl {α : Type u_1} {s : Set α} [BooleanAlgebra α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (compl ⁻¹' s)

theorem isAntichain_union {α : Type u_1} {r : α → α → Prop} {s t : Set α} :

IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a

@[deprecated IsAntichain.singleton (since := "2025-09-20")]

theorem isAntichain_singleton {α : Type u_1} {r : α → α → Prop} {a : α} :

IsAntichain r {a}

Alias of IsAntichain.singleton.

theorem Set.Subsingleton.isAntichain {α : Type u_1} {s : Set α} (hs : s.Subsingleton) (r : α → α → Prop) :

IsAntichain r s

theorem subsingleton_of_isChain_of_isAntichain {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsChain r s) (ht : IsAntichain r s) :

A set which is simultaneously a chain and antichain is subsingleton.

theorem isChain_and_isAntichain_iff_subsingleton {α : Type u_1} {r : α → α → Prop} {s : Set α} :

IsChain r s ∧ IsAntichain r s ↔ s.Subsingleton

theorem inter_subsingleton_of_isChain_of_isAntichain {α : Type u_1} {r : α → α → Prop} {s t : Set α} (hs : IsChain r s) (ht : IsAntichain r t) :

(s ∩ t).Subsingleton

The intersection of a chain and an antichain is subsingleton.

theorem inter_subsingleton_of_isAntichain_of_isChain {α : Type u_1} {r : α → α → Prop} {s t : Set α} (hs : IsAntichain r s) (ht : IsChain r t) :

(s ∩ t).Subsingleton

The intersection of an antichain and a chain is subsingleton.

theorem IsAntichain.not_lt {α : Type u_1} {s : Set α} {a b : α} [Preorder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) (ha : a ∈ s) (hb : b ∈ s) :

¬a < b

theorem isAntichain_and_least_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s ∧ IsLeast s a ↔ s = {a}

theorem isAntichain_and_greatest_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s ∧ IsGreatest s a ↔ s = {a}

theorem IsAntichain.least_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

IsLeast s a ↔ s = {a}

theorem IsAntichain.greatest_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

IsGreatest s a ↔ s = {a}

theorem IsLeast.antichain_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] (hs : IsLeast s a) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s ↔ s = {a}

theorem IsGreatest.antichain_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] (hs : IsGreatest s a) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s ↔ s = {a}

theorem IsAntichain.bot_mem_iff {α : Type u_1} {s : Set α} [Preorder α] [OrderBot α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

⊥ ∈ s ↔ s = {⊥}

theorem IsAntichain.top_mem_iff {α : Type u_1} {s : Set α} [Preorder α] [OrderTop α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

⊤ ∈ s ↔ s = {⊤}

theorem IsAntichain.minimal_mem_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

Minimal (fun (x : α) => x ∈ s) a ↔ a ∈ s

theorem IsAntichain.maximal_mem_iff {α : Type u_1} {s : Set α} {a : α} [Preorder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s) :

Maximal (fun (x : α) => x ∈ s) a ↔ a ∈ s

theorem IsAntichain.eq_setOf_maximal {α : Type u_1} {s t : Set α} [Preorder α] (ht : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) t) (h : ∀ (x : α), Maximal (fun (x : α) => x ∈ s) x → x ∈ t) (hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) => x ∈ s) b) :

{x : α | Maximal (fun (x : α) => x ∈ s) x} = t

If t is an antichain shadowing and including the set of maximal elements of s, then t is the set of maximal elements of s.

theorem IsAntichain.eq_setOf_minimal {α : Type u_1} {s t : Set α} [Preorder α] (ht : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) t) (h : ∀ (x : α), Minimal (fun (x : α) => x ∈ s) x → x ∈ t) (hs : ∀ a ∈ t, ∃ (b : α), a ≤ b ∧ Minimal (fun (x : α) => x ∈ s) b) :

{x : α | Minimal (fun (x : α) => x ∈ s) x} = t

If t is an antichain shadowed by and including the set of minimal elements of s, then t is the set of minimal elements of s.

theorem IsAntichain.of_strictMonoOn_antitoneOn {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) (hf' : AntitoneOn f s) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s

theorem IsAntichain.of_monotoneOn_strictAntiOn {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) (hf' : StrictAntiOn f s) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s

theorem isAntichain_iff_forall_not_lt {α : Type u_1} [PartialOrder α] {s : Set α} :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ¬a < b

theorem setOf_maximal_antichain {α : Type u_1} [PartialOrder α] (P : α → Prop) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) {x : α | Maximal P x}

theorem setOf_minimal_antichain {α : Type u_1} [PartialOrder α] (P : α → Prop) :

IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) {x : α | Minimal P x}

Strong antichains #

def IsStrongAntichain {α : Type u_1} (r : α → α → Prop) (s : Set α) :

A strong (upward) antichain is a set such that no two distinct elements are related to a common element.

Equations

IsStrongAntichain r s = s.Pairwise fun (a b : α) => ∀ (c : α), ¬r a c ∨ ¬r b c

Instances For

theorem IsStrongAntichain.subset {α : Type u_1} {r : α → α → Prop} {s t : Set α} (hs : IsStrongAntichain r s) (h : t ⊆ s) :

IsStrongAntichain r t

theorem IsStrongAntichain.mono {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : Set α} (hs : IsStrongAntichain r₁ s) (h : r₂ ≤ r₁) :

IsStrongAntichain r₂ s

theorem IsStrongAntichain.eq {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsStrongAntichain r s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hac : r a c) (hbc : r b c) :

a = b

theorem IsStrongAntichain.isAntichain {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsRefl α r] (h : IsStrongAntichain r s) :

IsAntichain r s

theorem IsStrongAntichain.subsingleton {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsDirected α r] (h : IsStrongAntichain r s) :

theorem IsStrongAntichain.flip {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsSymm α r] (hs : IsStrongAntichain r s) :

IsStrongAntichain (flip r) s

theorem IsStrongAntichain.swap {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsSymm α r] (hs : IsStrongAntichain r s) :

IsStrongAntichain (Function.swap r) s

theorem IsStrongAntichain.image {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsStrongAntichain r s) {f : α → β} (hf : Function.Surjective f) (h : ∀ (a b : α), r' (f a) (f b) → r a b) :

IsStrongAntichain r' (f '' s)

theorem IsStrongAntichain.preimage {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsStrongAntichain r s) {f : β → α} (hf : Function.Injective f) (h : ∀ (a b : β), r' a b → r (f a) (f b)) :

IsStrongAntichain r' (f ⁻¹' s)

theorem isStrongAntichain_insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} :

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

theorem IsStrongAntichain.insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hs : IsStrongAntichain r s) (h : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ∀ (c : α), ¬r a c ∨ ¬r b c) :

IsStrongAntichain r (insert a s)

theorem Set.Subsingleton.isStrongAntichain {α : Type u_1} {s : Set α} (hs : s.Subsingleton) (r : α → α → Prop) :

IsStrongAntichain r s

Weak antichains #

def IsWeakAntichain {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] (s : Set ((i : ι) → α i)) :

A weak antichain in Π i, α i is a set such that no two distinct elements are strongly less than each other.

Equations

IsWeakAntichain s = IsAntichain (fun (x1 x2 : (i : ι) → α i) => StrongLT x1 x2) s

Instances For

theorem IsWeakAntichain.subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] {s t : Set ((i : ι) → α i)} (hs : IsWeakAntichain s) :

t ⊆ s → IsWeakAntichain t

theorem IsWeakAntichain.eq {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a b : (i : ι) → α i} (hs : IsWeakAntichain s) :

a ∈ s → b ∈ s → StrongLT a b → a = b

theorem IsWeakAntichain.insert {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a : (i : ι) → α i} (hs : IsWeakAntichain s) :

(∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT b a) → (∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT a b) → IsWeakAntichain (insert a s)

theorem isWeakAntichain_insert {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a : (i : ι) → α i} :

IsWeakAntichain (insert a s) ↔ IsWeakAntichain s ∧ ∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT a b ∧ ¬StrongLT b a

theorem IsAntichain.isWeakAntichain {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} (hs : IsAntichain (fun (x1 x2 : (i : ι) → α i) => x1 ≤ x2) s) :

IsWeakAntichain s

theorem Set.Subsingleton.isWeakAntichain {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} (hs : s.Subsingleton) :

IsWeakAntichain s