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.iUnion_eq_sigma_of_disjoint: 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 #
Notation for Set.sInter Intersection of a set of sets.
Equations
- Set.«term⋂₀_» = Lean.ParserDescr.node `Set.term⋂₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))
Instances For
Notation for Set.sUnion. Union of a set of sets.
Equations
- Set.«term⋃₀_» = Lean.ParserDescr.node `Set.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for Set.iUnion. Indexed union of a family of sets
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for Set.iInter. Indexed intersection of a family of sets
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
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.instOrderTopSetInstLESet = OrderTop.mk (_ : ∀ (a : Set α), a ⊆ Set.univ)
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₁ (pq.mpr x) = 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₁ (pq.mpr x) = f₂ x)
:
Set.iInter f₁ = Set.iInter f₂
theorem
Set.nonempty_of_nonempty_iUnion
{α : Type u_1}
{ι : Sort u_4}
{s : ι → Set α}
(h_Union : Set.Nonempty (⋃ (i : ι), s i))
:
Nonempty ι
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_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.directed_on_iUnion
{α : Type u_1}
{ι : Sort u_4}
{r : α → α → Prop}
{f : ι → Set α}
(hd : Directed (fun x x_1 => x ⊆ x_1) f)
(h : ∀ (x : ι), DirectedOn r (f x))
:
DirectedOn r (⋃ (x : ι), f x)
theorem
Set.iUnion_inter_of_antitone
{ι : Type u_11}
{α : Type u_12}
[Preorder ι]
[IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)]
{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 x x_1 => x ≤ x_1)]
{s : ι → Set α}
{t : ι → Set α}
(hs : Monotone s)
(ht : Monotone t)
:
theorem
Set.image_projection_prod
{ι : Type u_11}
{α : ι → Type u_12}
{v : (i : ι) → Set (α i)}
(hv : Set.Nonempty (Set.pi Set.univ v))
(i : ι)
:
Unions and intersections indexed by Prop #
@[simp]
theorem
Set.nonempty_iUnion
{α : Type u_1}
{ι : Sort u_4}
{s : ι → Set α}
:
Set.Nonempty (⋃ (i : ι), s i) ↔ ∃ i, Set.Nonempty (s i)
theorem
Set.nonempty_biUnion
{α : Type u_1}
{β : Type u_2}
{t : Set α}
{s : α → Set β}
:
Set.Nonempty (⋃ (i : α) (_ : i ∈ t), s i) ↔ ∃ i, i ∈ t ∧ Set.Nonempty (s i)
theorem
Set.iUnion_nonempty_index
{α : Type u_1}
{β : Type u_2}
(s : Set α)
(t : Set.Nonempty s → Set β)
:
⋃ (h : Set.Nonempty s), t h = ⋃ (x : α) (h : x ∈ s), t (_ : ∃ x, x ∈ s)
Bounded unions and intersections #
theorem
Set.subset_biUnion_of_mem
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{u : α → Set β}
{x : α}
(xs : x ∈ s)
:
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)
:
A specialization of iInter₂_subset.
@[simp]
⋃₀ and 𝒫 form a Galois connection.
@[simp]
theorem
Set.nonempty_sUnion
{α : Type u_1}
{S : Set (Set α)}
:
Set.Nonempty (⋃₀ S) ↔ ∃ s, s ∈ S ∧ Set.Nonempty s
@[simp]
theorem
Set.nonempty_iInter
{α : Type u_1}
{ι : Sort u_4}
{f : ι → Set α}
:
Set.Nonempty (⋂ (i : ι), f i) ↔ ∃ x, ∀ (i : ι), x ∈ f i
theorem
Set.nonempty_iInter₂
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_7}
{s : (i : ι) → κ i → Set α}
:
Set.Nonempty (⋂ (i : ι) (j : κ i), s i j) ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j
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))
:
mapsTo #
theorem
Set.mapsTo_sUnion
{α : Type u_1}
{β : Type u_2}
{S : Set (Set α)}
{t : Set β}
{f : α → β}
(H : ∀ (s : Set α), s ∈ S → Set.MapsTo f s t)
:
Set.MapsTo f (⋃₀ S) t
theorem
Set.mapsTo_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → Set α}
{t : Set β}
{f : α → β}
(H : ∀ (i : ι), Set.MapsTo f (s i) t)
:
Set.MapsTo f (⋃ (i : ι), 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 : α → β}
(H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t)
:
Set.MapsTo f (⋃ (i : ι) (j : κ i), 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)
theorem
Set.mapsTo_sInter
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{T : Set (Set β)}
{f : α → β}
(H : ∀ (t : Set β), t ∈ T → Set.MapsTo f s t)
:
Set.MapsTo f s (⋂₀ T)
theorem
Set.mapsTo_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : Set α}
{t : ι → Set β}
{f : α → β}
(H : ∀ (i : ι), Set.MapsTo f s (t i))
:
Set.MapsTo f s (⋂ (i : ι), 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 : α → β}
(H : ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j))
:
Set.MapsTo f s (⋂ (i : ι) (j : κ i), 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 (Set.restrictPreimage (U i) 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 (Set.restrictPreimage (U i) 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 (Set.restrictPreimage (U i) 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 : Set β), 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.univ_subtype
{α : Type u_1}
{p : α → Prop}
:
Set.univ = ⋃ (x : α) (h : p x), {{ val := x, property := h }}
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_iUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
Set.image2 f s t = ⋃ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), {f i j}
The Set.image2 version of Set.image_eq_iUnion
theorem
Set.univ_pi_eq_iInter
{α : Type u_1}
{π : α → Type u_11}
(t : (i : α) → Set (π i))
:
Set.pi Set.univ t = ⋂ (i : α), Function.eval i ⁻¹' t i
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.nonempty_iInter_Iic_iff
{α : Type u_1}
{ι : Sort u_4}
[Preorder α]
{f : ι → α}
:
Set.Nonempty (⋂ (i : ι), Set.Iic (f i)) ↔ BddBelow (Set.range f)
theorem
Set.nonempty_iInter_Ici_iff
{α : Type u_1}
{ι : Sort u_4}
[Preorder α]
{f : ι → α}
:
Set.Nonempty (⋂ (i : ι), Set.Ici (f i)) ↔ BddAbove (Set.range f)
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 = { val := ↑x.snd, property := (_ : ↑x.snd ∈ ⋃ (i : α), t i) }
Instances For
noncomputable def
Set.unionEqSigmaOfDisjoint
{α : Type u_1}
{β : Type u_2}
{t : α → Set β}
(h : ∀ (i j : α), 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) (_ : Function.Bijective (Set.sigmaToiUnion t))).symm
Instances For
theorem
iSup_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice β]
(s : ι → Set α)
(f : α → β)
:
theorem
iInf_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice β]
(s : ι → Set α)
(f : α → β)
: