The set lattice #
This file is a collection of results on the complete atomic boolean algebra structure of Set α.
Notation for the complete lattice operations can be found in Mathlib.Order.SetNotation.
Main declarations #
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.instBooleanAlgebra.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 #
Union and intersection over an indexed family of sets #
theorem
Set.subset_iUnion_of_subset
{α : Type u_1}
{ι : Sort u_5}
{s : Set α}
{t : ι → Set α}
(i : ι)
(h : s ⊆ 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_5}
{s : ι → Set α}
{t : Set α}
(i : ι)
(h : 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_5}
{κ : ι → Sort u_8}
{s : Set α}
{t : (i : ι) → κ i → Set α}
(i : ι)
(j : κ i)
(h : s ⊆ 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_5}
{κ : ι → Sort u_8}
{s : (i : ι) → κ i → Set α}
{t : Set α}
(i : ι)
(j : κ i)
(h : 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_congr_of_surjective
{α : Type u_1}
{ι : Sort u_5}
{ι₂ : Sort u_7}
{f : ι → Set α}
{g : ι₂ → Set α}
(h : ι → ι₂)
(h1 : Function.Surjective h)
(h2 : ∀ (x : ι), g (h x) = f x)
:
theorem
Set.iInter_congr_of_surjective
{α : Type u_1}
{ι : Sort u_5}
{ι₂ : Sort u_7}
{f : ι → Set α}
{g : ι₂ → Set α}
(h : ι → ι₂)
(h1 : Function.Surjective h)
(h2 : ∀ (x : ι), g (h x) = f x)
:
theorem
Set.iUnion_inter_of_antitone
{ι : Type u_12}
{α : Type u_13}
[Preorder ι]
[IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 ≤ x2)]
{s t : ι → Set α}
(hs : Antitone s)
(ht : Antitone t)
:
theorem
Set.iInter_union_of_monotone
{ι : Type u_12}
{α : Type u_13}
[Preorder ι]
[IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 ≤ x2)]
{s 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)
:
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)
:
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)
:
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.
⋃₀ and 𝒫 form a Galois connection.
@[deprecated Set.sUnionPowersetGI (since := "2024-12-07")]
Alias of Set.sUnionPowersetGI.
⋃₀ and 𝒫 form a Galois insertion.
Equations
Instances For
Alias of Set.sUnion_subset_sUnion.
Alias of Set.sInter_subset_sInter.
theorem
Set.iUnion_range_eq_sUnion
{α : Type u_12}
{β : Type u_13}
(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_5}
(C : ι → Set α)
{f : (x : ι) → β → ↑(C x)}
(hf : ∀ (x : ι), Function.Surjective (f x))
:
theorem
Set.biUnion_lt_eq_iUnion
{α : Type u_1}
{β : Type u_2}
[LT α]
[NoMaxOrder α]
{s : α → Set β}
:
theorem
Set.biInter_lt_eq_iInter
{α : Type u_1}
{β : Type u_2}
[LT α]
[NoMaxOrder α]
{s : α → Set β}
:
theorem
Set.biUnion_gt_eq_iUnion
{α : Type u_1}
{β : Type u_2}
[LT α]
[NoMinOrder α]
{s : α → Set β}
:
theorem
Set.biInter_gt_eq_iInf
{α : Type u_1}
{β : Type u_2}
[LT α]
[NoMinOrder α]
{s : α → Set β}
:
theorem
Set.directedOn_iUnion
{α : Type u_1}
{ι : Sort u_5}
{r : α → α → Prop}
{f : ι → Set α}
(hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) f)
(h : ∀ (x : ι), DirectedOn r (f x))
:
DirectedOn r (⋃ (x : ι), f x)
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_5}
{ι₂ : Sort u_7}
{f : ι → ι₂}
(hf : Surjective f)
(g : ι₂ → Set α)
:
theorem
Function.Surjective.iInter_comp
{α : Type u_1}
{ι : Sort u_5}
{ι₂ : Sort u_7}
{f : ι → ι₂}
(hf : Surjective f)
(g : ι₂ → Set α)
:
Disjoint sets #
Intervals #
theorem
Set.Ici_iSup₂
{α : Type u_1}
{ι : Sort u_5}
{κ : ι → Sort u_8}
[CompleteLattice α]
(f : (i : ι) → κ i → α)
:
theorem
Set.Iic_iInf₂
{α : Type u_1}
{ι : Sort u_5}
{κ : ι → Sort u_8}
[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
theorem
Set.sigmaToiUnion_injective
{α : Type u_1}
{β : Type u_2}
(t : α → Set β)
(h : Pairwise (Function.onFun Disjoint t))
:
theorem
Set.sigmaToiUnion_bijective
{α : Type u_1}
{β : Type u_2}
(t : α → Set β)
(h : Pairwise (Function.onFun Disjoint t))
:
noncomputable def
Set.sigmaEquiv
{α : Type u_1}
{β : Type u_2}
(s : α → Set β)
(hs : ∀ (b : β), ∃! i : α, b ∈ 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 (Function.onFun Disjoint t))
:
Equivalence between a disjoint union and a dependent sum.
Equations
Instances For
theorem
iSup_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_5}
[CompleteLattice β]
(s : ι → Set α)
(f : α → β)
:
theorem
iInf_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_5}
[CompleteLattice β]
(s : ι → Set α)
(f : α → β)
:
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 : α → β)
: