Documentation

Mathlib.Data.Set.Sigma

Sets in sigma types #

This file defines Set.sigma, the indexed sum of sets.

@[simp]
theorem Set.range_sigmaMk {ι : Type u_1} {α : ιType u_3} (i : ι) :
Set.range (Sigma.mk i) = Sigma.fst ⁻¹' {i}
theorem Set.preimage_image_sigmaMk_of_ne {ι : Type u_1} {α : ιType u_3} {i : ι} {j : ι} (h : i j) (s : Set (α j)) :
theorem Set.image_sigmaMk_preimage_sigmaMap_subset {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} {β : ι'Type u_5} (f : ιι') (g : (i : ι) → α iβ (f i)) (i : ι) (s : Set (β (f i))) :
Sigma.mk i '' (g i ⁻¹' s) Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)
theorem Set.image_sigmaMk_preimage_sigmaMap {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} {β : ι'Type u_5} {f : ιι'} (hf : Function.Injective f) (g : (i : ι) → α iβ (f i)) (i : ι) (s : Set (β (f i))) :
Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)
def Set.sigma {ι : Type u_1} {α : ιType u_3} (s : Set ι) (t : (i : ι) → Set (α i)) :
Set ((i : ι) × α i)

Indexed sum of sets. s.sigma t is the set of dependent pairs ⟨i, a⟩ such that i ∈ s and a ∈ t i.

Equations
  • s.sigma t = {x : (i : ι) × α i | x.fst s x.snd t x.fst}
Instances For
    @[simp]
    theorem Set.mem_sigma_iff {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {x : (i : ι) × α i} :
    x s.sigma t x.fst s x.snd t x.fst
    theorem Set.mk_sigma_iff {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i} :
    i, a s.sigma t i s a t i
    theorem Set.mk_mem_sigma {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i} (hi : i s) (ha : a t i) :
    i, a s.sigma t
    theorem Set.sigma_mono {ι : Type u_1} {α : ιType u_3} {s₁ : Set ι} {s₂ : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} (hs : s₁ s₂) (ht : ∀ (i : ι), t₁ i t₂ i) :
    s₁.sigma t₁ s₂.sigma t₂
    theorem Set.sigma_subset_iff {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {u : Set ((i : ι) × α i)} :
    s.sigma t u ∀ ⦃i : ι⦄, i s∀ ⦃a : α i⦄, a t ii, a u
    theorem Set.forall_sigma_iff {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α iProp} :
    (∀ xs.sigma t, p x) ∀ ⦃i : ι⦄, i s∀ ⦃a : α i⦄, a t ip i, a
    theorem Set.exists_sigma_iff {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α iProp} :
    (∃ xs.sigma t, p x) is, at i, p i, a
    @[simp]
    theorem Set.sigma_empty {ι : Type u_1} {α : ιType u_3} {s : Set ι} :
    (s.sigma fun (i : ι) => ) =
    @[simp]
    theorem Set.empty_sigma {ι : Type u_1} {α : ιType u_3} {t : (i : ι) → Set (α i)} :
    .sigma t =
    theorem Set.univ_sigma_univ {ι : Type u_1} {α : ιType u_3} {i : ι} :
    (Set.univ.sigma fun (x : ι) => Set.univ) = Set.univ
    @[simp]
    theorem Set.sigma_univ {ι : Type u_1} {α : ιType u_3} {s : Set ι} :
    (s.sigma fun (x : ι) => Set.univ) = Sigma.fst ⁻¹' s
    @[simp]
    theorem Set.univ_sigma_preimage_mk {ι : Type u_1} {α : ιType u_3} (s : Set ((i : ι) × α i)) :
    (Set.univ.sigma fun (i : ι) => Sigma.mk i ⁻¹' s) = s
    @[simp]
    theorem Set.singleton_sigma {ι : Type u_1} {α : ιType u_3} {t : (i : ι) → Set (α i)} {i : ι} :
    {i}.sigma t = Sigma.mk i '' t i
    @[simp]
    theorem Set.sigma_singleton {ι : Type u_1} {α : ιType u_3} {s : Set ι} {a : (i : ι) → α i} :
    (s.sigma fun (i : ι) => {a i}) = (fun (i : ι) => i, a i) '' s
    theorem Set.singleton_sigma_singleton {ι : Type u_1} {α : ιType u_3} {i : ι} {a : (i : ι) → α i} :
    ({i}.sigma fun (i : ι) => {a i}) = {i, a i}
    @[simp]
    theorem Set.union_sigma {ι : Type u_1} {α : ιType u_3} {s₁ : Set ι} {s₂ : Set ι} {t : (i : ι) → Set (α i)} :
    (s₁ s₂).sigma t = s₁.sigma t s₂.sigma t
    @[simp]
    theorem Set.sigma_union {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} :
    (s.sigma fun (i : ι) => t₁ i t₂ i) = s.sigma t₁ s.sigma t₂
    theorem Set.sigma_inter_sigma {ι : Type u_1} {α : ιType u_3} {s₁ : Set ι} {s₂ : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} :
    s₁.sigma t₁ s₂.sigma t₂ = (s₁ s₂).sigma fun (i : ι) => t₁ i t₂ i
    theorem biSup_sigma {ι : Type u_1} {α : ιType u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma αβ) :
    ijs.sigma t, f ij = is, jt i, f i, j
    theorem biSup_sigma' {ι : Type u_1} {α : ιType u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α iβ) :
    is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
    theorem biInf_sigma {ι : Type u_1} {α : ιType u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma αβ) :
    ijs.sigma t, f ij = is, jt i, f i, j
    theorem biInf_sigma' {ι : Type u_1} {α : ιType u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α iβ) :
    is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
    theorem Set.biUnion_sigma {ι : Type u_1} {α : ιType u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma αSet β) :
    ijs.sigma t, f ij = is, jt i, f i, j
    theorem Set.biUnion_sigma' {ι : Type u_1} {α : ιType u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α iSet β) :
    is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
    theorem Set.biInter_sigma {ι : Type u_1} {α : ιType u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma αSet β) :
    ijs.sigma t, f ij = is, jt i, f i, j
    theorem Set.biInter_sigma' {ι : Type u_1} {α : ιType u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α iSet β) :
    is, jt i, f i j = ijs.sigma t, f ij.fst ij.snd
    theorem Set.insert_sigma {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} :
    (insert i s).sigma t = Sigma.mk i '' t i s.sigma t
    theorem Set.sigma_insert {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i} :
    (s.sigma fun (i : ι) => insert (a i) (t i)) = (fun (i : ι) => i, a i) '' s s.sigma t
    theorem Set.sigma_preimage_eq {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ιType u_7} {f : ι'ι} {g : (i : ι) → β iα i} :
    ((f ⁻¹' s).sigma fun (i : ι') => g (f i) ⁻¹' t (f i)) = (fun (p : (i : ι') × β (f i)) => f p.fst, g (f p.fst) p.snd) ⁻¹' s.sigma t
    theorem Set.sigma_preimage_left {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {f : ι'ι} :
    ((f ⁻¹' s).sigma fun (i : ι') => t (f i)) = (fun (p : (i : ι') × α (f i)) => f p.fst, p.snd) ⁻¹' s.sigma t
    theorem Set.sigma_preimage_right {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ιType u_7} {g : (i : ι) → β iα i} :
    (s.sigma fun (i : ι) => g i ⁻¹' t i) = (fun (p : (i : ι) × β i) => p.fst, g p.fst p.snd) ⁻¹' s.sigma t
    theorem Set.preimage_sigmaMap_sigma {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} {α' : ι'Type u_8} (f : ιι') (g : (i : ι) → α iα' (f i)) (s : Set ι') (t : (i : ι') → Set (α' i)) :
    Sigma.map f g ⁻¹' s.sigma t = (f ⁻¹' s).sigma fun (i : ι) => g i ⁻¹' t (f i)
    @[simp]
    theorem Set.mk_preimage_sigma {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hi : i s) :
    Sigma.mk i ⁻¹' s.sigma t = t i
    @[simp]
    theorem Set.mk_preimage_sigma_eq_empty {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hi : is) :
    Sigma.mk i ⁻¹' s.sigma t =
    theorem Set.mk_preimage_sigma_eq_if {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [DecidablePred fun (x : ι) => x s] :
    Sigma.mk i ⁻¹' s.sigma t = if i s then t i else
    theorem Set.mk_preimage_sigma_fn_eq_if {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {β : Type u_8} [DecidablePred fun (x : ι) => x s] (g : βα i) :
    (fun (b : β) => i, g b) ⁻¹' s.sigma t = if i s then g ⁻¹' t i else
    theorem Set.sigma_univ_range_eq {ι : Type u_1} {α : ιType u_3} {β : ιType u_7} {f : (i : ι) → α iβ i} :
    (Set.univ.sigma fun (i : ι) => Set.range (f i)) = Set.range fun (x : (i : ι) × α i) => x.fst, f x.fst x.snd
    theorem Set.Nonempty.sigma {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
    s.Nonempty(∀ (i : ι), (t i).Nonempty)(s.sigma t).Nonempty
    theorem Set.Nonempty.sigma_fst {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
    (s.sigma t).Nonemptys.Nonempty
    theorem Set.Nonempty.sigma_snd {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
    (s.sigma t).Nonemptyis, (t i).Nonempty
    theorem Set.sigma_nonempty_iff {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
    (s.sigma t).Nonempty is, (t i).Nonempty
    theorem Set.sigma_eq_empty_iff {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
    s.sigma t = is, t i =
    theorem Set.image_sigmaMk_subset_sigma_left {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i} (ha : ∀ (i : ι), a i t i) :
    (fun (i : ι) => i, a i) '' s s.sigma t
    theorem Set.image_sigmaMk_subset_sigma_right {ι : Type u_1} {α : ιType u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hi : i s) :
    Sigma.mk i '' t i s.sigma t
    theorem Set.sigma_subset_preimage_fst {ι : Type u_1} {α : ιType u_3} (s : Set ι) (t : (i : ι) → Set (α i)) :
    s.sigma t Sigma.fst ⁻¹' s
    theorem Set.fst_image_sigma_subset {ι : Type u_1} {α : ιType u_3} (s : Set ι) (t : (i : ι) → Set (α i)) :
    Sigma.fst '' s.sigma t s
    theorem Set.fst_image_sigma {ι : Type u_1} {α : ιType u_3} {t : (i : ι) → Set (α i)} (s : Set ι) (ht : ∀ (i : ι), (t i).Nonempty) :
    Sigma.fst '' s.sigma t = s
    theorem Set.sigma_diff_sigma {ι : Type u_1} {α : ιType u_3} {s₁ : Set ι} {s₂ : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} :
    s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) (s₁ \ s₂).sigma t₁