Finite sets
This file defines predicates finite : set α → Prop and infinite : set α → Prop and proves some
basic facts about finite sets.
The subtype corresponding to a finite set is a finite type. Note
that because finite isn't a typeclass, this will not fire if it
is made into an instance
Equations
- h.fintype = classical.choice h
@[instance]
Finite sets can be lifted to finsets.
Equations
- set.can_lift = {coe := coe lift_base, cond := set.finite α, prf := _}
Membership of a subset of a finite type is decidable.
Using this as an instance leads to potential loops with subtype.fintype under certain decidability
assumptions, so it should only be declared a local instance.
Equations
@[instance]
Equations
- set.fintype_empty = fintype.of_finset ∅ set.fintype_empty._proof_1
@[instance]
def
set.fintype_insert'
{α : Type u}
{a : α}
(s : set α)
[fintype ↥s] :
a ∉ s → fintype ↥(has_insert.insert a s)
A fintype structure on insert a s.
Equations
- s.fintype_insert' h = fintype.of_finset {val := a :: s.to_finset.val, nodup := _} _
theorem
set.card_fintype_insert'
{α : Type u}
{a : α}
(s : set α)
[fintype ↥s]
(h : a ∉ s) :
fintype.card ↥(has_insert.insert a s) = fintype.card ↥s + 1
@[simp]
theorem
set.card_insert
{α : Type u}
{a : α}
(s : set α)
[fintype ↥s]
(h : a ∉ s)
{d : fintype ↥(has_insert.insert a s)} :
fintype.card ↥(has_insert.insert a s) = fintype.card ↥s + 1
theorem
set.card_image_of_injective
{α : Type u}
{β : Type v}
(s : set α)
[fintype ↥s]
{f : α → β}
[fintype ↥(f '' s)] :
function.injective f → fintype.card ↥(f '' s) = fintype.card ↥s
@[instance]
def
set.fintype_insert
{α : Type u}
[decidable_eq α]
(a : α)
(s : set α)
[fintype ↥s] :
fintype ↥(has_insert.insert a s)
Equations
- set.fintype_insert a s = dite (a ∈ s) (λ (h : a ∈ s), _.mpr (_.mpr _inst_2)) (λ (h : a ∉ s), s.fintype_insert' h)
@[simp]
theorem
set.finite.insert
{α : Type u}
(a : α)
{s : set α} :
s.finite → (has_insert.insert a s).finite
theorem
set.to_finset_insert
{α : Type u}
[decidable_eq α]
{a : α}
{s : set α}
(hs : s.finite) :
_.to_finset = has_insert.insert a hs.to_finset
theorem
set.finite.dinduction_on
{α : Type u}
{C : Π (s : set α), s.finite → Prop}
{s : set α}
(h : s.finite) :
C ∅ set.finite_empty → (∀ {a : α} {s : set α}, a ∉ s → ∀ (h : s.finite), C s h → C (has_insert.insert a s) _) → C s h
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
Embedding of ℕ into an infinite set.
Equations
@[instance]
Equations
- s.fintype_union t = fintype.of_finset (s.to_finset ∪ t.to_finset) _
@[instance]
Equations
- s.fintype_sep p = fintype.of_finset (finset.filter p s.to_finset) _
@[instance]
Equations
- s.fintype_inter t = s.fintype_sep t
A fintype structure on a set defines a fintype structure on its subset.
Equations
- s.fintype_subset h = _.mpr (s.fintype_inter t)
@[instance]
def
set.fintype_image
{α : Type u}
{β : Type v}
[decidable_eq β]
(s : set α)
(f : α → β)
[fintype ↥s] :
Equations
- s.fintype_image f = fintype.of_finset (finset.image f s.to_finset) _
@[instance]
Equations
@[instance]
Equations
def
set.fintype_of_fintype_image
{α : Type u}
{β : Type v}
(s : set α)
{f : α → β}
{g : β → option α}
(I : function.is_partial_inv f g)
[fintype ↥(f '' s)] :
If a function f has a partial inverse and sends a set s to a set with [fintype] instance,
then s has a fintype structure as well.
Equations
- s.fintype_of_fintype_image I = fintype.of_finset {val := multiset.filter_map g (f '' s).to_finset.val, nodup := _} _
theorem
set.finite_of_finite_image
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.inj_on f s → (f '' s).finite → s.finite
theorem
set.finite_image_iff
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β} :
set.inj_on f s → ((f '' s).finite ↔ s.finite)
theorem
set.finite.preimage
{α : Type u}
{β : Type v}
{s : set β}
{f : α → β} :
set.inj_on f (f ⁻¹' s) → s.finite → (f ⁻¹' s).finite
@[instance]
def
set.fintype_Union
{α : Type u}
[decidable_eq α]
{ι : Type u_1}
[fintype ι]
(f : ι → set α)
[Π (i : ι), fintype ↥(f i)] :
Equations
- set.fintype_Union f = fintype.of_finset (finset.univ.bind (λ (i : ι), (f i).to_finset)) _
def
set.fintype_bUnion
{α : Type u}
[decidable_eq α]
{ι : Type u_1}
{s : set ι}
[fintype ↥s]
(f : ι → set α) :
A union of sets with fintype structure over a set with fintype structure has a fintype
structure.
Equations
- set.fintype_bUnion f H = _.mpr (set.fintype_Union (λ (i : ↥s), f ↑i))
@[instance]
def
set.fintype_bUnion'
{α : Type u}
[decidable_eq α]
{ι : Type u_1}
{s : set ι}
[fintype ↥s]
(f : ι → set α)
[H : Π (i : ι), fintype ↥(f i)] :
Equations
- set.fintype_bUnion' f = set.fintype_bUnion (λ (i : ι), f i) (λ (i : ι) (_x : i ∈ s), H i)
@[instance]
Equations
@[instance]
Equations
- set.fintype_le_nat n = _.mp (set.fintype_lt_nat (n + 1))
@[instance]
def
set.fintype_image2
{α : Type u}
{β : Type v}
{γ : Type x}
[decidable_eq γ]
(f : α → β → γ)
(s : set α)
(t : set β)
[hs : fintype ↥s]
[ht : fintype ↥t] :
fintype ↥(set.image2 f s t)
image2 f s t is finitype if s and t are.
Equations
- set.fintype_image2 f s t = _.mpr ((s.prod t).fintype_image (λ (x : α × β), f x.fst x.snd))
theorem
set.finite.image2
{α : Type u}
{β : Type v}
{γ : Type x}
(f : α → β → γ)
{s : set α}
{t : set β} :
s.finite → t.finite → (set.image2 f s t).finite
If s : set α is a set with fintype instance and f : α → set β is a function such that
each f a, a ∈ s, has a fintype structure, then s >>= f has a fintype structure.
Equations
- s.fintype_bind f H = set.fintype_bUnion (λ (i : α), f i) H
@[instance]
def
set.fintype_bind'
{α β : Type u_1}
[decidable_eq β]
(s : set α)
[fintype ↥s]
(f : α → set β)
[H : Π (a : α), fintype ↥(f a)] :
Equations
- s.fintype_bind' f = s.fintype_bind f (λ (i : α) (_x : i ∈ s), H i)
@[instance]
def
set.fintype_seq
{α β : Type u}
[decidable_eq β]
(f : set (α → β))
(s : set α)
[fintype ↥f]
[fintype ↥s] :
Equations
- f.fintype_seq s = _.mpr (f.fintype_bind' (λ (_x : α → β), _x <$> s))
@[simp]
theorem
set.eq_finite_Union_of_finite_subset_Union
{α : Type u}
{ι : Type u_1}
{s : ι → set α}
{t : set α} :
@[instance]
Equations
If P is some relation between terms of γ and sets in γ,
such that every finite set t : set γ has some c : γ related to it,
then there is a recursively defined sequence u in γ
so u n is related to the image of {0, 1, ..., n-1} under u.
(We use this later to show sequentially compact sets are totally bounded.)
theorem
set.finite_range_ite
{α : Type u}
{β : Type v}
{p : α → Prop}
[decidable_pred p]
{f g : α → β} :
theorem
set.range_find_greatest_subset
{α : Type u}
{P : α → ℕ → Prop}
[Π (x : α), decidable_pred (P x)]
{b : ℕ} :
set.range (λ (x : α), nat.find_greatest (P x) b) ⊆ ↑(finset.range (b + 1))
theorem
set.finite_range_find_greatest
{α : Type u}
{P : α → ℕ → Prop}
[Π (x : α), decidable_pred (P x)]
{b : ℕ} :
(set.range (λ (x : α), nat.find_greatest (P x) b)).finite
theorem
set.card_lt_card
{α : Type u}
{s t : set α}
[fintype ↥s]
[fintype ↥t] :
s ⊂ t → fintype.card ↥s < fintype.card ↥t
theorem
set.card_le_of_subset
{α : Type u}
{s t : set α}
[fintype ↥s]
[fintype ↥t] :
s ⊆ t → fintype.card ↥s ≤ fintype.card ↥t
theorem
set.eq_of_subset_of_card_le
{α : Type u}
{s t : set α}
[fintype ↥s]
[fintype ↥t] :
s ⊆ t → fintype.card ↥t ≤ fintype.card ↥s → s = t
theorem
set.card_range_of_injective
{α : Type u}
{β : Type v}
[fintype α]
{f : α → β}
(hf : function.injective f)
[fintype ↥(set.range f)] :
fintype.card ↥(set.range f) = fintype.card α
theorem
set.finite.exists_maximal_wrt
{α : Type u}
{β : Type v}
[partial_order β]
(f : α → β)
(s : set α) :
A finite set is bounded above.
A finite set is bounded below.
@[simp]
theorem
finset.mem_preimage
{α : Type u}
{β : Type v}
{f : α → β}
{s : finset β}
{hf : set.inj_on f (f ⁻¹' ↑s)}
{x : α} :
theorem
finset.monotone_preimage
{α : Type u}
{β : Type v}
{f : α → β}
(h : function.injective f) :
theorem
finset.image_subset_iff_subset_preimage
{α : Type u}
{β : Type v}
[decidable_eq β]
{f : α → β}
{s : finset α}
{t : finset β}
(hf : set.inj_on f (f ⁻¹' ↑t)) :
finset.image f s ⊆ t ↔ s ⊆ t.preimage f hf
theorem
finset.image_preimage
{α : Type u}
{β : Type v}
[decidable_eq β]
(f : α → β)
(s : finset β)
[Π (x : β), decidable (x ∈ set.range f)]
(hf : set.inj_on f (f ⁻¹' ↑s)) :
finset.image f (s.preimage f hf) = finset.filter (λ (x : β), x ∈ set.range f) s
theorem
finset.image_preimage_of_bij
{α : Type u}
{β : Type v}
[decidable_eq β]
(f : α → β)
(s : finset β)
(hf : set.bij_on f (f ⁻¹' ↑s) ↑s) :
finset.image f (s.preimage f _) = s
theorem
finset.sigma_preimage_mk
{α : Type u}
{β : α → Type u_1}
[decidable_eq α]
(s : finset (Σ (a : α), β a))
(t : finset α) :
theorem
finset.sigma_preimage_mk_of_subset
{α : Type u}
{β : α → Type u_1}
[decidable_eq α]
(s : finset (Σ (a : α), β a))
{t : finset α} :
theorem
finset.sigma_image_fst_preimage_mk
{α : Type u}
{β : α → Type u_1}
[decidable_eq α]
(s : finset (Σ (a : α), β a)) :
theorem
finset.sum_preimage'
{α : Type u}
{β : Type v}
{γ : Type x}
[add_comm_monoid β]
(f : α → γ)
[decidable_pred (λ (x : γ), x ∈ set.range f)]
(s : finset γ)
(hf : set.inj_on f (f ⁻¹' ↑s))
(g : γ → β) :
theorem
finset.prod_preimage'
{α : Type u}
{β : Type v}
{γ : Type x}
[comm_monoid β]
(f : α → γ)
[decidable_pred (λ (x : γ), x ∈ set.range f)]
(s : finset γ)
(hf : set.inj_on f (f ⁻¹' ↑s))
(g : γ → β) :
theorem
finset.sum_preimage
{α : Type u}
{β : Type v}
{γ : Type x}
[add_comm_monoid β]
(f : α → γ)
(s : finset γ)
(hf : set.inj_on f (f ⁻¹' ↑s))
(g : γ → β) :
theorem
finset.prod_preimage
{α : Type u}
{β : Type v}
{γ : Type x}
[comm_monoid β]
(f : α → γ)
(s : finset γ)
(hf : set.inj_on f (f ⁻¹' ↑s))
(g : γ → β) :
theorem
finset.sum_preimage_of_bij
{α : Type u}
{β : Type v}
{γ : Type x}
[add_comm_monoid β]
(f : α → γ)
(s : finset γ)
(hf : set.bij_on f (f ⁻¹' ↑s) ↑s)
(g : γ → β) :
theorem
finset.prod_preimage_of_bij
{α : Type u}
{β : Type v}
{γ : Type x}
[comm_monoid β]
(f : α → γ)
(s : finset γ)
(hf : set.bij_on f (f ⁻¹' ↑s) ↑s)
(g : γ → β) :
A finset is bounded above.
A finset is bounded below.
theorem
fintype.exists_max
{α : Type u}
[fintype α]
[nonempty α]
{β : Type u_1}
[linear_order β]
(f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀