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 ofs : set α
are unrelated byr : α → α → Prop
.is_strong_antichain r s
: Any two elements ofs : set α
are not related byr : α → α → Prop
to a common element.is_antichain.mk r s
: Turnss
into an antichain by keeping only the "maximal" elements.
@[protected]
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) :
theorem
is_antichain.image_compl
{α : Type u_1}
{s : set α}
[boolean_algebra α]
(hs : is_antichain has_le.le s) :
theorem
is_antichain.preimage_compl
{α : Type u_1}
{s : set α}
[boolean_algebra α]
(hs : is_antichain has_le.le s) :
theorem
set.subsingleton.is_antichain
{α : Type u_1}
{s : set α}
(hs : s.subsingleton)
(r : α → α → Prop) :
is_antichain r s
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) :
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}
Strong antichains #
An strong (upward) antichain is a set such that no two distinct elements are related to a common element.
@[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₁) :
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) :
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) :