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_reducible]
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_reducible]
instance
Set.fintypesUnion
{α : Type u}
[DecidableEq α]
{s : Set (Set α)}
[Fintype ↑s]
[H : (t : ↑s) → Fintype ↑↑t]
:
Equations
theorem
Set.toFinset_iUnion
{α : Type u}
{β : Type v}
[Fintype β]
[DecidableEq α]
(f : β → Set α)
[(w : β) → Fintype ↑(f w)]
:
@[instance_reducible]
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 : ↥s.toFinset) => (t ↑x).toFinset) ⋯
Instances For
@[instance_reducible]
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_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).
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.
@[simp]
theorem
Set.finite_iUnion_of_subsingleton
{α : Type u}
{ι : Sort u_1}
[Subsingleton ι]
{s : ι → Set α}
:
theorem
Set.PairwiseDisjoint.finite_biUnion_iff
{α : Type u}
{β : Type v}
{f : β → Set α}
{s : Set β}
(hs : s.PairwiseDisjoint f)
:
An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but finitely many are empty.
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 #
Infinite sets #
theorem
Set.infinite_iUnion
{α : Type u}
{ι : Type u_1}
[Infinite ι]
{s : ι → Set α}
(hs : Function.Injective s)
:
(⋃ (i : ι), s i).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 : ι → α)
:
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 : ι → α)
:
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 : ι → α)
:
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 : ι → α)
:
theorem
Set.Finite.iSup_biInf_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsDirectedOrder ι']
[Order.Frame α]
{s : Set ι}
(hs : s.Finite)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Monotone (f i))
:
theorem
Set.Finite.iInf_biSup_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsCodirectedOrder ι']
[Order.Coframe α]
{s : Set ι}
(hs : s.Finite)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Monotone (f i))
:
theorem
Set.Finite.iSup_biInf_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsCodirectedOrder ι']
[Order.Frame α]
{s : Set ι}
(hs : s.Finite)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Antitone (f i))
:
theorem
Set.Finite.iInf_biSup_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι']
[Nonempty ι']
[IsDirectedOrder ι']
[Order.Coframe α]
{s : Set ι}
(hs : s.Finite)
{f : ι → ι' → α}
(hf : ∀ i ∈ s, Antitone (f i))
:
theorem
iSup_iInf_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirectedOrder ι']
[Order.Frame α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Monotone (f i))
:
theorem
iInf_iSup_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsCodirectedOrder ι']
[Order.Coframe α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Monotone (f i))
:
theorem
iSup_iInf_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsCodirectedOrder ι']
[Order.Frame α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Antitone (f i))
:
theorem
iInf_iSup_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirectedOrder ι']
[Order.Coframe α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Antitone (f i))
:
@[deprecated iSup_iInf_of_monotone (since := "2026-02-03")]
theorem
Set.iSup_iInf_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirectedOrder ι']
[Order.Frame α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Monotone (f i))
:
Alias of iSup_iInf_of_monotone.
@[deprecated iSup_iInf_of_antitone (since := "2026-02-03")]
theorem
Set.iSup_iInf_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsCodirectedOrder ι']
[Order.Frame α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Antitone (f i))
:
Alias of iSup_iInf_of_antitone.
@[deprecated iInf_iSup_of_monotone (since := "2026-02-03")]
theorem
Set.iInf_iSup_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsCodirectedOrder ι']
[Order.Coframe α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Monotone (f i))
:
Alias of iInf_iSup_of_monotone.
@[deprecated iInf_iSup_of_antitone (since := "2026-02-03")]
theorem
Set.iInf_iSup_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[Nonempty ι']
[IsDirectedOrder ι']
[Order.Coframe α]
{f : ι → ι' → α}
(hf : ∀ (i : ι), Antitone (f i))
:
Alias of iInf_iSup_of_antitone.
theorem
Set.iUnion_iInter_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsDirectedOrder ι']
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Monotone (s i))
:
An increasing union distributes over finite intersection.
theorem
Set.iUnion_iInter_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsCodirectedOrder ι']
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Antitone (s i))
:
A decreasing union distributes over finite intersection.
theorem
Set.iInter_iUnion_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsCodirectedOrder ι']
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Monotone (s i))
:
An increasing intersection distributes over finite union.
theorem
Set.iInter_iUnion_of_antitone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Finite ι]
[Preorder ι']
[IsDirectedOrder ι']
[Nonempty ι']
{s : ι → ι' → Set α}
(hs : ∀ (i : ι), Antitone (s i))
:
A decreasing intersection distributes over finite union.
theorem
iInf_iSup_eq_of_finite
{α : Type u}
{ι : Sort v}
{κ : ι → Sort w}
[Order.Frame α]
[Finite ι]
{f : (a : ι) → κ a → α}
:
theorem
iSup_iInf_eq_of_finite
{α : Type u}
{ι : Sort v}
{κ : ι → Sort w}
[Order.Coframe α]
[Finite ι]
{f : (a : ι) → κ a → α}
:
theorem
Set.Finite.biInf_iSup_eq
{α : Type u}
{ι : Type v}
{κ : ι → Sort w}
[Nonempty ((a : ι) → κ a)]
[Order.Frame α]
{s : Set ι}
(hs : s.Finite)
{f : (a : ι) → κ a → α}
:
theorem
Set.Finite.biSup_iInf_eq
{α : Type u}
{ι : Type v}
{κ : ι → Sort w}
[Nonempty ((a : ι) → κ a)]
[Order.Coframe α]
{s : Set ι}
(hs : s.Finite)
{f : (a : ι) → κ a → α}
:
theorem
Set.Finite.bddAbove
{α : Type u}
[Preorder α]
[IsDirectedOrder α]
[Nonempty α]
{s : Set α}
(hs : s.Finite)
:
BddAbove s
A finite set is bounded above.
theorem
Set.Finite.bddBelow
{α : Type u}
[Preorder α]
[IsCodirectedOrder α]
[Nonempty α]
{s : Set α}
(hs : s.Finite)
:
BddBelow s
A finite set is bounded below.
theorem
Set.infinite_of_not_bddAbove
{α : Type u}
[Preorder α]
[IsDirectedOrder α]
[Nonempty α]
{s : Set α}
:
theorem
Set.infinite_of_not_bddBelow
{α : Type u}
[Preorder α]
[IsCodirectedOrder α]
[Nonempty α]
{s : Set α}
:
A finset is bounded above.
A finset is bounded below.
@[deprecated Set.finite_sdiff_iUnion_Ioo (since := "2026-06-03")]
Alias of Set.finite_sdiff_iUnion_Ioo.
@[deprecated Set.finite_sdiff_iUnion_Ioo' (since := "2026-06-03")]
Alias of Set.finite_sdiff_iUnion_Ioo'.
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