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.

source
@[simp]
theorem set.range_sigma_mk {ι : Type u_1} {α : ι → Type u_3} (i : ι) :
set.range (sigma.mk i) = sigma.fst ⁻¹' {i}
source
theorem set.preimage_image_sigma_mk_of_ne {ι : Type u_1} {α : ι → Type u_3} {i j : ι} (h : i ≠ j) (s : set (α j)) :
sigma.mk i ⁻¹' (sigma.mk j '' s) = ∅
source
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)
source
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)
source
@[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
source
@[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
source
@[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
source
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
source
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₂
source
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
source
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⟩
source
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⟩
source
@[simp]
theorem set.sigma_empty {ι : Type u_1} {α : ι → Type u_3} {s : set ι} :
s.sigma (λ (i : ι), ∅) = ∅
source
@[simp]
theorem set.empty_sigma {ι : Type u_1} {α : ι → Type u_3} {t : Π (i : ι), set (α i)} :
∅.sigma t = ∅
source
theorem set.univ_sigma_univ {ι : Type u_1} {α : ι → Type u_3} {i : ι} :
set.univ.sigma (λ (_x : ι), set.univ) = set.univ
source
@[simp]
theorem set.sigma_univ {ι : Type u_1} {α : ι → Type u_3} {s : set ι} :
s.sigma (λ (_x : ι), set.univ) = sigma.fst ⁻¹' s
source
@[simp]
theorem set.singleton_sigma {ι : Type u_1} {α : ι → Type u_3} {t : Π (i : ι), set (α i)} {i : ι} :
{i}.sigma t = sigma.mk i '' t i
source
@[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
source
theorem set.singleton_sigma_singleton {ι : Type u_1} {α : ι → Type u_3} {i : ι} {a : Π (i : ι), α i} :
{i}.sigma (λ (i : ι), {a i}) = {⟨i, a i⟩}
source
@[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
source
@[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₂
source
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)
source
theorem set.insert_sigma {ι : Type u_1} {α : ι → Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} :
(has_insert.insert i s).sigma t = sigma.mk i '' t i ∪ s.sigma t
source
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
source
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
source
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
source
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
source
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))
source
@[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
source
@[simp]
theorem set.mk_preimage_sigma_eq_empty {ι : Type u_1} {α : ι → Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} (hi : i ∉ s) :
sigma.mk i ⁻¹' s.sigma t = ∅
source
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) ∅
source
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) ∅
source
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⟩)
source
@[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
source
theorem set.nonempty.sigma_fst {ι : Type u_1} {α : ι → Type u_3} {s : set ι} {t : Π (i : ι), set (α i)} :
(s.sigma t).nonempty → s.nonempty
source
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)
source
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
source
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 = ∅
source
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
source
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
source
theorem set.sigma_subset_preimage_fst {ι : Type u_1} {α : ι → Type u_3} (s : set ι) (t : Π (i : ι), set (α i)) :
s.sigma t ⊆ sigma.fst ⁻¹' s
source
theorem set.fst_image_sigma_subset {ι : Type u_1} {α : ι → Type u_3} (s : set ι) (t : Π (i : ι), set (α i)) :
sigma.fst '' s.sigma t ⊆ s
source
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
source
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₁