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 #

@[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
@[protected]
theorem is_antichain.subset {α : Type u_1} {r : α → α → Prop} {s t : set α} (hs : is_antichain r s) (h : t s) :
theorem is_antichain.mono {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : set α} (hs : is_antichain r₁ s) (h : r₂ r₁) :
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 br₁ 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 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) :
@[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) :
theorem is_antichain.swap {α : Type u_1} {r : α → α → Prop} {s : set α} (hs : is_antichain 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 br (f a) (f b)) :
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 sa 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 sa b¬r b a) (hr : ∀ ⦃b : α⦄, b sa b¬r a b) :
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 sa 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 sa b¬r a b) :
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') :
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') :
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') :
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') :
theorem is_antichain.image_rel_embedding_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} {φ : r ↪r r'} :
theorem is_antichain.image_rel_iso_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} {φ : r ≃r r'} :
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 β) :
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 β) :
theorem is_antichain.image_embedding_iff {α : Type u_1} {β : Type u_2} {s : set α} [has_le α] [has_le β] {φ : α ↪o β} :
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 β) :
theorem is_antichain.image_iso_iff {α : Type u_1} {β : Type u_2} {s : set α} [has_le α] [has_le β] {φ : α ≃o β} :
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 β) :
theorem is_antichain.preimage_iso_iff {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {t : set β} {φ : α ≃o β} :
theorem is_antichain.to_dual {α : Type u_1} {s : set α} [has_le α] (hs : is_antichain has_le.le s) :
theorem is_antichain_singleton {α : Type u_1} (a : α) (r : α → α → Prop) :
theorem set.subsingleton.is_antichain {α : Type u_1} {s : set α} (hs : s.subsingleton) (r : α → α → Prop) :
theorem is_antichain_and_least_iff {α : Type u_1} {s : set α} {a : α} [preorder α] :
theorem is_antichain_and_greatest_iff {α : Type u_1} {s : set α} {a : α} [preorder α] :
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) :
theorem is_greatest.antichain_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : is_greatest 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
@[protected]
theorem is_strong_antichain.subset {α : Type u_1} {r : α → α → Prop} {s t : set α} (hs : is_strong_antichain r s) (h : t s) :
theorem is_strong_antichain.mono {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : set α} (hs : is_strong_antichain r₁ s) (h : r₂ r₁) :
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) :
@[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) :
theorem is_strong_antichain.swap {α : Type u_1} {r : α → α → Prop} {s : set α} [is_symm α r] (hs : is_strong_antichain 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) :
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 br (f a) (f b)) :
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 sa 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 sa b∀ (c : α), ¬r a c ¬r b c) :
theorem set.subsingleton.is_strong_antichain {α : Type u_1} {s : set α} (hs : s.subsingleton) (r : α → α → Prop) :