The set lattice and (pre)images of functions #
This file contains lemmas on the interaction between the indexed union/intersection of sets
and the image and preimage operations: Set.image, Set.preimage, Set.image2, Set.kernImage.
It also covers Set.MapsTo, Set.InjOn, Set.SurjOn, Set.BijOn.
In order to accommodate Set.image2, the file includes results on union/intersection in products.
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
theorem
Set.image_preimage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
GaloisConnection (image f) (preimage f)
theorem
Set.preimage_kernImage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
:
GaloisConnection (preimage f) (kernImage f)
Bounded unions and intersections #
Lemmas about Set.MapsTo #
@[simp]
@[simp]
restrictPreimage #
theorem
Set.injective_iff_injective_of_iUnion_eq_univ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_5}
{f : α → β}
{U : ι → Set β}
(hU : iUnion U = 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_5}
{f : α → β}
{U : ι → Set β}
(hU : iUnion U = 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_5}
{f : α → β}
{U : ι → Set β}
(hU : iUnion U = univ)
:
Function.Bijective f ↔ ∀ (i : ι), Function.Bijective ((U i).restrictPreimage f)
InjOn #
theorem
Set.image_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_5}
{f : α → β}
(hf : Function.Bijective f)
(s : ι → Set α)
:
theorem
Set.image_iInter₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_5}
{κ : ι → Sort u_8}
{f : α → β}
(hf : Function.Bijective f)
(s : (i : ι) → κ i → Set α)
:
SurjOn #
BijOn #
image, preimage #
theorem
Set.image_eq_iUnion
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
f '' s = ⋃ i ∈ s, {f i}
@[simp]
theorem
Set.iUnion_iUnion_eq'
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_5}
{f : ι → α}
{g : α → Set β}
:
⋃ (x : α), ⋃ (y : ι), ⋃ (_ : f y = x), g x = ⋃ (y : ι), g (f y)
@[simp]
theorem
Set.iInter_iInter_eq'
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_5}
{f : ι → α}
{g : α → Set β}
:
⋂ (x : α), ⋂ (y : ι), ⋂ (_ : f y = x), g x = ⋂ (y : ι), g (f y)
theorem
Set.iUnion₂_inter_iUnion₂
{α : Type u_1}
{ι₁ : Sort u_9}
{κ₁ : Sort u_10}
{ι₂ : ι₁ → Sort u_11}
{k₂ : κ₁ → Sort u_12}
(f : (i₁ : ι₁) → ι₂ i₁ → Set α)
(g : (j₁ : κ₁) → k₂ j₁ → Set α)
:
(⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), f i₁ i₂) ∩ ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), g j₁ j₂ = ⋃ (i₁ : ι₁), ⋃ (i₂ : ι₂ i₁), ⋃ (j₁ : κ₁), ⋃ (j₂ : k₂ j₁), f i₁ i₂ ∩ g j₁ j₂
theorem
Set.iInter₂_union_iInter₂
{α : Type u_1}
{ι₁ : Sort u_9}
{κ₁ : Sort u_10}
{ι₂ : ι₁ → Sort u_11}
{k₂ : κ₁ → Sort u_12}
(f : (i₁ : ι₁) → ι₂ i₁ → Set α)
(g : (j₁ : κ₁) → k₂ j₁ → Set α)
:
(⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), f i₁ i₂) ∪ ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), g j₁ j₂ = ⋂ (i₁ : ι₁), ⋂ (i₂ : ι₂ i₁), ⋂ (j₁ : κ₁), ⋂ (j₂ : k₂ j₁), f i₁ i₂ ∪ g j₁ j₂
theorem
Set.biUnion_inter_of_pairwise_disjoint
{α : Type u_1}
{ι : Type u_9}
{f : ι → Set α}
(h : Pairwise (Function.onFun Disjoint f))
(s t : Set ι)
:
⋃ i ∈ s ∩ t, f i = (⋃ i ∈ s, f i) ∩ ⋃ i ∈ t, f i
theorem
Set.biUnion_iInter_of_pairwise_disjoint
{α : Type u_1}
{ι : Type u_9}
{κ : Type u_10}
[hκ : Nonempty κ]
{f : ι → Set α}
(h : Pairwise (Function.onFun Disjoint f))
(s : κ → Set ι)
:
⋃ i ∈ ⋂ (j : κ), s j, f i = ⋂ (j : κ), ⋃ i ∈ s j, f i
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Set.biUnion_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(s : Set β)
(t : Set γ)
(f : β × γ → Set α)
:
⋃ x ∈ s ×ˢ t, f x = ⋃ i ∈ s, ⋃ j ∈ t, f (i, j)
Analogue of biSup_prod for sets.
theorem
Set.image2_eq_iUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
The Set.image2 version of Set.image_eq_iUnion