Relations holding pairwise on finite sets #
In this file we prove a few results about the interaction of Set.PairwiseDisjoint and Finset,
as well as the interaction of List.Pairwise Disjoint and the condition of
Disjoint on List.toFinset, in Set form.
instance
instDecidablePairwiseToSetOfDecidableEqOfDecidableRel
{α : Type u_1}
[DecidableEq α]
{r : α → α → Prop}
[DecidableRel r]
{s : Finset α}
:
Decidable ((↑s).Pairwise r)
Equations
- instDecidablePairwiseToSetOfDecidableEqOfDecidableRel = decidable_of_iff' (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) ⋯
theorem
Finset.pairwiseDisjoint_range_singleton
{α : Type u_1}
:
(Set.range singleton).PairwiseDisjoint id
theorem
Set.PairwiseDisjoint.image_finset_of_le
{α : Type u_1}
{ι : Type u_2}
[SemilatticeInf α]
[OrderBot α]
[DecidableEq ι]
{s : Finset ι}
{f : ι → α}
(hs : (↑s).PairwiseDisjoint f)
{g : ι → ι}
(hf : ∀ (a : ι), f (g a) ≤ f a)
:
(↑(Finset.image g s)).PairwiseDisjoint f
theorem
Set.PairwiseDisjoint.attach
{α : Type u_1}
{ι : Type u_2}
[SemilatticeInf α]
[OrderBot α]
{s : Finset ι}
{f : ι → α}
(hs : (↑s).PairwiseDisjoint f)
:
(↑s.attach).PairwiseDisjoint (f ∘ Subtype.val)
theorem
Set.PairwiseDisjoint.biUnion_finset
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[Lattice α]
[OrderBot α]
{s : Set ι'}
{g : ι' → Finset ι}
{f : ι → α}
(hs : s.PairwiseDisjoint fun (i' : ι') => (g i').sup f)
(hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f)
:
(⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f
Bind operation for Set.PairwiseDisjoint. In a complete lattice, you can use
Set.PairwiseDisjoint.biUnion.
theorem
List.pairwise_of_coe_toFinset_pairwise
{α : Type u_1}
[DecidableEq α]
{r : α → α → Prop}
{l : List α}
(hl : (↑l.toFinset).Pairwise r)
(hn : l.Nodup)
:
List.Pairwise r l
theorem
List.pairwise_iff_coe_toFinset_pairwise
{α : Type u_1}
[DecidableEq α]
{r : α → α → Prop}
{l : List α}
(hn : l.Nodup)
(hs : Symmetric r)
:
(↑l.toFinset).Pairwise r ↔ List.Pairwise r l
theorem
List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint
{α : Type u_5}
{ι : Type u_6}
[SemilatticeInf α]
[OrderBot α]
[DecidableEq ι]
{l : List ι}
{f : ι → α}
(hl : (↑l.toFinset).PairwiseDisjoint f)
(hn : l.Nodup)
:
List.Pairwise (Disjoint on f) l
theorem
List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint
{α : Type u_5}
{ι : Type u_6}
[SemilatticeInf α]
[OrderBot α]
[DecidableEq ι]
{l : List ι}
{f : ι → α}
(hn : l.Nodup)
:
(↑l.toFinset).PairwiseDisjoint f ↔ List.Pairwise (Disjoint on f) l