def
Set.sum_to_union
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
:
(i : ι) × ↥(x i) → ↥(⋃ i : ι, x i)
Equations
- Set.sum_to_union ⟨i, ⟨a, h⟩⟩ = ⟨a, ⋯⟩
Instances For
@[simp]
theorem
Set.sum_to_union_surj
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
:
Function.Surjective Set.sum_to_union
theorem
Set.sum_to_union_inj_of_disjoint
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
(h : ∀ (i j : ι), i ≠ j → x i ∩ x j = ∅)
:
Function.Injective Set.sum_to_union
theorem
Set.sum_to_union_bij_of_disjoint
{α : Type u_1}
{ι : Type u_3}
{x : ι → Set α}
(h : ∀ (i j : ι), i ≠ j → x i ∩ x j = ∅)
:
Function.Bijective Set.sum_to_union
def
sigma_reindex_bij
{ι : Type u_8}
{ι' : Type u_9}
{x : ι → Type u}
(f : Function.Bijection ι' ι)
:
Function.Bijection (Sigma (x ∘ f.val)) (Sigma x)
Equations
- sigma_reindex_bij f = ⟨fun (x_1 : Sigma (x ∘ f.val)) => match x_1 with | ⟨i', h⟩ => ⟨f.val i', h⟩, ⋯⟩
Instances For
noncomputable def
Set.IsPartition.sigma_assoc
{ι : Type u_8}
{ι' : Type u_9}
{x : ι → Type u_11}
{p : ι' → Set ι}
(h : Set.IsPartition p)
:
Function.Bijection ((i : ι) × x i) ((i' : ι') × (i : ↥(p i')) × x i.val)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Sigma.prod_distrib
{ι : Type u_8}
{ι' : ι → Type u_12}
{x : (i : ι) → ι' i → Type u_13}
:
Function.Bijection ((i : ι) → (i' : ι' i) × x i i') ((y : (i : ι) → ι' i) × ((i : ι) → x i (y i)))
Equations
- One or more equations did not get rendered due to their size.