The set lattice #
This file provides usual set notation for unions and intersections, a CompleteLattice instance
for Set α, and some more set constructions.
Main declarations #
Set.iUnion: indexed union. Union of an indexed family of sets.Set.iInter: indexed intersection. Intersection of an indexed family of sets.Set.sInter: set intersection. Intersection of sets belonging to a set of sets.Set.sUnion: set union. Union of sets belonging to a set of sets.Set.sInter_eq_biInter,Set.sUnion_eq_biInter: Shows that⋂₀ s = ⋂ x ∈ s, xand⋃₀ s = ⋃ x ∈ s, x.Set.completeAtomicBooleanAlgebra:Set αis aCompleteAtomicBooleanAlgebrawith≤ = ⊆,< = ⊂,⊓ = ∩,⊔ = ∪,⨅ = ⋂,⨆ = ⋃and\as the set difference. SeeSet.BooleanAlgebra.Set.kernImage: For a functionf : α → β,s.kernImage fis the set ofysuch thatf ⁻¹ y ⊆ s.Set.seq: Union of the image of a set under a sequence of functions.seq s tis the union off '' tover allf ∈ s, wheret : Set αands : Set (α → β).Set.unionEqSigmaOfDisjoint: Equivalence between⋃ i, t iandΣ i, t i, wheretis an indexed family of disjoint sets.
Naming convention #
In lemma names,
⋃ i, s iis callediUnion⋂ i, s iis callediInter⋃ i j, s i jis callediUnion₂. This is aniUnioninside aniUnion.⋂ i j, s i jis callediInter₂. This is aniInterinside aniInter.⋃ i ∈ s, t iis calledbiUnionfor "boundediUnion". This is the special case ofiUnion₂wherej : i ∈ s.⋂ i ∈ s, t iis calledbiInterfor "boundediInter". This is the special case ofiInter₂wherej : i ∈ s.
Notation #
⋃:Set.iUnion⋂:Set.iInter⋃₀:Set.sUnion⋂₀:Set.sInter
Complete lattice and complete Boolean algebra instances #
Equations
- Set.completeAtomicBooleanAlgebra = CompleteAtomicBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
Set.image_preimage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
GaloisConnection (Set.image f) (Set.preimage f)
theorem
Set.kernImage_eq_compl
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set α}
:
Set.kernImage f s = (f '' sᶜ)ᶜ
theorem
Set.kernImage_compl
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set α}
:
Set.kernImage f sᶜ = (f '' s)ᶜ
theorem
Set.kernImage_empty
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
Set.kernImage f ∅ = (Set.range f)ᶜ
theorem
Set.compl_range_subset_kernImage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set α}
:
(Set.range f)ᶜ ⊆ Set.kernImage f s
theorem
Set.kernImage_union_preimage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set α}
{t : Set β}
:
Set.kernImage f (s ∪ f ⁻¹' t) = Set.kernImage f s ∪ t
theorem
Set.kernImage_preimage_union
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set α}
{t : Set β}
:
Set.kernImage f (f ⁻¹' t ∪ s) = t ∪ Set.kernImage f s
Union and intersection over an indexed family of sets #
Equations
- Set.instOrderTop = OrderTop.mk ⋯
theorem
Set.iUnion_congr_Prop
{α : Type u_1}
{p : Prop}
{q : Prop}
{f₁ : p → Set α}
{f₂ : q → Set α}
(pq : p ↔ q)
(f : ∀ (x : q), f₁ ⋯ = f₂ x)
:
Set.iUnion f₁ = Set.iUnion f₂
theorem
Set.iInter_congr_Prop
{α : Type u_1}
{p : Prop}
{q : Prop}
{f₁ : p → Set α}
{f₂ : q → Set α}
(pq : p ↔ q)
(f : ∀ (x : q), f₁ ⋯ = f₂ x)
:
Set.iInter f₁ = Set.iInter f₂
theorem
Set.subset_iUnion_of_subset
{α : Type u_1}
{ι : Sort u_4}
{s : Set α}
{t : ι → Set α}
(i : ι)
(h : s ⊆ t i)
:
s ⊆ ⋃ (i : ι), t i
This rather trivial consequence of subset_iUnionis convenient with apply, and has i
explicit for this purpose.
theorem
Set.iInter_subset_of_subset
{α : Type u_1}
{ι : Sort u_4}
{s : ι → Set α}
{t : Set α}
(i : ι)
(h : s i ⊆ t)
:
⋂ (i : ι), s i ⊆ t
This rather trivial consequence of iInter_subsetis convenient with apply, and has i
explicit for this purpose.
theorem
Set.subset_iUnion₂_of_subset
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : Set α}
{t : (i : ι) → κ i → Set α}
(i : ι)
(j : κ i)
(h : s ⊆ t i j)
:
s ⊆ ⋃ (i : ι), ⋃ (j : κ i), t i j
This rather trivial consequence of subset_iUnion₂ is convenient with apply, and has i and
j explicit for this purpose.
theorem
Set.iInter₂_subset_of_subset
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : (i : ι) → κ i → Set α}
{t : Set α}
(i : ι)
(j : κ i)
(h : s i j ⊆ t)
:
⋂ (i : ι), ⋂ (j : κ i), s i j ⊆ t
This rather trivial consequence of iInter₂_subset is convenient with apply, and has i and
j explicit for this purpose.
theorem
Set.iUnion_mono''
{α : Type u_1}
{ι : Sort u_4}
{s : ι → Set α}
{t : ι → Set α}
(h : ∀ (i : ι), s i ⊆ t i)
:
Set.iUnion s ⊆ Set.iUnion t
theorem
Set.iInter_mono''
{α : Type u_1}
{ι : Sort u_4}
{s : ι → Set α}
{t : ι → Set α}
(h : ∀ (i : ι), s i ⊆ t i)
:
Set.iInter s ⊆ Set.iInter t
theorem
Set.iUnion₂_mono'
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
{κ : ι → Sort u_7}
{κ' : ι' → Sort u_10}
{s : (i : ι) → κ i → Set α}
{t : (i' : ι') → κ' i' → Set α}
(h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), s i j ⊆ t i' j')
:
⋃ (i : ι), ⋃ (j : κ i), s i j ⊆ ⋃ (i' : ι'), ⋃ (j' : κ' i'), t i' j'
theorem
Set.iInter₂_mono'
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
{κ : ι → Sort u_7}
{κ' : ι' → Sort u_10}
{s : (i : ι) → κ i → Set α}
{t : (i' : ι') → κ' i' → Set α}
(h : ∀ (i' : ι') (j' : κ' i'), ∃ (i : ι) (j : κ i), s i j ⊆ t i' j')
:
⋂ (i : ι), ⋂ (j : κ i), s i j ⊆ ⋂ (i' : ι'), ⋂ (j' : κ' i'), t i' j'
theorem
Set.iUnion_congr_of_surjective
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_6}
{f : ι → Set α}
{g : ι₂ → Set α}
(h : ι → ι₂)
(h1 : Function.Surjective h)
(h2 : ∀ (x : ι), g (h x) = f x)
:
⋃ (x : ι), f x = ⋃ (y : ι₂), g y
theorem
Set.iInter_congr_of_surjective
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_6}
{f : ι → Set α}
{g : ι₂ → Set α}
(h : ι → ι₂)
(h1 : Function.Surjective h)
(h2 : ∀ (x : ι), g (h x) = f x)
:
⋂ (x : ι), f x = ⋂ (y : ι₂), g y
theorem
Set.iUnion_inter_of_antitone
{ι : Type u_11}
{α : Type u_12}
[Preorder ι]
[IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 ≤ x2)]
{s : ι → Set α}
{t : ι → Set α}
(hs : Antitone s)
(ht : Antitone t)
:
theorem
Set.iInter_union_of_monotone
{ι : Type u_11}
{α : Type u_12}
[Preorder ι]
[IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 ≤ x2)]
{s : ι → Set α}
{t : ι → Set α}
(hs : Monotone s)
(ht : Monotone t)
:
Unions and intersections indexed by Prop #
Bounded unions and intersections #
theorem
Set.mem_biUnion
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : α → Set β}
{x : α}
{y : β}
(xs : x ∈ s)
(ytx : y ∈ t x)
:
y ∈ ⋃ x ∈ s, t x
A specialization of mem_iUnion₂.
theorem
Set.mem_biInter
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : α → Set β}
{y : β}
(h : ∀ x ∈ s, y ∈ t x)
:
y ∈ ⋂ x ∈ s, t x
A specialization of mem_iInter₂.
theorem
Set.subset_biUnion_of_mem
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{u : α → Set β}
{x : α}
(xs : x ∈ s)
:
u x ⊆ ⋃ x ∈ s, u x
A specialization of subset_iUnion₂.
theorem
Set.biInter_subset_of_mem
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : α → Set β}
{x : α}
(xs : x ∈ s)
:
⋂ x ∈ s, t x ⊆ t x
A specialization of iInter₂_subset.
@[simp]
⋃₀ and 𝒫 form a Galois connection.
⋃₀ and 𝒫 form a Galois insertion.
Equations
- Set.sUnion_powerset_gi = gi_sSup_Iic
Instances For
theorem
Set.iUnion_range_eq_sUnion
{α : Type u_11}
{β : Type u_12}
(C : Set (Set α))
{f : (s : ↑C) → β → ↑↑s}
(hf : ∀ (s : ↑C), Function.Surjective (f s))
:
theorem
Set.iUnion_range_eq_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
(C : ι → Set α)
{f : (x : ι) → β → ↑(C x)}
(hf : ∀ (x : ι), Function.Surjective (f x))
:
Lemmas about Set.MapsTo #
Porting note: some lemmas in this section were upgraded from implications to iffs.
@[simp]
theorem
Set.mapsTo_sUnion
{α : Type u_1}
{β : Type u_2}
{S : Set (Set α)}
{t : Set β}
{f : α → β}
:
Set.MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, Set.MapsTo f s t
@[simp]
theorem
Set.mapsTo_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → Set α}
{t : Set β}
{f : α → β}
:
Set.MapsTo f (⋃ (i : ι), s i) t ↔ ∀ (i : ι), Set.MapsTo f (s i) t
theorem
Set.mapsTo_iUnion₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : (i : ι) → κ i → Set α}
{t : Set β}
{f : α → β}
:
Set.MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) t ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t
theorem
Set.mapsTo_iUnion_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → Set α}
{t : ι → Set β}
{f : α → β}
(H : ∀ (i : ι), Set.MapsTo f (s i) (t i))
:
Set.MapsTo f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem
Set.mapsTo_iUnion₂_iUnion₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : (i : ι) → κ i → Set α}
{t : (i : ι) → κ i → Set β}
{f : α → β}
(H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j))
:
Set.MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)
@[simp]
theorem
Set.mapsTo_sInter
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{T : Set (Set β)}
{f : α → β}
:
Set.MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, Set.MapsTo f s t
@[simp]
theorem
Set.mapsTo_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : Set α}
{t : ι → Set β}
{f : α → β}
:
Set.MapsTo f s (⋂ (i : ι), t i) ↔ ∀ (i : ι), Set.MapsTo f s (t i)
theorem
Set.mapsTo_iInter₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : Set α}
{t : (i : ι) → κ i → Set β}
{f : α → β}
:
Set.MapsTo f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)
theorem
Set.mapsTo_iInter_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → Set α}
{t : ι → Set β}
{f : α → β}
(H : ∀ (i : ι), Set.MapsTo f (s i) (t i))
:
Set.MapsTo f (⋂ (i : ι), s i) (⋂ (i : ι), t i)
theorem
Set.mapsTo_iInter₂_iInter₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : (i : ι) → κ i → Set α}
{t : (i : ι) → κ i → Set β}
{f : α → β}
(H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j))
:
Set.MapsTo f (⋂ (i : ι), ⋂ (j : κ i), s i j) (⋂ (i : ι), ⋂ (j : κ i), t i j)
restrictPreimage #
theorem
Set.injective_iff_injective_of_iUnion_eq_univ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{U : ι → Set β}
(hU : Set.iUnion U = Set.univ)
:
Function.Injective f ↔ ∀ (i : ι), Function.Injective ((U i).restrictPreimage f)
theorem
Set.surjective_iff_surjective_of_iUnion_eq_univ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{U : ι → Set β}
(hU : Set.iUnion U = Set.univ)
:
Function.Surjective f ↔ ∀ (i : ι), Function.Surjective ((U i).restrictPreimage f)
theorem
Set.bijective_iff_bijective_of_iUnion_eq_univ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{U : ι → Set β}
(hU : Set.iUnion U = Set.univ)
:
Function.Bijective f ↔ ∀ (i : ι), Function.Bijective ((U i).restrictPreimage f)
InjOn #
theorem
Set.image_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
(hf : Function.Bijective f)
(s : ι → Set α)
:
SurjOn #
theorem
Set.surjOn_sUnion
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{T : Set (Set β)}
{f : α → β}
(H : ∀ t ∈ T, Set.SurjOn f s t)
:
Set.SurjOn f s (⋃₀ T)
theorem
Set.surjOn_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : Set α}
{t : ι → Set β}
{f : α → β}
(H : ∀ (i : ι), Set.SurjOn f s (t i))
:
Set.SurjOn f s (⋃ (i : ι), t i)
theorem
Set.surjOn_iUnion_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → Set α}
{t : ι → Set β}
{f : α → β}
(H : ∀ (i : ι), Set.SurjOn f (s i) (t i))
:
Set.SurjOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem
Set.surjOn_iUnion₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : Set α}
{t : (i : ι) → κ i → Set β}
{f : α → β}
(H : ∀ (i : ι) (j : κ i), Set.SurjOn f s (t i j))
:
Set.SurjOn f s (⋃ (i : ι), ⋃ (j : κ i), t i j)
theorem
Set.surjOn_iUnion₂_iUnion₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : (i : ι) → κ i → Set α}
{t : (i : ι) → κ i → Set β}
{f : α → β}
(H : ∀ (i : ι) (j : κ i), Set.SurjOn f (s i j) (t i j))
:
Set.SurjOn f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)
theorem
Set.surjOn_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[Nonempty ι]
{s : ι → Set α}
{t : Set β}
{f : α → β}
(H : ∀ (i : ι), Set.SurjOn f (s i) t)
(Hinj : Set.InjOn f (⋃ (i : ι), s i))
:
Set.SurjOn f (⋂ (i : ι), s i) t
theorem
Set.surjOn_iInter_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[Nonempty ι]
{s : ι → Set α}
{t : ι → Set β}
{f : α → β}
(H : ∀ (i : ι), Set.SurjOn f (s i) (t i))
(Hinj : Set.InjOn f (⋃ (i : ι), s i))
:
Set.SurjOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)
BijOn #
image, preimage #
theorem
Set.image2_eq_iUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
Set.image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
The Set.image2 version of Set.image_eq_iUnion
theorem
Set.iUnion_image_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
{s : Set α}
{t : Set β}
:
⋃ a ∈ s, f a '' t = Set.image2 f s t
theorem
Set.iUnion_image_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
{s : Set α}
{t : Set β}
:
⋃ b ∈ t, (fun (x : α) => f x b) '' s = Set.image2 f s t
theorem
Set.image2_iUnion_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
(f : α → β → γ)
(s : ι → Set α)
(t : Set β)
:
Set.image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), Set.image2 f (s i) t
theorem
Set.image2_iUnion_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
(f : α → β → γ)
(s : Set α)
(t : ι → Set β)
:
Set.image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), Set.image2 f s (t i)
theorem
Set.image2_iUnion₂_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
{κ : ι → Sort u_7}
(f : α → β → γ)
(s : (i : ι) → κ i → Set α)
(t : Set β)
:
Set.image2 f (⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), Set.image2 f (s i j) t
theorem
Set.image2_iUnion₂_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
{κ : ι → Sort u_7}
(f : α → β → γ)
(s : Set α)
(t : (i : ι) → κ i → Set β)
:
Set.image2 f s (⋃ (i : ι), ⋃ (j : κ i), t i j) = ⋃ (i : ι), ⋃ (j : κ i), Set.image2 f s (t i j)
theorem
Set.image2_iInter_subset_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
(f : α → β → γ)
(s : ι → Set α)
(t : Set β)
:
Set.image2 f (⋂ (i : ι), s i) t ⊆ ⋂ (i : ι), Set.image2 f (s i) t
theorem
Set.image2_iInter_subset_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
(f : α → β → γ)
(s : Set α)
(t : ι → Set β)
:
Set.image2 f s (⋂ (i : ι), t i) ⊆ ⋂ (i : ι), Set.image2 f s (t i)
theorem
Set.image2_iInter₂_subset_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
{κ : ι → Sort u_7}
(f : α → β → γ)
(s : (i : ι) → κ i → Set α)
(t : Set β)
:
Set.image2 f (⋂ (i : ι), ⋂ (j : κ i), s i j) t ⊆ ⋂ (i : ι), ⋂ (j : κ i), Set.image2 f (s i j) t
theorem
Set.image2_iInter₂_subset_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Sort u_4}
{κ : ι → Sort u_7}
(f : α → β → γ)
(s : Set α)
(t : (i : ι) → κ i → Set β)
:
Set.image2 f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ⊆ ⋂ (i : ι), ⋂ (j : κ i), Set.image2 f s (t i j)
theorem
Set.image2_eq_seq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
Set.image2 f s t = (f '' s).seq t
theorem
Set.pi_def
{α : Type u_1}
{π : α → Type u_11}
(i : Set α)
(s : (a : α) → Set (π a))
:
i.pi s = ⋂ a ∈ i, Function.eval a ⁻¹' s a
theorem
Set.univ_pi_eq_iInter
{α : Type u_1}
{π : α → Type u_11}
(t : (i : α) → Set (π i))
:
Set.univ.pi t = ⋂ (i : α), Function.eval i ⁻¹' t i
theorem
Set.directedOn_iUnion
{α : Type u_1}
{ι : Sort u_4}
{r : α → α → Prop}
{f : ι → Set α}
(hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) f)
(h : ∀ (x : ι), DirectedOn r (f x))
:
DirectedOn r (⋃ (x : ι), f x)
@[deprecated Set.directedOn_iUnion]
theorem
Set.directed_on_iUnion
{α : Type u_1}
{ι : Sort u_4}
{r : α → α → Prop}
{f : ι → Set α}
(hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) f)
(h : ∀ (x : ι), DirectedOn r (f x))
:
DirectedOn r (⋃ (x : ι), f x)
Alias of Set.directedOn_iUnion.
theorem
Set.directedOn_sUnion
{α : Type u_1}
{r : α → α → Prop}
{S : Set (Set α)}
(hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) S)
(h : ∀ x ∈ S, DirectedOn r x)
:
DirectedOn r (⋃₀ S)
theorem
Function.Surjective.iUnion_comp
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_6}
{f : ι → ι₂}
(hf : Function.Surjective f)
(g : ι₂ → Set α)
:
⋃ (x : ι), g (f x) = ⋃ (y : ι₂), g y
theorem
Function.Surjective.iInter_comp
{α : Type u_1}
{ι : Sort u_4}
{ι₂ : Sort u_6}
{f : ι → ι₂}
(hf : Function.Surjective f)
(g : ι₂ → Set α)
:
⋂ (x : ι), g (f x) = ⋂ (y : ι₂), g y
Disjoint sets #
Intervals #
theorem
Set.Ici_iSup₂
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_7}
[CompleteLattice α]
(f : (i : ι) → κ i → α)
:
theorem
Set.Iic_iInf₂
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_7}
[CompleteLattice α]
(f : (i : ι) → κ i → α)
:
def
Set.sigmaToiUnion
{α : Type u_1}
{β : Type u_2}
(t : α → Set β)
(x : (i : α) × ↑(t i))
:
↑(⋃ (i : α), t i)
If t is an indexed family of sets, then there is a natural map from Σ i, t i to ⋃ i, t i
sending ⟨i, x⟩ to x.
Equations
- Set.sigmaToiUnion t x = ⟨↑x.snd, ⋯⟩
Instances For
noncomputable def
Set.sigmaEquiv
{α : Type u_1}
{β : Type u_2}
(s : α → Set β)
(hs : ∀ (b : β), ∃! i : α, b ∈ s i)
:
(i : α) × ↑(s i) ≃ β
Equivalence from the disjoint union of a family of sets forming a partition of β, to β
itself.
Equations
- Set.sigmaEquiv s hs = { toFun := fun (x : (i : α) × ↑(s i)) => match x with | ⟨fst, b⟩ => ↑b, invFun := fun (b : β) => ⟨Exists.choose ⋯, ⟨b, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
noncomputable def
Set.unionEqSigmaOfDisjoint
{α : Type u_1}
{β : Type u_2}
{t : α → Set β}
(h : Pairwise fun (i j : α) => Disjoint (t i) (t j))
:
↑(⋃ (i : α), t i) ≃ (i : α) × ↑(t i)
Equivalence between a disjoint union and a dependent sum.
Equations
- Set.unionEqSigmaOfDisjoint h = (Equiv.ofBijective (Set.sigmaToiUnion t) ⋯).symm
Instances For
theorem
iSup_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice β]
(s : ι → Set α)
(f : α → β)
:
⨆ a ∈ ⋃ (i : ι), s i, f a = ⨆ (i : ι), ⨆ a ∈ s i, f a
theorem
iInf_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice β]
(s : ι → Set α)
(f : α → β)
:
⨅ a ∈ ⋃ (i : ι), s i, f a = ⨅ (i : ι), ⨅ a ∈ s i, f a
theorem
iSup_sUnion
{α : Type u_1}
{β : Type u_2}
[CompleteLattice β]
(S : Set (Set α))
(f : α → β)
:
theorem
iInf_sUnion
{α : Type u_1}
{β : Type u_2}
[CompleteLattice β]
(S : Set (Set α))
(f : α → β)
: