Relations holding pairwise #
This file develops pairwise relations and defines pairwise disjoint indexed sets.
We also prove many basic facts about Pairwise. It is possible that an intermediate file,
with more imports than Logic.Pairwise but not importing Data.Set.Lattice would be appropriate
to hold many of these basic facts.
Main declarations #
Set.PairwiseDisjoint:s.PairwiseDisjoint fstates that images underfof distinct elements ofsare either equal orDisjoint.
Notes #
The spelling s.PairwiseDisjoint id is preferred over s.Pairwise Disjoint to permit dot notation
on Set.PairwiseDisjoint, even though the latter unfolds to something nicer.
theorem
pairwise_disjoint_on_bool
{α : Type u_1}
[inst : SemilatticeInf α]
[inst : OrderBot α]
{a : α}
{b : α}
:
theorem
pairwise_disjoint_on
{α : Type u_1}
{ι : Type u_2}
[inst : SemilatticeInf α]
[inst : OrderBot α]
[inst : LinearOrder ι]
(f : ι → α)
:
theorem
Set.Pairwise.mono
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{t : Set α}
(h : t ⊆ s)
(hs : Set.Pairwise s r)
:
Set.Pairwise t r
theorem
Set.Pairwise.mono'
{α : Type u_1}
{r : α → α → Prop}
{p : α → α → Prop}
{s : Set α}
(H : r ≤ p)
(hr : Set.Pairwise s r)
:
Set.Pairwise s p
theorem
Set.Subsingleton.pairwise
{α : Type u_1}
{s : Set α}
(h : Set.Subsingleton s)
(r : α → α → Prop)
:
Set.Pairwise s r
@[simp]
theorem
Set.Pairwise.of_refl
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
[inst : IsRefl α r]
:
Set.Pairwise s r → ⦃a : α⦄ → a ∈ s → ⦃b : α⦄ → b ∈ s → r a b
Alias of the forward direction of Set.pairwise_iff_of_refl.
theorem
Set.Nonempty.pairwise_iff_exists_forall
{α : Type u_1}
{ι : Type u_2}
{r : α → α → Prop}
{f : ι → α}
[inst : IsEquiv α r]
{s : Set ι}
(hs : Set.Nonempty s)
:
Set.Pairwise s (r on f) ↔ ∃ z, (x : ι) → x ∈ s → r (f x) z
theorem
Set.Nonempty.pairwise_eq_iff_exists_eq
{α : Type u_1}
{ι : Type u_2}
{s : Set α}
(hs : Set.Nonempty s)
{f : α → ι}
:
(Set.Pairwise s fun x y => f x = f y) ↔ ∃ z, ∀ (x : α), x ∈ s → f x = z
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∈ 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_2}
{ι : Type u_1}
[inst : Nonempty ι]
(s : Set α)
(f : α → ι)
:
(Set.Pairwise s fun x y => f x = f y) ↔ ∃ z, ∀ (x : α), x ∈ s → f x = z
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∈ s. See also
Set.Nonempty.pairwise_eq_iff_exists_eq for a version that assumes Set.Nonempty s instead of
[Nonempty ι].
theorem
Set.pairwise_union
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{t : Set α}
:
Set.Pairwise (s ∪ t) r ↔ Set.Pairwise s r ∧ Set.Pairwise t r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a
theorem
Set.pairwise_union_of_symmetric
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{t : Set α}
(hr : Symmetric r)
:
Set.Pairwise (s ∪ t) r ↔ Set.Pairwise s r ∧ Set.Pairwise t r ∧ ((a : α) → a ∈ s → (b : α) → b ∈ t → a ≠ b → r a b)
theorem
Set.pairwise_insert
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
:
Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a
theorem
Set.pairwise_insert_of_not_mem
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
(ha : ¬a ∈ s)
:
Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → r a b ∧ r b a
theorem
Set.Pairwise.insert
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
(hs : Set.Pairwise s r)
(h : ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a)
:
Set.Pairwise (insert a s) r
theorem
Set.Pairwise.insert_of_not_mem
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
(ha : ¬a ∈ s)
(hs : Set.Pairwise s r)
(h : ∀ (b : α), b ∈ s → r a b ∧ r b a)
:
Set.Pairwise (insert a s) r
theorem
Set.pairwise_insert_of_symmetric
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
(hr : Symmetric r)
:
Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ((b : α) → b ∈ s → a ≠ b → r a b)
theorem
Set.pairwise_insert_of_symmetric_of_not_mem
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
(hr : Symmetric r)
(ha : ¬a ∈ s)
:
Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ((b : α) → b ∈ s → r a b)
theorem
Set.Pairwise.insert_of_symmetric
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
(hs : Set.Pairwise s r)
(hr : Symmetric r)
(h : (b : α) → b ∈ s → a ≠ b → r a b)
:
Set.Pairwise (insert a s) r
theorem
Set.Pairwise.insert_of_symmetric_of_not_mem
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{a : α}
(hs : Set.Pairwise s r)
(hr : Symmetric r)
(ha : ¬a ∈ s)
(h : (b : α) → b ∈ s → r a b)
:
Set.Pairwise (insert a s) r
theorem
Set.pairwise_pair
{α : Type u_1}
{r : α → α → Prop}
{a : α}
{b : α}
:
Set.Pairwise {a, b} r ↔ a ≠ b → r a b ∧ r b a
theorem
Set.pairwise_pair_of_symmetric
{α : Type u_1}
{r : α → α → Prop}
{a : α}
{b : α}
(hr : Symmetric r)
:
Set.Pairwise {a, b} r ↔ a ≠ b → r a b
@[simp]
Alias of the forward direction of Set.pairwise_bot_iff.
theorem
Set.InjOn.pairwise_image
{α : Type u_2}
{ι : Type u_1}
{r : α → α → Prop}
{f : ι → α}
{s : Set ι}
(h : Set.InjOn f s)
:
Set.Pairwise (f '' s) r ↔ Set.Pairwise s (r on f)
theorem
Set.pairwise_unionᵢ
{α : Type u_1}
{ι : Type u_2}
{r : α → α → Prop}
{f : ι → Set α}
(h : Directed (fun x x_1 => x ⊆ x_1) f)
:
Set.Pairwise (Set.unionᵢ fun n => f n) r ↔ ∀ (n : ι), Set.Pairwise (f n) r
theorem
Set.pairwise_unionₛ
{α : Type u_1}
{r : α → α → Prop}
{s : Set (Set α)}
(h : DirectedOn (fun x x_1 => x ⊆ x_1) s)
:
Set.Pairwise (⋃₀ s) r ↔ ∀ (a : Set α), a ∈ s → Set.Pairwise a r
theorem
pairwise_subtype_iff_pairwise_set
{α : Type u_1}
(s : Set α)
(r : α → α → Prop)
:
(Pairwise fun x y => r ↑x ↑y) ↔ Set.Pairwise s r
theorem
Set.Pairwise.subtype
{α : Type u_1}
(s : Set α)
(r : α → α → Prop)
:
Set.Pairwise s r → Pairwise fun x y => r ↑x ↑y
Alias of the reverse direction of pairwise_subtype_iff_pairwise_set.
theorem
Pairwise.set_of_subtype
{α : Type u_1}
(s : Set α)
(r : α → α → Prop)
:
(Pairwise fun x y => r ↑x ↑y) → Set.Pairwise s r
Alias of the forward direction of pairwise_subtype_iff_pairwise_set.
def
Set.PairwiseDisjoint
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
(s : Set ι)
(f : ι → α)
:
A set is PairwiseDisjoint under f, if the images of any distinct two elements under f
are disjoint.
s.Pairwise Disjoint is (definitionally) the same as s.PairwiseDisjoint id. We prefer the latter
in order to allow dot notation on Set.PairwiseDisjoint, even though the former unfolds more
nicely.
Equations
- Set.PairwiseDisjoint s f = Set.Pairwise s (Disjoint on f)
theorem
Set.PairwiseDisjoint.subset
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{t : Set ι}
{f : ι → α}
(ht : Set.PairwiseDisjoint t f)
(h : s ⊆ t)
:
theorem
Set.PairwiseDisjoint.mono_on
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
{g : ι → α}
(hs : Set.PairwiseDisjoint s f)
(h : ∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i)
:
theorem
Set.PairwiseDisjoint.mono
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
{g : ι → α}
(hs : Set.PairwiseDisjoint s f)
(h : g ≤ f)
:
@[simp]
theorem
Set.pairwiseDisjoint_empty
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{f : ι → α}
:
@[simp]
theorem
Set.pairwiseDisjoint_singleton
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
(i : ι)
(f : ι → α)
:
Set.PairwiseDisjoint {i} f
theorem
Set.pairwiseDisjoint_insert
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
{i : ι}
:
Set.PairwiseDisjoint (insert i s) f ↔ Set.PairwiseDisjoint s f ∧ ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (f i) (f j)
theorem
Set.pairwiseDisjoint_insert_of_not_mem
{α : Type u_2}
{ι : Type u_1}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
{i : ι}
(hi : ¬i ∈ s)
:
Set.PairwiseDisjoint (insert i s) f ↔ Set.PairwiseDisjoint s f ∧ ∀ (j : ι), j ∈ s → Disjoint (f i) (f j)
theorem
Set.PairwiseDisjoint.insert
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s f)
{i : ι}
(h : ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (f i) (f j))
:
Set.PairwiseDisjoint (insert i s) f
theorem
Set.PairwiseDisjoint.insert_of_not_mem
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s f)
{i : ι}
(hi : ¬i ∈ s)
(h : ∀ (j : ι), j ∈ s → Disjoint (f i) (f j))
:
Set.PairwiseDisjoint (insert i s) f
theorem
Set.PairwiseDisjoint.image_of_le
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s f)
{g : ι → ι}
(hg : f ∘ g ≤ f)
:
Set.PairwiseDisjoint (g '' s) f
theorem
Set.InjOn.pairwiseDisjoint_image
{α : Type u_3}
{ι : Type u_2}
{ι' : Type u_1}
[inst : PartialOrder α]
[inst : OrderBot α]
{f : ι → α}
{g : ι' → ι}
{s : Set ι'}
(h : Set.InjOn g s)
:
Set.PairwiseDisjoint (g '' s) f ↔ Set.PairwiseDisjoint s (f ∘ g)
theorem
Set.PairwiseDisjoint.range
{α : Type u_2}
{ι : Type u_1}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
(g : ↑s → ι)
(hg : ∀ (i : ↑s), f (g i) ≤ f ↑i)
(ht : Set.PairwiseDisjoint s f)
:
theorem
Set.pairwiseDisjoint_union
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{t : Set ι}
{f : ι → α}
:
Set.PairwiseDisjoint (s ∪ t) f ↔ Set.PairwiseDisjoint s f ∧ Set.PairwiseDisjoint t f ∧ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)
theorem
Set.PairwiseDisjoint.union
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{t : Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s f)
(ht : Set.PairwiseDisjoint t f)
(h : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j))
:
Set.PairwiseDisjoint (s ∪ t) f
theorem
Set.pairwiseDisjoint_unionᵢ
{α : Type u_3}
{ι : Type u_1}
{ι' : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{f : ι → α}
{g : ι' → Set ι}
(h : Directed (fun x x_1 => x ⊆ x_1) g)
:
Set.PairwiseDisjoint (Set.unionᵢ fun n => g n) f ↔ ∀ ⦃n : ι'⦄, Set.PairwiseDisjoint (g n) f
theorem
Set.pairwiseDisjoint_unionₛ
{α : Type u_2}
{ι : Type u_1}
[inst : PartialOrder α]
[inst : OrderBot α]
{f : ι → α}
{s : Set (Set ι)}
(h : DirectedOn (fun x x_1 => x ⊆ x_1) s)
:
Set.PairwiseDisjoint (⋃₀ s) f ↔ ∀ ⦃a : Set ι⦄, a ∈ s → Set.PairwiseDisjoint a f
theorem
Set.PairwiseDisjoint.elim
{α : Type u_1}
{ι : Type u_2}
[inst : PartialOrder α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s f)
{i : ι}
{j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(h : ¬Disjoint (f i) (f j))
:
i = j
theorem
Set.PairwiseDisjoint.elim'
{α : Type u_1}
{ι : Type u_2}
[inst : SemilatticeInf α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s f)
{i : ι}
{j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(h : f i ⊓ f j ≠ ⊥)
:
i = j
theorem
Set.PairwiseDisjoint.eq_of_le
{α : Type u_1}
{ι : Type u_2}
[inst : SemilatticeInf α]
[inst : OrderBot α]
{s : Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s f)
{i : ι}
{j : ι}
(hi : i ∈ s)
(hj : j ∈ s)
(hf : f i ≠ ⊥)
(hij : f i ≤ f j)
:
i = j
theorem
Set.PairwiseDisjoint.bunionᵢ
{α : Type u_3}
{ι : Type u_2}
{ι' : Type u_1}
[inst : CompleteLattice α]
{s : Set ι'}
{g : ι' → Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s fun i' => ⨆ i, ⨆ h, f i)
(hg : ∀ (i : ι'), i ∈ s → Set.PairwiseDisjoint (g i) f)
:
Set.PairwiseDisjoint (Set.unionᵢ fun i => Set.unionᵢ fun h => g i) f
Bind operation for Set.PairwiseDisjoint. If you want to only consider finsets of indices, you
can use Set.PairwiseDisjoint.bunionᵢ_finset.
Pairwise disjoint set of sets #
theorem
Set.pairwiseDisjoint_range_singleton
{ι : Type u_1}
:
Set.PairwiseDisjoint (Set.range singleton) id
theorem
Set.pairwiseDisjoint_fiber
{α : Type u_1}
{ι : Type u_2}
(f : ι → α)
(s : Set α)
:
Set.PairwiseDisjoint s fun a => f ⁻¹' {a}
theorem
Set.bunionᵢ_diff_bunionᵢ_eq
{α : Type u_2}
{ι : Type u_1}
{s : Set ι}
{t : Set ι}
{f : ι → Set α}
(h : Set.PairwiseDisjoint (s ∪ t) f)
:
((Set.unionᵢ fun i => Set.unionᵢ fun h => f i) \ Set.unionᵢ fun i => Set.unionᵢ fun h => f i) = Set.unionᵢ fun i => Set.unionᵢ fun h => f i
noncomputable def
Set.bunionᵢEqSigmaOfDisjoint
{α : Type u_1}
{ι : Type u_2}
{s : Set ι}
{f : ι → Set α}
(h : Set.PairwiseDisjoint s f)
:
↑(Set.unionᵢ fun i => Set.unionᵢ fun h => f i) ≃ (i : ↑s) × ↑(f ↑i)
Equivalence between a disjoint bounded union and a dependent sum.
Equations
- One or more equations did not get rendered due to their size.
theorem
Set.pairwiseDisjoint_image_right_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(hf : ∀ (a : α), a ∈ s → Function.Injective (f a))
:
(Set.PairwiseDisjoint s fun a => f a '' t) ↔ Set.InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
The partial images of a binary function f whose partial evaluations are injective are pairwise
disjoint iff f is injective .
theorem
Set.pairwiseDisjoint_image_left_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(hf : ∀ (b : β), b ∈ t → Function.Injective fun a => f a b)
:
(Set.PairwiseDisjoint t fun b => (fun a => f a b) '' s) ↔ Set.InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
The partial images of a binary function f whose partial evaluations are injective are pairwise
disjoint iff f is injective .
theorem
Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ
{α : Type u_1}
{ι : Type u_2}
{f : ι → Set α}
{s : Set ι}
{t : Set ι}
(h₀ : Set.PairwiseDisjoint (s ∪ t) f)
(h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i))
(h : (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) ⊆ Set.unionᵢ fun i => Set.unionᵢ fun h => f i)
:
s ⊆ t
theorem
Pairwise.subset_of_bunionᵢ_subset_bunionᵢ
{α : Type u_2}
{ι : Type u_1}
{f : ι → Set α}
{s : Set ι}
{t : Set ι}
(h₀ : Pairwise (Disjoint on f))
(h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i))
(h : (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) ⊆ Set.unionᵢ fun i => Set.unionᵢ fun h => f i)
:
s ⊆ t
theorem
Pairwise.bunionᵢ_injective
{α : Type u_2}
{ι : Type u_1}
{f : ι → Set α}
(h₀ : Pairwise (Disjoint on f))
(h₁ : ∀ (i : ι), Set.Nonempty (f i))
:
Function.Injective fun s => Set.unionᵢ fun i => Set.unionᵢ fun h => f i