Relations holding pairwise on finite sets #
In this file we prove a few results about the interaction of set.pairwise_disjoint and finset.
@[protected, instance]
def
pairwise.decidable
{α : Type u_1}
[decidable_eq α]
{r : α → α → Prop}
[decidable_rel r]
{s : finset α} :
Equations
- pairwise.decidable = decidable_of_iff' (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≠ b → r a b) pairwise.decidable._proof_1
theorem
set.pairwise_disjoint.elim_finset
{α : Type u_1}
{ι : Type u_2}
[decidable_eq α]
{s : set ι}
{f : ι → finset α}
(hs : s.pairwise_disjoint f)
{i j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(a : α)
(hai : a ∈ f i)
(haj : a ∈ f j) :
i = j
theorem
set.pairwise_disjoint.image_finset_of_le
{α : Type u_1}
{ι : Type u_2}
[decidable_eq ι]
[semilattice_inf α]
[order_bot α]
{s : finset ι}
{f : ι → α}
(hs : ↑s.pairwise_disjoint f)
{g : ι → ι}
(hf : ∀ (a : ι), f (g a) ≤ f a) :
↑(finset.image g s).pairwise_disjoint f
theorem
set.pairwise_disjoint.bUnion_finset
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[lattice α]
[order_bot α]
{s : set ι'}
{g : ι' → finset ι}
{f : ι → α}
(hs : s.pairwise_disjoint (λ (i' : ι'), (g i').sup f))
(hg : ∀ (i : ι'), i ∈ s → ↑(g i).pairwise_disjoint f) :
(⋃ (i : ι') (H : i ∈ s), ↑(g i)).pairwise_disjoint f
Bind operation for set.pairwise_disjoint. In a complete lattice, you can use
set.pairwise_disjoint.bUnion.