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.
• IsAntichain.mk r s: Turns s into an antichain by keeping only the "maximal" elements.
theorem Symmetric.compl {α : Type u_1} {r : ααProp} (h : ) :
def IsAntichain {α : Type u_1} (r : ααProp) (s : Set α) :

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

Equations
Instances For
theorem IsAntichain.subset {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (hs : ) (h : t s) :
theorem IsAntichain.mono {α : Type u_1} {r₁ : ααProp} {r₂ : ααProp} {s : Set α} (hs : IsAntichain r₁ s) (h : r₂ r₁) :
theorem IsAntichain.mono_on {α : Type u_1} {r₁ : ααProp} {r₂ : ααProp} {s : Set α} (hs : IsAntichain r₁ s) (h : Set.Pairwise s fun ⦃a b : α⦄ => r₂ a br₁ a b) :
theorem IsAntichain.eq {α : Type u_1} {r : ααProp} {s : Set α} (hs : ) {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 : ) {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) :
theorem IsAntichain.subsingleton {α : Type u_1} {r : ααProp} {s : Set α} [] (h : ) :
theorem IsAntichain.flip {α : Type u_1} {r : ααProp} {s : Set α} (hs : ) :
theorem IsAntichain.swap {α : Type u_1} {r : ααProp} {s : Set α} (hs : ) :
theorem IsAntichain.image {α : Type u_1} {β : Type u_2} {r : ααProp} {r' : ββProp} {s : Set α} (hs : ) (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 : ) {f : βα} (hf : ) (h : ∀ ⦃a b : β⦄, r' a br (f a) (f b)) :
theorem isAntichain_insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} :
IsAntichain r (insert a s) ∀ ⦃b : α⦄, b sa b¬r a b ¬r b a
theorem IsAntichain.insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : ) (hl : ∀ ⦃b : α⦄, b sa b¬r b a) (hr : ∀ ⦃b : α⦄, b sa b¬r a b) :
theorem isAntichain_insert_of_symmetric {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hr : ) :
IsAntichain r (insert a s) ∀ ⦃b : α⦄, b sa b¬r a b
theorem IsAntichain.insert_of_symmetric {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : ) (hr : ) (h : ∀ ⦃b : α⦄, b sa b¬r a b) :
theorem IsAntichain.image_relEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {r' : ββProp} {s : Set α} (hs : ) (φ : 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 : ) (φ : 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)
theorem IsAntichain.image_relIso_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {r' : ββProp} {s : Set α} {φ : r ≃r r'} :
IsAntichain r' (φ '' s)
theorem IsAntichain.image_embedding {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) (φ : α ↪o β) :
IsAntichain (fun (x x_1 : β) => x x_1) (φ '' s)
theorem IsAntichain.preimage_embedding {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} (ht : IsAntichain (fun (x x_1 : β) => x x_1) t) (φ : α ↪o β) :
IsAntichain (fun (x x_1 : α) => x x_1) (φ ⁻¹' t)
theorem IsAntichain.image_embedding_iff {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] {φ : α ↪o β} :
IsAntichain (fun (x x_1 : β) => x x_1) (φ '' s) IsAntichain (fun (x x_1 : α) => x x_1) s
theorem IsAntichain.image_iso {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) (φ : α ≃o β) :
IsAntichain (fun (x x_1 : β) => x x_1) (φ '' s)
theorem IsAntichain.image_iso_iff {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] {φ : α ≃o β} :
IsAntichain (fun (x x_1 : β) => x x_1) (φ '' s) IsAntichain (fun (x x_1 : α) => x x_1) s
theorem IsAntichain.preimage_iso {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} (ht : IsAntichain (fun (x x_1 : β) => x x_1) t) (φ : α ≃o β) :
IsAntichain (fun (x x_1 : α) => x x_1) (φ ⁻¹' t)
theorem IsAntichain.preimage_iso_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} {φ : α ≃o β} :
IsAntichain (fun (x x_1 : α) => x x_1) (φ ⁻¹' t) IsAntichain (fun (x x_1 : β) => x x_1) t
theorem IsAntichain.to_dual {α : Type u_1} {s : Set α} [LE α] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
IsAntichain (fun (x x_1 : αᵒᵈ) => x x_1) s
theorem IsAntichain.to_dual_iff {α : Type u_1} {s : Set α} [LE α] :
IsAntichain (fun (x x_1 : α) => x x_1) s IsAntichain (fun (x x_1 : αᵒᵈ) => x x_1) s
theorem IsAntichain.image_compl {α : Type u_1} {s : Set α} [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
IsAntichain (fun (x x_1 : α) => x x_1) (compl '' s)
theorem IsAntichain.preimage_compl {α : Type u_1} {s : Set α} [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
IsAntichain (fun (x x_1 : α) => x x_1) (compl ⁻¹' s)
theorem isAntichain_singleton {α : Type u_1} (a : α) (r : ααProp) :
theorem Set.Subsingleton.isAntichain {α : Type u_1} {s : Set α} (hs : ) (r : ααProp) :
theorem IsAntichain.not_lt {α : Type u_1} {s : Set α} {a : α} {b : α} [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) (ha : a s) (hb : b s) :
¬a < b
theorem isAntichain_and_least_iff {α : Type u_1} {s : Set α} {a : α} [] :
IsAntichain (fun (x x_1 : α) => x x_1) s IsLeast s a s = {a}
theorem isAntichain_and_greatest_iff {α : Type u_1} {s : Set α} {a : α} [] :
IsAntichain (fun (x x_1 : α) => x x_1) s s = {a}
theorem IsAntichain.least_iff {α : Type u_1} {s : Set α} {a : α} [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
IsLeast s a s = {a}
theorem IsAntichain.greatest_iff {α : Type u_1} {s : Set α} {a : α} [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
s = {a}
theorem IsLeast.antichain_iff {α : Type u_1} {s : Set α} {a : α} [] (hs : IsLeast s a) :
IsAntichain (fun (x x_1 : α) => x x_1) s s = {a}
theorem IsGreatest.antichain_iff {α : Type u_1} {s : Set α} {a : α} [] (hs : ) :
IsAntichain (fun (x x_1 : α) => x x_1) s s = {a}
theorem IsAntichain.bot_mem_iff {α : Type u_1} {s : Set α} [] [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
s s = {}
theorem IsAntichain.top_mem_iff {α : Type u_1} {s : Set α} [] [] (hs : IsAntichain (fun (x x_1 : α) => x x_1) s) :
s s = {}
theorem isAntichain_iff_forall_not_lt {α : Type u_1} {s : Set α} [] :
IsAntichain (fun (x x_1 : α) => x x_1) s ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b s¬a < b

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
Instances For
theorem IsStrongAntichain.subset {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (hs : ) (h : t s) :
theorem IsStrongAntichain.mono {α : Type u_1} {r₁ : ααProp} {r₂ : ααProp} {s : Set α} (hs : ) (h : r₂ r₁) :
theorem IsStrongAntichain.eq {α : Type u_1} {r : ααProp} {s : Set α} (hs : ) {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 : ) :
theorem IsStrongAntichain.subsingleton {α : Type u_1} {r : ααProp} {s : Set α} [] (h : ) :
theorem IsStrongAntichain.flip {α : Type u_1} {r : ααProp} {s : Set α} [IsSymm α r] (hs : ) :
theorem IsStrongAntichain.swap {α : Type u_1} {r : ααProp} {s : Set α} [IsSymm α r] (hs : ) :
theorem IsStrongAntichain.image {α : Type u_1} {β : Type u_2} {r : ααProp} {r' : ββProp} {s : Set α} (hs : ) {f : αβ} (hf : ) (h : ∀ (a b : α), r' (f a) (f b)r a b) :
theorem IsStrongAntichain.preimage {α : Type u_1} {β : Type u_2} {r : ααProp} {r' : ββProp} {s : Set α} (hs : ) {f : βα} (hf : ) (h : ∀ (a b : β), r' a br (f a) (f b)) :
theorem isStrongAntichain_insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} :
IsStrongAntichain r (insert a s) ∀ ⦃b : α⦄, b sa b∀ (c : α), ¬r a c ¬r b c
theorem IsStrongAntichain.insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : ) (h : ∀ ⦃b : α⦄, b sa b∀ (c : α), ¬r a c ¬r b c) :
theorem Set.Subsingleton.isStrongAntichain {α : Type u_1} {s : Set α} (hs : ) (r : ααProp) :
theorem IsAntichain.of_strictMonoOn_antitoneOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) (hf' : ) :
IsAntichain (fun (x x_1 : α) => x x_1) s
theorem IsAntichain.of_monotoneOn_strictAntiOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) (hf' : ) :
IsAntichain (fun (x x_1 : α) => x x_1) 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
Instances For
theorem IsWeakAntichain.subset {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {t : Set ((i : ι) → α i)} (hs : ) :
t s
theorem IsWeakAntichain.eq {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a : (i : ι) → α i} {b : (i : ι) → α i} (hs : ) :
a sb sStrongLT a ba = b
theorem IsWeakAntichain.insert {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a : (i : ι) → α i} (hs : ) :
(∀ ⦃b : (i : ι) → α i⦄, b sa b¬StrongLT b a)(∀ ⦃b : (i : ι) → α i⦄, b sa 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) ∀ ⦃b : (i : ι) → α i⦄, b sa 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 (x x_1 : (i : ι) → α i) => x x_1) s) :
theorem Set.Subsingleton.isWeakAntichain {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} (hs : ) :