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
@[protected]
theorem is_antichain.subset {α : Type u_1} {r : α α Prop} {s t : set α} (hs : s) (h : t s) :
t
theorem is_antichain.mono {α : Type u_1} {r₁ r₂ : α α Prop} {s : set α} (hs : s) (h : r₂ r₁) :
s
theorem is_antichain.mono_on {α : Type u_1} {r₁ r₂ : α α Prop} {s : set α} (hs : s) (h : s.pairwise (λ ⦃a b : α⦄, r₂ a b r₁ a b)) :
s
@[protected]
theorem is_antichain.eq {α : Type u_1} {r : α α Prop} {s : set α} (hs : 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 : 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 : set.univ) :
r
@[protected]
theorem is_antichain.subsingleton {α : Type u_1} {r : α α Prop} {s : set α} [ r] (h : s) :
@[protected]
theorem is_antichain.flip {α : Type u_1} {r : α α Prop} {s : set α} (hs : s) :
theorem is_antichain.swap {α : Type u_1} {r : α α Prop} {s : set α} (hs : s) :
theorem is_antichain.image {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} (hs : s) (f : α β) (h : ⦃a b : α⦄, r' (f a) (f b) r a b) :
(f '' s)
theorem is_antichain.preimage {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} (hs : s) {f : β α} (hf : function.injective f) (h : ⦃a b : β⦄, r' a b r (f a) (f b)) :
(f ⁻¹' s)
theorem is_antichain_insert {α : Type u_1} {r : α α Prop} {s : set α} {a : α} :
s) 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 : s) (hl : ⦃b : α⦄, b s a b ¬r b a) (hr : ⦃b : α⦄, b s a b ¬r a b) :
s)
theorem is_antichain_insert_of_symmetric {α : Type u_1} {r : α α Prop} {s : set α} {a : α} (hr : symmetric r) :
s) s ⦃b : α⦄, b s a b ¬r a b
theorem is_antichain.insert_of_symmetric {α : Type u_1} {r : α α Prop} {s : set α} {a : α} (hs : s) (hr : symmetric r) (h : ⦃b : α⦄, b s a b ¬r a b) :
s)
theorem is_antichain.image_rel_embedding {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} (hs : s) (φ : r ↪r r') :
(φ '' s)
theorem is_antichain.preimage_rel_embedding {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {t : set β} (ht : t) (φ : r ↪r r') :
(φ ⁻¹' t)
theorem is_antichain.image_rel_iso {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} (hs : s) (φ : r ≃r r') :
(φ '' s)
theorem is_antichain.preimage_rel_iso {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {t : set β} (hs : t) (φ : r ≃r r') :
(φ ⁻¹' t)
theorem is_antichain.image_rel_embedding_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} {φ : r ↪r r'} :
(φ '' s) s
theorem is_antichain.image_rel_iso_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} {φ : r ≃r r'} :
(φ '' s) s
theorem is_antichain.image_embedding {α : Type u_1} {β : Type u_2} {s : set α} [has_le α] [has_le β] (hs : s) (φ : α ↪o β) :
(φ '' s)
theorem is_antichain.preimage_embedding {α : Type u_1} {β : Type u_2} [has_le α] [has_le β] {t : set β} (ht : t) (φ : α ↪o β) :
(φ ⁻¹' t)
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 : s) (φ : α ≃o β) :
(φ '' s)
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 : t) (φ : α ≃o β) :
(φ ⁻¹' t)
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 : s) :
theorem is_antichain.to_dual_iff {α : Type u_1} {s : set α} [has_le α] :
theorem is_antichain.image_compl {α : Type u_1} {s : set α} (hs : s) :
theorem is_antichain.preimage_compl {α : Type u_1} {s : set α} (hs : s) :
theorem is_antichain_singleton {α : Type u_1} (a : α) (r : α α Prop) :
{a}
theorem set.subsingleton.is_antichain {α : Type u_1} {s : set α} (hs : s.subsingleton) (r : α α Prop) :
s
theorem is_antichain.not_lt {α : Type u_1} {s : set α} {a b : α} [preorder α] (hs : s) (ha : a s) (hb : b s) :
¬a < b
theorem is_antichain_and_least_iff {α : Type u_1} {s : set α} {a : α} [preorder α] :
s = {a}
theorem is_antichain_and_greatest_iff {α : Type u_1} {s : set α} {a : α} [preorder α] :
s = {a}
theorem is_antichain.least_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : s) :
a s = {a}
theorem is_antichain.greatest_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : s) :
a s = {a}
theorem is_least.antichain_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : a) :
s = {a}
theorem is_greatest.antichain_iff {α : Type u_1} {s : set α} {a : α} [preorder α] (hs : a) :
s = {a}
theorem is_antichain.bot_mem_iff {α : Type u_1} {s : set α} [preorder α] [order_bot α] (hs : s) :
s s = {}
theorem is_antichain.top_mem_iff {α : Type u_1} {s : set α} [preorder α] [order_top α] (hs : s) :
s s = {}
theorem is_antichain_iff_forall_not_lt {α : Type u_1} {s : set α}  :
⦃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 : s) (h : t s) :
theorem is_strong_antichain.mono {α : Type u_1} {r₁ r₂ : α α Prop} {s : set α} (hs : s) (h : r₂ r₁) :
theorem is_strong_antichain.eq {α : Type u_1} {r : α α Prop} {s : set α} (hs : 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 α} [ r] (h : s) :
s
@[protected]
theorem is_strong_antichain.subsingleton {α : Type u_1} {r : α α Prop} {s : set α} [ r] (h : s) :
@[protected]
theorem is_strong_antichain.flip {α : Type u_1} {r : α α Prop} {s : set α} [ r] (hs : s) :
s
theorem is_strong_antichain.swap {α : Type u_1} {r : α α Prop} {s : set α} [ r] (hs : s) :
theorem is_strong_antichain.image {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} (hs : s) {f : α β} (hf : function.surjective f) (h : (a b : α), r' (f a) (f b) r a b) :
(f '' s)
theorem is_strong_antichain.preimage {α : Type u_1} {β : Type u_2} {r : α α Prop} {r' : β β Prop} {s : set α} (hs : s) {f : β α} (hf : function.injective f) (h : (a b : β), r' a b r (f a) (f b)) :
(f ⁻¹' s)
theorem is_strong_antichain_insert {α : Type u_1} {r : α α Prop} {s : set α} {a : α} :
⦃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 : 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) :
t 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 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 ¬ a) ( ⦃b : Π (i : ι), α i⦄, b s a b ¬ b)
theorem is_weak_antichain_insert {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} {a : Π (i : ι), α i} :
⦃b : Π (i : ι), α i⦄, b s a b ¬ b ¬ a
@[protected]
theorem is_antichain.is_weak_antichain {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} (hs : s) :
theorem set.subsingleton.is_weak_antichain {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] {s : set (Π (i : ι), α i)} (hs : s.subsingleton) :