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.

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) ⋯

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)

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

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) ⋯

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.

instance Finite.Set.finite_iUnion {α : Type u} {ι : Sort w} [Finite ι] (f : ι → Set α) [∀ (i : ι), Finite ↑(f i)] : Finite ↑(⋃ (i : ι), f i)

instance Finite.Set.finite_sUnion {α : Type u} {s : Set (Set α)} [Finite ↑s] [H : ∀ (t : ↑s), Finite ↑↑t] : Finite ↑(⋃₀ s)

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)

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)

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).

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.

theorem Set.finite_iUnion {α : Type u} {ι : Sort w} [Finite ι] {f : ι → Set α} (H : ∀ (i : ι), (f i).Finite) : (⋃ (i : ι), f i).Finite

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.

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

theorem Set.Finite.sUnion {α : Type u} {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, t.Finite) : (⋃₀ s).Finite

theorem Set.Finite.sInter {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : t.Finite) : (⋂₀ s).Finite

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.

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.

theorem Set.Infinite.iUnion {α : Type u} {ι : Sort u_1} {s : ι → Set α} (i : ι) (hi : (s i).Infinite) : (⋃ (i : ι), s i).Infinite

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

@[simp]

theorem Set.finite_iUnion_of_subsingleton {α : Type u} {ι : Sort u_1} [Subsingleton ι] {s : ι → Set α} : (⋃ (i : ι), s i).Finite ↔ ∀ (i : ι), (s i).Finite

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.

theorem Set.Finite.preimage' {α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite) : (f ⁻¹' s).Finite

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.

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

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

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

theorem Set.infinite_iUnion {α : Type u} {ι : Type u_1} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) : (⋃ (i : ι), s i).Infinite

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

theorem Set.Infinite.sUnion {α : Type u} {s : Set (Set α)} (hs : s.Infinite) : (⋃₀ s).Infinite

Order properties

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)

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)

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)

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)

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

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

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

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

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

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

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

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

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.

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.

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.

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.

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

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

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.

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.

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

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.

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.

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

theorem Finset.bddAbove {α : Type u} [SemilatticeSup α] [Nonempty α] (s : Finset α) : BddAbove ↑s

A finset is bounded above.

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

A finset is bounded below.

theorem Set.finite_diff_iUnion_Ioo {α : Type u} [LinearOrder α] (s : Set α) : (s \ ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y).Finite

theorem Set.finite_diff_iUnion_Ioo' {α : Type u} [LinearOrder α] (s : Set α) : (s \ ⋃ (x : ↑s × ↑s), Ioo ↑x.1 ↑x.2).Finite

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

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

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