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]
:
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
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.
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.
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 : ι → α)
:
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.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)
:
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 α}
:
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)
:
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 α}
:
A finset is bounded above.
A finset is bounded below.