mathlib documentation

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 : simple_graph α, this corresponds to independent sets of G.

Definitions #

is_antichain r s: Any two elements of s : set α are unrelated by r : α → α → Prop.
is_strong_antichain r s: Any two elements of s : set α are not related by r : α → α → Prop to a common element.
is_antichain.mk r s: Turns s into an antichain by keeping only the "maximal" elements.

@[protected]

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

def is_antichain {α : Type u_1} (r : α → α → Prop) (s : set α) :

Prop

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

Equations

is_antichain r s = s.pairwise rᶜ

@[protected]

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

is_antichain r t

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

is_antichain r₂ s

theorem is_antichain.mono_on {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : set α} (hs : is_antichain r₁ s) (h : s.pairwise (λ ⦃a b : α⦄, r₂ a b → r₁ a b)) :

is_antichain r₂ s

@[protected]

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

a = b

@[protected]

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

a = b

@[protected]

theorem is_antichain.is_antisymm {α : Type u_1} {r : α → α → Prop} (h : is_antichain r set.univ) :

is_antisymm α r

@[protected]

theorem is_antichain.subsingleton {α : Type u_1} {r : α → α → Prop} {s : set α} [is_trichotomous α r] (h : is_antichain r s) :

@[protected]

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

is_antichain (flip r) s

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

is_antichain (function.swap r) s

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

is_antichain r' (f '' s)

theorem is_antichain.preimage {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} (hs : is_antichain r s) {f : β → α} (hf : function.injective f) (h : ∀ ⦃a b : β⦄, r' a b → r (f a) (f b)) :

is_antichain r' (f ⁻¹' s)

theorem is_antichain_insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} :

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

@[protected]

theorem is_antichain.insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hs : is_antichain r s) (hl : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r b a) (hr : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b) :

is_antichain r (insert a s)

theorem is_antichain_insert_of_symmetric {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hr : symmetric r) :

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

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

is_antichain r (insert a s)

theorem is_antichain_singleton {α : Type u_1} (a : α) (r : α → α → Prop) :

is_antichain r {a}

theorem set.subsingleton.is_antichain {α : Type u_1} {s : set α} (hs : s.subsingleton) (r : α → α → Prop) :

is_antichain r s

theorem is_antichain_and_least_iff {α : Type u_1} {s : set α} {a : α} [preorder α] :

is_antichain has_le.le s ∧ is_least s a ↔ s = {a}

theorem is_antichain_and_greatest_iff {α : Type u_1} {s : set α} {a : α} [preorder α] :

is_antichain has_le.le s ∧ is_greatest s a ↔ s = {a}

theorem is_antichain.least_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : is_antichain has_le.le s) :

is_least s a ↔ s = {a}

theorem is_antichain.greatest_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : is_antichain has_le.le s) :

is_greatest s a ↔ s = {a}

theorem is_least.antichain_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : is_least s a) :

is_antichain has_le.le s ↔ s = {a}

theorem is_greatest.antichain_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : is_greatest s a) :

is_antichain has_le.le s ↔ s = {a}

theorem is_antichain.bot_mem_iff {α : Type u_1} {s : set α} [preorder α] [order_bot α] (hs : is_antichain has_le.le s) :

⊥ ∈ s ↔ s = {⊥}

theorem is_antichain.top_mem_iff {α : Type u_1} {s : set α} [preorder α] [order_top α] (hs : is_antichain has_le.le s) :

⊤ ∈ s ↔ s = {⊤}

Strong antichains #

def is_strong_antichain {α : Type u_1} (r : α → α → Prop) (s : set α) :

Prop

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

Equations

is_strong_antichain r s = s.pairwise (λ (a b : α), ∀ (c : α), ¬r a c ∨ ¬r b c)

@[protected]

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

is_strong_antichain r t

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

is_strong_antichain r₂ s

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

a = b

@[protected]

theorem is_strong_antichain.is_antichain {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α r] (h : is_strong_antichain r s) :

is_antichain r s

@[protected]

theorem is_strong_antichain.subsingleton {α : Type u_1} {r : α → α → Prop} {s : set α} [is_directed α r] (h : is_strong_antichain r s) :

@[protected]

theorem is_strong_antichain.flip {α : Type u_1} {r : α → α → Prop} {s : set α} [is_symm α r] (hs : is_strong_antichain r s) :

is_strong_antichain (flip r) s

theorem is_strong_antichain.swap {α : Type u_1} {r : α → α → Prop} {s : set α} [is_symm α r] (hs : is_strong_antichain r s) :

is_strong_antichain (function.swap r) s

theorem is_strong_antichain.image {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} (hs : is_strong_antichain r s) {f : α → β} (hf : function.surjective f) (h : ∀ (a b : α), r' (f a) (f b) → r a b) :

is_strong_antichain r' (f '' s)

theorem is_strong_antichain.preimage {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} (hs : is_strong_antichain r s) {f : β → α} (hf : function.injective f) (h : ∀ (a b : β), r' a b → r (f a) (f b)) :

is_strong_antichain r' (f ⁻¹' s)

theorem is_strong_antichain_insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} :

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

@[protected]

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

is_strong_antichain r (insert a s)

theorem set.subsingleton.is_strong_antichain {α : Type u_1} {s : set α} (hs : s.subsingleton) (r : α → α → Prop) :

is_strong_antichain r s