Relations holding pairwise on finite sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove a few results about the interaction of set.pairwise_disjoint and finset,
as well as the interaction of list.pairwise disjoint and the condition of
disjoint on list.to_finset, in set form.
@[protected, instance]
def
pairwise.decidable
{α : Type u_1}
[decidable_eq α]
{r : α → α → Prop}
[decidable_rel r]
{s : finset α} :
theorem
set.pairwise_disjoint.image_finset_of_le
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
[decidable_eq ι]
{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.attach
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : finset ι}
{f : ι → α}
(hs : ↑s.pairwise_disjoint f) :
↑(s.attach).pairwise_disjoint (f ∘ subtype.val)
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.
theorem
list.pairwise_of_coe_to_finset_pairwise
{α : Type u_1}
[decidable_eq α]
{r : α → α → Prop}
{l : list α}
(hl : ↑(l.to_finset).pairwise r)
(hn : l.nodup) :
list.pairwise r l
theorem
list.pairwise_iff_coe_to_finset_pairwise
{α : Type u_1}
[decidable_eq α]
{r : α → α → Prop}
{l : list α}
(hn : l.nodup)
(hs : symmetric r) :
↑(l.to_finset).pairwise r ↔ list.pairwise r l
theorem
list.pairwise_disjoint_of_coe_to_finset_pairwise_disjoint
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
[decidable_eq ι]
{l : list ι}
{f : ι → α}
(hl : ↑(l.to_finset).pairwise_disjoint f)
(hn : l.nodup) :
list.pairwise (disjoint on f) l
theorem
list.pairwise_disjoint_iff_coe_to_finset_pairwise_disjoint
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
[decidable_eq ι]
{l : list ι}
{f : ι → α}
(hn : l.nodup) :
↑(l.to_finset).pairwise_disjoint f ↔ list.pairwise (disjoint on f) l