mathlib3 documentation

data.set.sigma

Sets in sigma types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]
theorem set.range_sigma_mk {ι : Type u_1} {α : ι Type u_3} (i : ι) :
theorem set.preimage_image_sigma_mk_of_ne {ι : Type u_1} {α : ι Type u_3} {i j : ι} (h : i j) (s : set (α j)) :
theorem set.image_sigma_mk_preimage_sigma_map_subset {ι : Type u_1} {ι' : Type u_2} {α : ι Type u_3} {β : ι' Type u_4} (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_sigma_mk_preimage_sigma_map {ι : Type u_1} {ι' : Type u_2} {α : ι Type u_3} {β : ι' Type u_4} {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)
@[protected]
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
@[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
@[simp]
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₁ s₂ : set ι} {t₁ 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 i i, a⟩ u
theorem set.forall_sigma_iff {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {p : (Σ (i : ι), α i) Prop} :
( (x : Σ (i : ι), α i), x s.sigma t p x) ⦃i : ι⦄, i s ⦃a : α i⦄, a t i p i, a⟩
theorem set.exists_sigma_iff {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {p : (Σ (i : ι), α i) Prop} :
( (x : Σ (i : ι), α i) (H : x s.sigma t), p x) (i : ι) (H : i s) (a : α i) (H : a t i), p i, a⟩
@[simp]
theorem set.sigma_empty {ι : Type u_1} {α : ι Type u_3} {s : set ι} :
s.sigma (λ (i : ι), ) =
@[simp]
theorem set.empty_sigma {ι : Type u_1} {α : ι Type u_3} {t : Π (i : ι), set (α i)} :
theorem set.univ_sigma_univ {ι : Type u_1} {α : ι Type u_3} {i : ι} :
set.univ.sigma (λ (_x : ι), set.univ) = set.univ
@[simp]
theorem set.sigma_univ {ι : Type u_1} {α : ι Type u_3} {s : set ι} :
s.sigma (λ (_x : ι), set.univ) = sigma.fst ⁻¹' 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 (λ (i : ι), {a i}) = (λ (i : ι), i, a i⟩) '' s
theorem set.singleton_sigma_singleton {ι : Type u_1} {α : ι Type u_3} {i : ι} {a : Π (i : ι), α i} :
{i}.sigma (λ (i : ι), {a i}) = {i, a i⟩}
@[simp]
theorem set.union_sigma {ι : Type u_1} {α : ι Type u_3} {s₁ 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₁ t₂ : Π (i : ι), set (α i)} :
s.sigma (λ (i : ι), t₁ i t₂ i) = s.sigma t₁ s.sigma t₂
theorem set.sigma_inter_sigma {ι : Type u_1} {α : ι Type u_3} {s₁ s₂ : set ι} {t₁ t₂ : Π (i : ι), set (α i)} :
s₁.sigma t₁ s₂.sigma t₂ = (s₁ s₂).sigma (λ (i : ι), t₁ i t₂ i)
theorem set.insert_sigma {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} :
theorem set.sigma_insert {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {a : Π (i : ι), α i} :
s.sigma (λ (i : ι), has_insert.insert (a i) (t i)) = (λ (i : ι), i, a i⟩) '' s s.sigma t
theorem set.sigma_preimage_eq {ι : Type u_1} {ι' : Type u_2} {α : ι Type u_3} {β : ι Type u_4} {s : set ι} {t : Π (i : ι), set (α i)} {f : ι' ι} {g : Π (i : ι), β i α i} :
(f ⁻¹' s).sigma (λ (i : ι'), g (f i) ⁻¹' t (f i)) = (λ (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 (λ (i : ι'), t (f i)) = (λ (p : Σ (i : ι'), α (f i)), f p.fst, p.snd⟩) ⁻¹' s.sigma t
theorem set.sigma_preimage_right {ι : Type u_1} {α : ι Type u_3} {β : ι Type u_4} {s : set ι} {t : Π (i : ι), set (α i)} {g : Π (i : ι), β i α i} :
s.sigma (λ (i : ι), g i ⁻¹' t i) = (λ (p : Σ (i : ι), β i), p.fst, g p.fst p.snd⟩) ⁻¹' s.sigma t
theorem set.preimage_sigma_map_sigma {ι : Type u_1} {ι' : Type u_2} {α : ι Type u_3} {α' : ι' Type u_4} (f : ι ι') (g : Π (i : ι), α i α' (f i)) (s : set ι') (t : Π (i : ι'), set (α' i)) :
sigma.map f g ⁻¹' s.sigma t = (f ⁻¹' s).sigma (λ (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) :
@[simp]
theorem set.mk_preimage_sigma_eq_empty {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} (hi : i s) :
theorem set.mk_preimage_sigma_eq_if {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} [decidable_pred (λ (_x : ι), _x s)] :
sigma.mk i ⁻¹' s.sigma t = ite (i s) (t i)
theorem set.mk_preimage_sigma_fn_eq_if {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} {β : Type u_2} [decidable_pred (λ (_x : ι), _x s)] (g : β α i) :
(λ (b : β), i, g b⟩) ⁻¹' s.sigma t = ite (i s) (g ⁻¹' t i)
theorem set.sigma_univ_range_eq {ι : Type u_1} {α : ι Type u_3} {β : ι Type u_4} {f : Π (i : ι), α i β i} :
set.univ.sigma (λ (i : ι), set.range (f i)) = set.range (λ (x : Σ (i : ι), α i), x.fst, f x.fst x.snd⟩)
@[protected]
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)} :
theorem set.nonempty.sigma_snd {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} :
(s.sigma t).nonempty ( (i : ι) (H : i s), (t i).nonempty)
theorem set.sigma_nonempty_iff {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} :
(s.sigma t).nonempty (i : ι) (H : i s), (t i).nonempty
theorem set.sigma_eq_empty_iff {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} :
s.sigma t = (i : ι), i s t i =
theorem set.image_sigma_mk_subset_sigma_left {ι : Type u_1} {α : ι Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {a : Π (i : ι), α i} (ha : (i : ι), a i t i) :
(λ (i : ι), i, a i⟩) '' s s.sigma t
theorem set.image_sigma_mk_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)) :
theorem set.fst_image_sigma_subset {ι : Type u_1} {α : ι Type u_3} (s : set ι) (t : Π (i : ι), set (α i)) :
theorem set.fst_image_sigma {ι : Type u_1} {α : ι Type u_3} {t : Π (i : ι), set (α i)} (s : set ι) (ht : (i : ι), (t i).nonempty) :
theorem set.sigma_diff_sigma {ι : Type u_1} {α : ι Type u_3} {s₁ s₂ : set ι} {t₁ t₂ : Π (i : ι), set (α i)} :
s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) (s₁ \ s₂).sigma t₁