mathlib3 documentation

order.antichain

Antichains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (has_insert.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 (has_insert.insert a s)

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

is_antichain r (has_insert.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 (has_insert.insert a s)

theorem is_antichain.image_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} (hs : is_antichain r s) (φ : r ↪r r') :

is_antichain r' (⇑φ '' s)

theorem is_antichain.preimage_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : set β} (ht : is_antichain r' t) (φ : r ↪r r') :

is_antichain r (⇑φ ⁻¹' t)

theorem is_antichain.image_rel_iso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} (hs : is_antichain r s) (φ : r ≃r r') :

is_antichain r' (⇑φ '' s)

theorem is_antichain.preimage_rel_iso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : set β} (hs : is_antichain r' t) (φ : r ≃r r') :

is_antichain r (⇑φ ⁻¹' t)

theorem is_antichain.image_rel_embedding_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} {φ : r ↪r r'} :

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

theorem is_antichain.image_rel_iso_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} {φ : r ≃r r'} :

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

theorem is_antichain.image_embedding {α : Type u_1} {β : Type u_2} {s : set α} [has_le α] [has_le β] (hs : is_antichain has_le.le s) (φ : α ↪o β) :

is_antichain has_le.le (⇑φ '' s)

theorem is_antichain.preimage_embedding {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {t : set β} (ht : is_antichain has_le.le t) (φ : α ↪o β) :

is_antichain has_le.le (⇑φ ⁻¹' t)

theorem is_antichain.image_embedding_iff {α : Type u_1} {β : Type u_2} {s : set α} [has_le α] [has_le β] {φ : α ↪o β} :

is_antichain has_le.le (⇑φ '' s) ↔ is_antichain has_le.le s

theorem is_antichain.image_iso {α : Type u_1} {β : Type u_2} {s : set α} [has_le α] [has_le β] (hs : is_antichain has_le.le s) (φ : α ≃o β) :

is_antichain has_le.le (⇑φ '' s)

theorem is_antichain.image_iso_iff {α : Type u_1} {β : Type u_2} {s : set α} [has_le α] [has_le β] {φ : α ≃o β} :

is_antichain has_le.le (⇑φ '' s) ↔ is_antichain has_le.le s

theorem is_antichain.preimage_iso {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {t : set β} (ht : is_antichain has_le.le t) (φ : α ≃o β) :

is_antichain has_le.le (⇑φ ⁻¹' t)

theorem is_antichain.preimage_iso_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {t : set β} {φ : α ≃o β} :

is_antichain has_le.le (⇑φ ⁻¹' t) ↔ is_antichain has_le.le t

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

is_antichain has_le.le s

theorem is_antichain.to_dual_iff {α : Type u_1} {s : set α} [has_le α] :

is_antichain has_le.le s ↔ is_antichain has_le.le s

theorem is_antichain.image_compl {α : Type u_1} {s : set α} [boolean_algebra α] (hs : is_antichain has_le.le s) :

is_antichain has_le.le (has_compl.compl '' s)

theorem is_antichain.preimage_compl {α : Type u_1} {s : set α} [boolean_algebra α] (hs : is_antichain has_le.le s) :

is_antichain has_le.le (has_compl.compl ⁻¹' 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.not_lt {α : Type u_1} {s : set α} {a b : α} [preorder α] (hs : is_antichain has_le.le s) (ha : a ∈ s) (hb : b ∈ s) :

¬a < b

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 = {⊤}

theorem is_antichain_iff_forall_not_lt {α : Type u_1} {s : set α} [partial_order α] :

is_antichain has_le.le s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ¬a < b

Strong antichains #

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

Prop

A 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 (has_insert.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 (has_insert.insert a s)

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

is_strong_antichain r s

Weak antichains #

def is_weak_antichain {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] (s : set (Π (i : ι), α i)) :

Prop

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

Equations

is_weak_antichain s = is_antichain strong_lt s

@[protected]

theorem is_weak_antichain.subset {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s t : set (Π (i : ι), α i)} (hs : is_weak_antichain s) :

t ⊆ s → is_weak_antichain t

@[protected]

theorem is_weak_antichain.eq {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} {a b : Π (i : ι), α i} (hs : is_weak_antichain s) :

a ∈ s → b ∈ s → strong_lt a b → a = b

@[protected]

theorem is_weak_antichain.insert {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} {a : Π (i : ι), α i} (hs : is_weak_antichain s) :

(∀ ⦃b : Π (i : ι), α i⦄, b ∈ s → a ≠ b → ¬strong_lt b a) → (∀ ⦃b : Π (i : ι), α i⦄, b ∈ s → a ≠ b → ¬strong_lt a b) → is_weak_antichain (has_insert.insert a s)

theorem is_weak_antichain_insert {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} {a : Π (i : ι), α i} :

is_weak_antichain (has_insert.insert a s) ↔ is_weak_antichain s ∧ ∀ ⦃b : Π (i : ι), α i⦄, b ∈ s → a ≠ b → ¬strong_lt a b ∧ ¬strong_lt b a

@[protected]

theorem is_antichain.is_weak_antichain {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} (hs : is_antichain has_le.le s) :

is_weak_antichain s

theorem set.subsingleton.is_weak_antichain {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} (hs : s.subsingleton) :

is_weak_antichain s