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 #

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
Instances For
    theorem IsAntichain.subset {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (hs : IsAntichain r s) (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 : s.Pairwise fun ⦃a b : α⦄ => r₂ a br₁ 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 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) :
    theorem IsAntichain.subsingleton {α : Type u_1} {r : ααProp} {s : Set α} [IsTrichotomous α r] (h : IsAntichain r s) :
    s.Subsingleton
    theorem IsAntichain.flip {α : Type u_1} {r : ααProp} {s : Set α} (hs : IsAntichain r s) :
    theorem IsAntichain.swap {α : Type u_1} {r : ααProp} {s : Set α} (hs : IsAntichain 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 br (f a) (f b)) :
    theorem isAntichain_insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} :
    IsAntichain r (insert a s) IsAntichain r s ∀ ⦃b : α⦄, b sa 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 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 : Symmetric r) :
    IsAntichain r (insert a s) IsAntichain r s ∀ ⦃b : α⦄, b sa 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 sa b¬r a b) :
    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_singleton {α : Type u_1} (a : α) (r : ααProp) :
    theorem Set.Subsingleton.isAntichain {α : Type u_1} {s : Set α} (hs : s.Subsingleton) (r : ααProp) :
    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_iff_forall_not_lt {α : Type u_1} {s : Set α} [PartialOrder α] :
    IsAntichain (fun (x1 x2 : α) => x1 x2) 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 : IsStrongAntichain r s) (h : t s) :
      theorem IsStrongAntichain.mono {α : Type u_1} {r₁ : ααProp} {r₂ : ααProp} {s : Set α} (hs : IsStrongAntichain r₁ s) (h : r₂ r₁) :
      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) :
      theorem IsStrongAntichain.subsingleton {α : Type u_1} {r : ααProp} {s : Set α} [IsDirected α r] (h : IsStrongAntichain r s) :
      s.Subsingleton
      theorem IsStrongAntichain.flip {α : Type u_1} {r : ααProp} {s : Set α} [IsSymm α r] (hs : IsStrongAntichain r s) :
      theorem IsStrongAntichain.swap {α : Type u_1} {r : ααProp} {s : Set α} [IsSymm α 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) :
      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 br (f a) (f b)) :
      theorem isStrongAntichain_insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} :
      IsStrongAntichain r (insert a s) IsStrongAntichain r s ∀ ⦃b : α⦄, b sa 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 sa b∀ (c : α), ¬r a c ¬r b c) :
      theorem Set.Subsingleton.isStrongAntichain {α : Type u_1} {s : Set α} (hs : s.Subsingleton) (r : ααProp) :
      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

      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 : IsWeakAntichain s) :
        theorem IsWeakAntichain.eq {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a : (i : ι) → α i} {b : (i : ι) → α i} (hs : IsWeakAntichain s) :
        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 : IsWeakAntichain s) :
        (∀ ⦃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) IsWeakAntichain 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 (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) :