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
instDecidablePairwiseToSet
{α : Type u_1}
[DecidableEq α]
{r : α → α → Prop}
[DecidableRel r]
{s : Finset α}
:
Decidable (Set.Pairwise (↑s) r)
Equations
- instDecidablePairwiseToSet = decidable_of_iff' (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r a b) (_ : Set.Pairwise (↑s) r ↔ Set.Pairwise (↑s) r)
theorem
Finset.pairwiseDisjoint_range_singleton
{α : Type u_1}
:
Set.PairwiseDisjoint (Set.range singleton) id
theorem
Set.PairwiseDisjoint.image_finset_of_le
{α : Type u_1}
{ι : Type u_2}
[SemilatticeInf α]
[OrderBot α]
[DecidableEq ι]
{s : Finset ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint (↑s) f)
{g : ι → ι}
(hf : ∀ (a : ι), f (g a) ≤ f a)
:
Set.PairwiseDisjoint (↑(Finset.image g s)) f
theorem
Set.PairwiseDisjoint.attach
{α : Type u_1}
{ι : Type u_2}
[SemilatticeInf α]
[OrderBot α]
{s : Finset ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint (↑s) f)
:
Set.PairwiseDisjoint (↑(Finset.attach s)) (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 : Set.PairwiseDisjoint s fun (i' : ι') => Finset.sup (g i') f)
(hg : ∀ i ∈ s, Set.PairwiseDisjoint (↑(g i)) f)
:
Set.PairwiseDisjoint (⋃ i ∈ s, ↑(g i)) 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 : Set.Pairwise (↑(List.toFinset l)) r)
(hn : List.Nodup l)
:
List.Pairwise r l
theorem
List.pairwise_iff_coe_toFinset_pairwise
{α : Type u_1}
[DecidableEq α]
{r : α → α → Prop}
{l : List α}
(hn : List.Nodup l)
(hs : Symmetric r)
:
Set.Pairwise (↑(List.toFinset l)) 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 : Set.PairwiseDisjoint (↑(List.toFinset l)) f)
(hn : List.Nodup l)
:
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 : List.Nodup l)
:
Set.PairwiseDisjoint (↑(List.toFinset l)) f ↔ List.Pairwise (Disjoint on f) l