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 ofs : Set αare unrelated byr : α → α → Prop.IsStrongAntichain r s: Any two elements ofs : Set αare not related byr : α → α → Propto a common element.IsMaxAntichain r s: An antichain such that no antichain strictly includingsexists.
An antichain is a set such that no two distinct elements are related.
Equations
Instances For
@[simp]
@[simp]
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)
:
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)
:
@[deprecated antisymm (since := "2026-01-06")]
theorem
IsAntichain.isAntisymm
{α : Sort u_1}
{r : α → α → Prop}
{a b : α}
[Std.Antisymm r]
:
r a b → r b a → a = b
Alias of antisymm.
theorem
IsAntichain.subsingleton
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
[Std.Trichotomous 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 : α}
(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)
:
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_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_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.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.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.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)
@[simp]
theorem
IsAntichain.diff
{α : Type u_1}
{r : α → α → Prop}
{s t : Set α}
(h : IsAntichain r s)
:
IsAntichain r (s \ t)
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")]
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
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)
:
theorem
IsAntichain.greatest_iff
{α : Type u_1}
{s : Set α}
{a : α}
[Preorder α]
(hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
IsGreatest.antichain_iff
{α : Type u_1}
{s : Set α}
{a : α}
[Preorder α]
(hs : IsGreatest s a)
:
theorem
IsAntichain.minimal_mem_iff
{α : Type u_1}
{s : Set α}
{a : α}
[Preorder α]
(hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
IsAntichain.maximal_mem_iff
{α : Type u_1}
{s : Set α}
{a : α}
[Preorder α]
(hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) 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)
:
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)
:
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
Strong antichains #
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 t : Set α}
(hs : IsStrongAntichain r s)
(h : t ⊆ s)
:
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)
:
theorem
IsStrongAntichain.isAntichain
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
[Std.Refl 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 α}
[Std.Symm r]
(hs : IsStrongAntichain r s)
:
IsStrongAntichain (flip r) s
theorem
IsStrongAntichain.swap
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
[Std.Symm r]
(hs : IsStrongAntichain 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)
:
Maximal antichains #
An antichain s is a maximal antichain if there does not exists an antichain strictly including
s.
Equations
Instances For
theorem
IsMaxAntichain.isAntichain
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(h : IsMaxAntichain r s)
:
IsAntichain r s
theorem
IsMaxAntichain.image
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(e : r ≃r s)
{c : Set α}
(hc : IsMaxAntichain r c)
:
IsMaxAntichain s (⇑e '' c)
theorem
IsMaxAntichain.isEmpty_iff
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(h : IsMaxAntichain r s)
:
theorem
IsMaxAntichain.nonempty_iff
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(h : IsMaxAntichain r s)
:
theorem
IsMaxAntichain.symm
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(h : IsMaxAntichain r s)
:
IsMaxAntichain (flip 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
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.insert
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Preorder (α i)]
{s : Set ((i : ι) → α i)}
{a : (i : ι) → α i}
(hs : IsWeakAntichain s)
:
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)
:
theorem
Set.Subsingleton.isWeakAntichain
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Preorder (α i)]
{s : Set ((i : ι) → α i)}
(hs : s.Subsingleton)
: