Relations holding pairwise #
This file defines pairwise relations and pairwise disjoint indexed sets.
Main declarations #
pairwise:pairwise rstates thatr i jfor alli ≠ j.set.pairwise:s.pairwise rstates thatr i jfor alli ≠ jwithi, j ∈ s.set.pairwise_disjoint:s.pairwise_disjoint fstates that images underfof distinct elements ofsare either equal ordisjoint.
Notes #
The spelling s.pairwise_disjoint id is preferred over s.pairwise disjoint to permit dot notation
on set.pairwise_disjoint, even though the latter unfolds to something nicer.
theorem
pairwise.mono
{α : Type u_1}
{r p : α → α → Prop}
(hr : pairwise r)
(h : ∀ ⦃i j : α⦄, r i j → p i j) :
pairwise p
theorem
symmetric.pairwise_on
{α : Type u_1}
{ι : Type u_2}
{r : α → α → Prop}
[linear_order ι]
(hr : symmetric r)
(f : ι → α) :
theorem
pairwise_disjoint_on
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
[linear_order ι]
(f : ι → α) :
theorem
function.injective_iff_pairwise_ne
{α : Type u_1}
{ι : Type u_2}
{f : ι → α} :
function.injective f ↔ pairwise (ne on f)
theorem
function.injective.pairwise_ne
{α : Type u_1}
{ι : Type u_2}
{f : ι → α} :
function.injective f → pairwise (ne on f)
Alias of function.injective_iff_pairwise_ne.
theorem
set.pairwise_of_forall
{α : Type u_1}
(s : set α)
(r : α → α → Prop)
(h : ∀ (a b : α), r a b) :
s.pairwise r
theorem
set.pairwise.imp
{α : Type u_1}
{r p : α → α → Prop}
{s : set α}
(h : s.pairwise r)
(hpq : ∀ ⦃a b : α⦄, r a b → p a b) :
s.pairwise p
@[protected]
theorem
set.subsingleton.pairwise
{α : Type u_1}
{s : set α}
(h : s.subsingleton)
(r : α → α → Prop) :
s.pairwise r
@[simp]
theorem
set.nonempty.pairwise_eq_iff_exists_eq
{α : Type u_1}
{ι : Type u_2}
{s : set α}
(hs : s.nonempty)
{f : α → ι} :
For a nonempty set s, a function f takes pairwise equal values on s if and only if
for some z in the codomain, f takes value z on all x ∈ s. See also
set.pairwise_eq_iff_exists_eq for a version that assumes [nonempty ι] instead of
set.nonempty s.
theorem
set.pairwise_eq_iff_exists_eq
{α : Type u_1}
{ι : Type u_2}
[nonempty ι]
(s : set α)
(f : α → ι) :
A function f : α → ι with nonempty codomain takes pairwise equal values on a set s if and
only if for some z in the codomain, f takes value z on all x ∈ s. See also
set.nonempty.pairwise_eq_iff_exists_eq for a version that assumes set.nonempty s instead of
[nonempty ι].
theorem
set.pairwise.on_injective
{α : Type u_1}
{ι : Type u_2}
{r : α → α → Prop}
{f : ι → α}
{s : set α}
(hs : s.pairwise r)
(hf : function.injective f)
(hfs : ∀ (x : ι), f x ∈ s) :
theorem
set.inj_on.pairwise_image
{α : Type u_1}
{ι : Type u_2}
{r : α → α → Prop}
{f : ι → α}
{s : set ι}
(h : set.inj_on f s) :
theorem
set.pairwise_Union
{α : Type u_1}
{ι : Type u_2}
{r : α → α → Prop}
{f : ι → set α}
(h : directed has_subset.subset f) :
theorem
set.pairwise_sUnion
{α : Type u_1}
{r : α → α → Prop}
{s : set (set α)}
(h : directed_on has_subset.subset s) :
theorem
pairwise.set_pairwise
{α : Type u_1}
{r : α → α → Prop}
(h : pairwise r)
(s : set α) :
s.pairwise r
Alias of pairwise_subtype_iff_pairwise_set.
Alias of pairwise_subtype_iff_pairwise_set.
def
set.pairwise_disjoint
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
(s : set ι)
(f : ι → α) :
Prop
A set is pairwise_disjoint under f, if the images of any distinct two elements under f
are disjoint.
s.pairwise disjoint is (definitionally) the same as s.pairwise_disjoint id. We prefer the latter
in order to allow dot notation on set.pairwise_disjoint, even though the former unfolds more
nicely.
Equations
- s.pairwise_disjoint f = s.pairwise (disjoint on f)
theorem
set.pairwise_disjoint.subset
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s t : set ι}
{f : ι → α}
(ht : t.pairwise_disjoint f)
(h : s ⊆ t) :
theorem
set.pairwise_disjoint.mono_on
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f g : ι → α}
(hs : s.pairwise_disjoint f)
(h : ∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i) :
theorem
set.pairwise_disjoint.mono
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f g : ι → α}
(hs : s.pairwise_disjoint f)
(h : g ≤ f) :
@[simp]
theorem
set.pairwise_disjoint_empty
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{f : ι → α} :
@[simp]
theorem
set.pairwise_disjoint_singleton
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
(i : ι)
(f : ι → α) :
{i}.pairwise_disjoint f
theorem
set.pairwise_disjoint_insert
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f : ι → α}
{i : ι} :
(insert i s).pairwise_disjoint f ↔ s.pairwise_disjoint f ∧ ∀ (j : ι), j ∈ s → i ≠ j → disjoint (f i) (f j)
theorem
set.pairwise_disjoint.insert
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f : ι → α}
(hs : s.pairwise_disjoint f)
{i : ι}
(h : ∀ (j : ι), j ∈ s → i ≠ j → disjoint (f i) (f j)) :
(insert i s).pairwise_disjoint f
theorem
set.pairwise_disjoint.image_of_le
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f : ι → α}
(hs : s.pairwise_disjoint f)
{g : ι → ι}
(hg : f ∘ g ≤ f) :
(g '' s).pairwise_disjoint f
theorem
set.inj_on.pairwise_disjoint_image
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[semilattice_inf α]
[order_bot α]
{f : ι → α}
{g : ι' → ι}
{s : set ι'}
(h : set.inj_on g s) :
(g '' s).pairwise_disjoint f ↔ s.pairwise_disjoint (f ∘ g)
theorem
set.pairwise_disjoint.range
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f : ι → α}
(g : ↥s → ι)
(hg : ∀ (i : ↥s), f (g i) ≤ f ↑i)
(ht : s.pairwise_disjoint f) :
(set.range g).pairwise_disjoint f
theorem
set.pairwise_disjoint_union
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s t : set ι}
{f : ι → α} :
(s ∪ t).pairwise_disjoint f ↔ s.pairwise_disjoint f ∧ t.pairwise_disjoint f ∧ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → disjoint (f i) (f j)
theorem
set.pairwise_disjoint.union
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s t : set ι}
{f : ι → α}
(hs : s.pairwise_disjoint f)
(ht : t.pairwise_disjoint f)
(h : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → disjoint (f i) (f j)) :
(s ∪ t).pairwise_disjoint f
theorem
set.pairwise_disjoint_Union
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[semilattice_inf α]
[order_bot α]
{f : ι → α}
{g : ι' → set ι}
(h : directed has_subset.subset g) :
(⋃ (n : ι'), g n).pairwise_disjoint f ↔ ∀ ⦃n : ι'⦄, (g n).pairwise_disjoint f
theorem
set.pairwise_disjoint_sUnion
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{f : ι → α}
{s : set (set ι)}
(h : directed_on has_subset.subset s) :
(⋃₀s).pairwise_disjoint f ↔ ∀ ⦃a : set ι⦄, a ∈ s → a.pairwise_disjoint f
theorem
set.pairwise_disjoint.elim
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f : ι → α}
(hs : s.pairwise_disjoint f)
{i j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(h : ¬disjoint (f i) (f j)) :
i = j
theorem
set.pairwise_disjoint.elim'
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f : ι → α}
(hs : s.pairwise_disjoint f)
{i j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(h : f i ⊓ f j ≠ ⊥) :
i = j
theorem
set.pairwise_disjoint.eq_of_le
{α : Type u_1}
{ι : Type u_2}
[semilattice_inf α]
[order_bot α]
{s : set ι}
{f : ι → α}
(hs : s.pairwise_disjoint f)
{i j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(hf : f i ≠ ⊥)
(hij : f i ≤ f j) :
i = j
theorem
set.pairwise_disjoint.bUnion
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[complete_lattice α]
{s : set ι'}
{g : ι' → set ι}
{f : ι → α}
(hs : s.pairwise_disjoint (λ (i' : ι'), ⨆ (i : ι) (H : i ∈ g i'), f i))
(hg : ∀ (i : ι'), i ∈ s → (g i).pairwise_disjoint f) :
(⋃ (i : ι') (H : i ∈ s), g i).pairwise_disjoint f
Bind operation for set.pairwise_disjoint. If you want to only consider finsets of indices, you
can use set.pairwise_disjoint.bUnion_finset.
Pairwise disjoint set of sets #
theorem
set.pairwise_disjoint_fiber
{α : Type u_1}
{ι : Type u_2}
(f : ι → α)
(s : set α) :
s.pairwise_disjoint (λ (a : α), f ⁻¹' {a})
theorem
set.pairwise_disjoint.elim_set
{α : Type u_1}
{ι : Type u_2}
{s : set ι}
{f : ι → set α}
(hs : s.pairwise_disjoint f)
{i j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(a : α)
(hai : a ∈ f i)
(haj : a ∈ f j) :
i = j
noncomputable
def
set.bUnion_eq_sigma_of_disjoint
{α : Type u_1}
{ι : Type u_2}
{s : set ι}
{f : ι → set α}
(h : s.pairwise_disjoint f) :
Equivalence between a disjoint bounded union and a dependent sum.
Equations
- set.bUnion_eq_sigma_of_disjoint h = (equiv.set_congr set.bUnion_eq_sigma_of_disjoint._proof_1).trans (set.Union_eq_sigma_of_disjoint _)