# Finiteness of unions and intersections #

## Implementation notes #

Each result in this file should come in three forms: a `Fintype` instance, a `Finite` instance and a `Set.Finite` constructor.

## Tags #

finite sets

### Fintype instances #

Every instance here should have a corresponding `Set.Finite` constructor in the next section.

source
instance Set.fintypeiUnion {α : Type u} {ι : Sort w} [DecidableEq α] [Fintype (PLift ι)] (f : ι → Set α) [(i : ι) → Fintype ↑(f i)] :
Fintype ↑(⋃ (i : ι), f i)
Equations

- Set.fintypeiUnion f = Fintype.ofFinset (Finset.univ.biUnion fun (i : PLift ι) => (f i.down).toFinset) ⋯

source
instance Set.fintypesUnion {α : Type u} [DecidableEq α] {s : Set (Set α)} [Fintype ↑s] [H : (t : ↑s) → Fintype ↑↑t] :
Fintype ↑(⋃₀ s)
Equations

- Set.fintypesUnion = ⋯.mpr (Set.fintypeiUnion Subtype.val)

source
theorem Set.toFinset_iUnion {α : Type u} {β : Type v} [Fintype β] [DecidableEq α] (f : β → Set α) [(w : β) → Fintype ↑(f w)] :
(⋃ (x : β), f x).toFinset = Finset.univ.biUnion fun (x : β) => (f x).toFinset
source
def Set.fintypeBiUnion {α : Type u} [DecidableEq α] {ι : Type u_1} (s : Set ι) [Fintype ↑s] (t : ι → Set α) (H : (i : ι) → i ∈ s → Fintype ↑(t i)) :
Fintype ↑(⋃ x ∈ s, t x)

A union of sets with `Fintype` structure over a set with `Fintype` structure has a `Fintype` structure.

Equations

- s.fintypeBiUnion t H = Fintype.ofFinset (s.toFinset.attach.biUnion fun (x : { x : ι // x ∈ s.toFinset }) => (t ↑x).toFinset) ⋯

Instances For

source
instance Set.fintypeBiUnion' {α : Type u} [DecidableEq α] {ι : Type u_1} (s : Set ι) [Fintype ↑s] (t : ι → Set α) [(i : ι) → Fintype ↑(t i)] :
Fintype ↑(⋃ x ∈ s, t x)
Equations

- s.fintypeBiUnion' t = Fintype.ofFinset (s.toFinset.biUnion fun (x : ι) => (t x).toFinset) ⋯

### Finite instances #

There is seemingly some overlap between the following instances and the `Fintype` instances in `Data.Set.Finite`. While every `Fintype` instance gives a `Finite` instance, those instances that depend on `Fintype` or `Decidable` instances need an additional `Finite` instance to be able to generally apply.

Some set instances do not appear here since they are consequences of others, for example `Subtype.Finite` for subsets of a finite type.

source
instance Finite.Set.finite_iUnion {α : Type u} {ι : Sort w} [Finite ι] (f : ι → Set α) [∀ (i : ι), Finite ↑(f i)] :
Finite ↑(⋃ (i : ι), f i)
source
instance Finite.Set.finite_sUnion {α : Type u} {s : Set (Set α)} [Finite ↑s] [H : ∀ (t : ↑s), Finite ↑↑t] :
Finite ↑(⋃₀ s)
source
theorem Finite.Set.finite_biUnion {α : Type u} {ι : Type u_1} (s : Set ι) [Finite ↑s] (t : ι → Set α) (H : ∀ i ∈ s, Finite ↑(t i)) :
Finite ↑(⋃ x ∈ s, t x)
source
instance Finite.Set.finite_biUnion' {α : Type u} {ι : Type u_1} (s : Set ι) [Finite ↑s] (t : ι → Set α) [∀ (i : ι), Finite ↑(t i)] :
Finite ↑(⋃ x ∈ s, t x)
source
instance Finite.Set.finite_biUnion'' {α : Type u} {ι : Type u_1} (p : ι → Prop) [h : Finite ↑{x : ι | p x}] (t : ι → Set α) [∀ (i : ι), Finite ↑(t i)] :
Finite ↑(⋃ (x : ι), ⋃ (_ : p x), t x)

Example: `Finite (⋃ (i < n), f i)` where `f : ℕ → Set α` and `[∀ i, Finite (f i)]` (when given instances from `Order.Interval.Finset.Nat`).

source
instance Finite.Set.finite_iInter {α : Type u} {ι : Sort u_1} [Nonempty ι] (t : ι → Set α) [∀ (i : ι), Finite ↑(t i)] :
Finite ↑(⋂ (i : ι), t i)

### Constructors for `Set.Finite` #

Every constructor here should have a corresponding `Fintype` instance in the previous section (or in the `Fintype` module).

The implementation of these constructors ideally should be no more than `Set.toFinite`, after possibly setting up some `Fintype` and classical `Decidable` instances.

source
theorem Set.finite_iUnion {α : Type u} {ι : Sort w} [Finite ι] {f : ι → Set α} (H : ∀ (i : ι), (f i).Finite) :
(⋃ (i : ι), f i).Finite
source
theorem Set.Finite.biUnion' {α : Type u} {ι : Type u_1} {s : Set ι} (hs : s.Finite) {t : (i : ι) → i ∈ s → Set α} (ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite) :
(⋃ (i : ι), ⋃ (h : i ∈ s), t i h).Finite

Dependent version of `Finite.biUnion`.

source
theorem Set.Finite.biUnion {α : Type u} {ι : Type u_1} {s : Set ι} (hs : s.Finite) {t : ι → Set α} (ht : ∀ i ∈ s, (t i).Finite) :
(⋃ i ∈ s, t i).Finite
source
theorem Set.Finite.sUnion {α : Type u} {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, t.Finite) :
(⋃₀ s).Finite
source
theorem Set.Finite.sInter {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : t.Finite) :
(⋂₀ s).Finite
source
theorem Set.Finite.iUnion {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set ι} (ht : t.Finite) (hs : ∀ i ∈ t, (s i).Finite) (he : ∀ i ∉ t, s i = ∅) :
(⋃ (i : ι), s i).Finite

If sets `s i` are finite for all `i` from a finite set `t` and are empty for `i ∉ t`, then the union `⋃ i, s i` is a finite set.

source
theorem Set.finite_iUnion_iff {α : Type u} {ι : Type u_1} {s : ι → Set α} (hs : Pairwise fun (i j : ι) => Disjoint (s i) (s j)) :
(⋃ (i : ι), s i).Finite ↔ (∀ (i : ι), (s i).Finite) ∧ {i : ι | (s i).Nonempty}.Finite

An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but finitely many are empty.

source
theorem Set.Infinite.iUnion {α : Type u} {ι : Sort u_1} {s : ι → Set α} (i : ι) (hi : (s i).Infinite) :
(⋃ (i : ι), s i).Infinite
source
theorem Set.Infinite.iUnion₂ {α : Type u} {ι : Sort u_1} {κ : ι → Sort u_2} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i) (hij : (s i j).Infinite) :
(⋃ (i : ι), ⋃ (j : κ i), s i j).Infinite
source
@[simp]
theorem Set.finite_iUnion_of_subsingleton {α : Type u} {ι : Sort u_1} [Subsingleton ι] {s : ι → Set α} :
(⋃ (i : ι), s i).Finite ↔ ∀ (i : ι), (s i).Finite
source
theorem Set.PairwiseDisjoint.finite_biUnion_iff {α : Type u} {β : Type v} {f : β → Set α} {s : Set β} (hs : s.PairwiseDisjoint f) :
(⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i : β | i ∈ s ∧ (f i).Nonempty}.Finite

An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but finitely many are empty.

source
theorem Set.Finite.preimage' {α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite) :
(f ⁻¹' s).Finite
source
theorem Set.union_finset_finite_of_range_finite {α : Type u} {β : Type v} (f : α → Finset β) (h : (range f).Finite) :
(⋃ (a : α), ↑(f a)).Finite

A finite union of finsets is finite.

source
theorem Set.Finite.of_finite_fibers {α : Type u} {β : Type v} (f : α → β) {s : Set α} (himage : (f '' s).Finite) (hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite) :
s.Finite

If the image of `s` under `f` is finite, and each fiber of `f` has a finite intersection with `s`, then `s` is itself finite.

It is useful to give `f` explicitly here so this can be used with `apply`.

### Properties #

source
theorem Set.finite_subset_iUnion {α : Type u} {s : Set α} (hs : s.Finite) {ι : Type u_1} {t : ι → Set α} (h : s ⊆ ⋃ (i : ι), t i) :
∃ (I : Set ι), I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
source
theorem Set.eq_finite_iUnion_of_finite_subset_iUnion {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set α} (tfin : t.Finite) (h : t ⊆ ⋃ (i : ι), s i) :
∃ (I : Set ι), I.Finite ∧ ∃ (σ : ↑{i : ι | i ∈ I} → Set α), (∀ (i : ↑{i : ι | i ∈ I}), (σ i).Finite) ∧ (∀ (i : ↑{i : ι | i ∈ I}), σ i ⊆ s ↑i) ∧ t = ⋃ (i : ↑{i : ι | i ∈ I}), σ i

### Infinite sets #

source
theorem Set.infinite_iUnion {α : Type u} {ι : Type u_1} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) :
(⋃ (i : ι), s i).Infinite
source
theorem Set.Infinite.biUnion {α : Type u} {ι : Type u_1} {s : ι → Set α} {a : Set ι} (ha : a.Infinite) (hs : InjOn s a) :
(⋃ i ∈ a, s i).Infinite
source
theorem Set.Infinite.sUnion {α : Type u} {s : Set (Set α)} (hs : s.Infinite) :
(⋃₀ s).Infinite

### Order properties #

source
theorem Set.map_finite_biSup {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [SupBotHomClass F α β] {s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) :
f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)
source
theorem Set.map_finite_biInf {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [InfTopHomClass F α β] {s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) :
f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)
source
theorem Set.map_finite_iSup {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [SupBotHomClass F α β] [Finite ι] (f : F) (g : ι → α) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
source
theorem Set.map_finite_iInf {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [InfTopHomClass F α β] [Finite ι] (f : F) (g : ι → α) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
source
theorem Set.Finite.iSup_biInf_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsDirected ι' fun (x1 x2 : ι') => x1 ≤ x2] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) :
⨆ (j : ι'), ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ (j : ι'), f i j
source
theorem Set.Finite.iSup_biInf_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (Function.swap fun (x1 x2 : ι') => x1 ≤ x2)] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) :
⨆ (j : ι'), ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ (j : ι'), f i j
source
theorem Set.Finite.iInf_biSup_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (Function.swap fun (x1 x2 : ι') => x1 ≤ x2)] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) :
⨅ (j : ι'), ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ (j : ι'), f i j
source
theorem Set.Finite.iInf_biSup_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsDirected ι' fun (x1 x2 : ι') => x1 ≤ x2] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) :
⨅ (j : ι'), ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ (j : ι'), f i j
source
theorem Set.iSup_iInf_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' fun (x1 x2 : ι') => x1 ≤ x2] [Order.Frame α] {f : ι → ι' → α} (hf : ∀ (i : ι), Monotone (f i)) :
⨆ (j : ι'), ⨅ (i : ι), f i j = ⨅ (i : ι), ⨆ (j : ι'), f i j
source
theorem Set.iSup_iInf_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (Function.swap fun (x1 x2 : ι') => x1 ≤ x2)] [Order.Frame α] {f : ι → ι' → α} (hf : ∀ (i : ι), Antitone (f i)) :
⨆ (j : ι'), ⨅ (i : ι), f i j = ⨅ (i : ι), ⨆ (j : ι'), f i j
source
theorem Set.iInf_iSup_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (Function.swap fun (x1 x2 : ι') => x1 ≤ x2)] [Order.Coframe α] {f : ι → ι' → α} (hf : ∀ (i : ι), Monotone (f i)) :
⨅ (j : ι'), ⨆ (i : ι), f i j = ⨆ (i : ι), ⨅ (j : ι'), f i j
source
theorem Set.iInf_iSup_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' fun (x1 x2 : ι') => x1 ≤ x2] [Order.Coframe α] {f : ι → ι' → α} (hf : ∀ (i : ι), Antitone (f i)) :
⨅ (j : ι'), ⨆ (i : ι), f i j = ⨆ (i : ι), ⨅ (j : ι'), f i j
source
theorem Set.iUnion_iInter_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [IsDirected ι' fun (x1 x2 : ι') => x1 ≤ x2] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Monotone (s i)) :
⋃ (j : ι'), ⋂ (i : ι), s i j = ⋂ (i : ι), ⋃ (j : ι'), s i j

An increasing union distributes over finite intersection.

source
theorem Set.iUnion_iInter_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [IsDirected ι' (Function.swap fun (x1 x2 : ι') => x1 ≤ x2)] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Antitone (s i)) :
⋃ (j : ι'), ⋂ (i : ι), s i j = ⋂ (i : ι), ⋃ (j : ι'), s i j

A decreasing union distributes over finite intersection.

source
theorem Set.iInter_iUnion_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [IsDirected ι' (Function.swap fun (x1 x2 : ι') => x1 ≤ x2)] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Monotone (s i)) :
⋂ (j : ι'), ⋃ (i : ι), s i j = ⋃ (i : ι), ⋂ (j : ι'), s i j

An increasing intersection distributes over finite union.

source
theorem Set.iInter_iUnion_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [IsDirected ι' fun (x1 x2 : ι') => x1 ≤ x2] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Antitone (s i)) :
⋂ (j : ι'), ⋃ (i : ι), s i j = ⋃ (i : ι), ⋂ (j : ι'), s i j

A decreasing intersection distributes over finite union.

source
theorem Set.iUnion_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [LinearOrder ι'] [Nonempty ι'] {α : ι → Type u_3} {I : Set ι} {s : (i : ι) → ι' → Set (α i)} (hI : I.Finite) (hs : ∀ i ∈ I, Monotone (s i)) :
(⋃ (j : ι'), I.pi fun (i : ι) => s i j) = I.pi fun (i : ι) => ⋃ (j : ι'), s i j
source
theorem Set.iUnion_univ_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [LinearOrder ι'] [Nonempty ι'] [Finite ι] {α : ι → Type u_3} {s : (i : ι) → ι' → Set (α i)} (hs : ∀ (i : ι), Monotone (s i)) :
(⋃ (j : ι'), univ.pi fun (i : ι) => s i j) = univ.pi fun (i : ι) => ⋃ (j : ι'), s i j
source
theorem Set.Finite.bddAbove {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] {s : Set α} (hs : s.Finite) :
BddAbove s

A finite set is bounded above.

source
theorem Set.Finite.bddAbove_biUnion {α : Type u} {β : Type v} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] {I : Set β} {S : β → Set α} (H : I.Finite) :
BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)

A finite union of sets which are all bounded above is still bounded above.

source
theorem Set.infinite_of_not_bddAbove {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] {s : Set α} :
¬BddAbove s → s.Infinite
source
theorem Set.Finite.bddBelow {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] {s : Set α} (hs : s.Finite) :
BddBelow s

A finite set is bounded below.

source
theorem Set.Finite.bddBelow_biUnion {α : Type u} {β : Type v} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] {I : Set β} {S : β → Set α} (H : I.Finite) :
BddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i)

A finite union of sets which are all bounded below is still bounded below.

source
theorem Set.infinite_of_not_bddBelow {α : Type u} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] {s : Set α} :
¬BddBelow s → s.Infinite
source
theorem Finset.bddAbove {α : Type u} [SemilatticeSup α] [Nonempty α] (s : Finset α) :
BddAbove ↑s

A finset is bounded above.

source
theorem Finset.bddBelow {α : Type u} [SemilatticeInf α] [Nonempty α] (s : Finset α) :
BddBelow ↑s

A finset is bounded below.

source
theorem Set.finite_diff_iUnion_Ioo {α : Type u} [LinearOrder α] (s : Set α) :
(s \ ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y).Finite
source
theorem Set.finite_diff_iUnion_Ioo' {α : Type u} [LinearOrder α] (s : Set α) :
(s \ ⋃ (x : ↑s × ↑s), Ioo ↑x.1 ↑x.2).Finite
source
theorem Directed.exists_mem_subset_of_finset_subset_biUnion {α : Type u_1} {ι : Type u_2} [Nonempty ι] {f : ι → Set α} (h : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) f) {s : Finset α} (hs : ↑s ⊆ ⋃ (i : ι), f i) :
∃ (i : ι), ↑s ⊆ f i
source
theorem DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {c : Set ι} (hn : c.Nonempty) (hc : DirectedOn (fun (i j : ι) => f i ⊆ f j) c) {s : Finset α} (hs : ↑s ⊆ ⋃ i ∈ c, f i) :
∃ i ∈ c, ↑s ⊆ f i
source
theorem DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion {α : Type u_1} {c : Set (Set α)} (hn : c.Nonempty) (hc : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) c) {s : Set α} (hs : s.Finite) (hsc : s ⊆ ⋃₀ c) :
∃ t ∈ c, s ⊆ t