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 #

@[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 b r₁ 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 b r (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 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) :
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) :
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.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 α] :
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 = {}
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
@[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 b r (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 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) :
theorem set.subsingleton.is_strong_antichain {α : Type u_1} {s : set α} (hs : s.subsingleton) (r : α α Prop) :

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
@[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) :
@[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} :
@[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) :
theorem set.subsingleton.is_weak_antichain {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} (hs : s.subsingleton) :