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 _
See also fintype_or_infinite.
@[protected, instance]
Finite sets can be lifted to finsets.
Equations
- set.finset.can_lift = {coe := coe coe_to_lift, 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
@[protected, instance]
Equations
- set.fintype_empty = fintype.of_finset ∅ set.fintype_empty._proof_1
@[protected, instance]
theorem
set.card_fintype_insert'
{α : Type u}
{a : α}
(s : set α)
[fintype ↥s]
(h : a ∉ s) :
fintype.card ↥(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)]
(H : function.injective f) :
fintype.card ↥(f '' s) = fintype.card ↥s
@[protected, instance]
Equations
- set.fintype_insert a s = dite (a ∈ s) (λ (h : a ∈ s), _.mpr (_.mpr _inst_2)) (λ (h : a ∉ s), s.fintype_insert' h)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
Embedding of ℕ into an infinite set.
Equations
@[protected, instance]
Equations
- s.fintype_union t = fintype.of_finset (s.to_finset ∪ t.to_finset) _
@[protected, instance]
Equations
- s.fintype_sep p = fintype.of_finset (finset.filter p s.to_finset) _
@[protected, instance]
def
set.fintype_inter
{α : Type u}
(s t : set α)
[fintype ↥s]
[decidable_pred (λ (_x : α), _x ∈ t)] :
Equations
- s.fintype_inter t = s.fintype_sep t
def
set.fintype_subset
{α : Type u}
(s : set α)
{t : set α}
[fintype ↥s]
[decidable_pred (λ (_x : α), _x ∈ t)]
(h : t ⊆ s) :
A fintype structure on a set defines a fintype structure on its subset.
Equations
- s.fintype_subset h = _.mpr (s.fintype_inter t)
@[protected, 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) _
@[protected, instance]
Equations
theorem
set.finite.of_preimage
{α : Type u}
{β : Type v}
{f : α → β}
{s : set β}
(h : (f ⁻¹' s).finite)
(hf : function.surjective f) :
s.finite
@[protected, 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 : α → β}
(hi : set.inj_on f s) :
theorem
set.finite_image_iff
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
(hi : set.inj_on f s) :
theorem
set.infinite_image_iff
{α : Type u}
{β : Type v}
{s : set α}
{f : α → β}
(hi : set.inj_on f s) :
theorem
set.infinite_of_inj_on_maps_to
{α : Type u}
{β : Type v}
{s : set α}
{t : set β}
{f : α → β}
(hi : set.inj_on f s)
(hm : set.maps_to f s t)
(hs : s.infinite) :
t.infinite
theorem
set.infinite.exists_lt_map_eq_of_maps_to
{α : Type u}
{β : Type v}
[linear_order α]
{s : set α}
{t : set β}
{f : α → β}
(hs : s.infinite)
(hf : set.maps_to f s t)
(ht : t.finite) :
theorem
set.infinite_range_of_injective
{α : Type u}
{β : Type v}
[infinite α]
{f : α → β}
(hi : function.injective f) :
theorem
set.infinite_of_injective_forall_mem
{α : Type u}
{β : Type v}
[infinite α]
{s : set β}
{f : α → β}
(hi : function.injective f)
(hf : ∀ (x : α), f x ∈ s) :
s.infinite
theorem
set.finite.preimage
{α : Type u}
{β : Type v}
{s : set β}
{f : α → β}
(I : set.inj_on f (f ⁻¹' s))
(h : s.finite) :
@[protected, instance]
def
set.fintype_Union
{α : Type u}
{ι : Sort w}
[decidable_eq α]
[fintype (plift ι)]
(f : ι → set α)
[Π (i : ι), fintype ↥(f i)] :
Equations
- set.fintype_Union f = fintype.of_finset (finset.univ.bUnion (λ (i : plift ι), (f i.down).to_finset)) _
def
set.fintype_bUnion
{α : Type u}
[decidable_eq α]
{ι : Type u_1}
{s : set ι}
[fintype ↥s]
(f : ι → set α)
(H : Π (i : ι), i ∈ s → fintype ↥(f i)) :
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))
@[protected, 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)
@[protected, instance]
Equations
@[protected, instance]
Equations
- set.fintype_le_nat n = _.mpr (_.mp (set.fintype_lt_nat (n + 1)))
@[protected, 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 ×ˢ t).fintype_image (λ (x : α × β), f x.fst x.snd))
theorem
set.finite.image2
{α : Type u}
{β : Type v}
{γ : Type x}
(f : α → β → γ)
{s : set α}
{t : set β}
(hs : s.finite)
(ht : t.finite) :
(set.image2 f s t).finite
def
set.fintype_bind
{α β : Type u_1}
[decidable_eq β]
(s : set α)
[fintype ↥s]
(f : α → set β)
(H : Π (a : α), a ∈ s → fintype ↥(f a)) :
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
@[protected, 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)
@[protected, instance]
def
set.fintype_seq
{α : Type u}
{β : Type v}
[decidable_eq β]
(f : set (α → β))
(s : set α)
[fintype ↥f]
[fintype ↥s] :
Equations
- f.fintype_seq s = _.mpr (set.fintype_bUnion' (λ (i : α → β), i '' s))
@[protected, instance]
def
set.fintype_seq'
{α β : Type u}
[decidable_eq β]
(f : set (α → β))
(s : set α)
[fintype ↥f]
[fintype ↥s] :
Equations
- f.fintype_seq' s = f.fintype_seq s
theorem
set.exists_min_image
{α : Type u}
{β : Type v}
[linear_order β]
(s : set α)
(f : α → β)
(h1 : s.finite) :
theorem
set.exists_max_image
{α : Type u}
{β : Type v}
[linear_order β]
(s : set α)
(f : α → β)
(h1 : s.finite) :
theorem
set.exists_lower_bound_image
{α : Type u}
{β : Type v}
[hα : nonempty α]
[linear_order β]
(s : set α)
(f : α → β)
(h : s.finite) :
theorem
set.exists_upper_bound_image
{α : Type u}
{β : Type v}
[hα : nonempty α]
[linear_order β]
(s : set α)
(f : α → β)
(h : s.finite) :
@[simp]
theorem
set.eq_finite_Union_of_finite_subset_Union
{α : Type u}
{ι : Type u_1}
{s : ι → set α}
{t : set α}
(tfin : t.finite)
(h : t ⊆ ⋃ (i : ι), s i) :
theorem
set.Union_Inter_of_monotone
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[fintype ι]
[linear_order ι']
[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.
@[protected, instance]
Equations
theorem
set.seq_of_forall_finite_exists
{γ : Type u_1}
{P : γ → set γ → Prop}
(h : ∀ (t : set γ), t.finite → (∃ (c : γ), P c t)) :
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 : α → β}
(hf : (set.range f).finite)
(hg : (set.range g).finite) :
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.eq_of_subset_of_card_le
{α : Type u}
{s t : set α}
[fintype ↥s]
[fintype ↥t]
(hsub : s ⊆ t)
(hcard : 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 α)
(h : s.finite) :
@[protected, instance]
Equations
- s.fintype_sdiff t = fintype.of_finset (s.to_finset \ t.to_finset) _
theorem
set.to_finset_ne_eq_erase
{α : Type u_1}
[decidable_eq α]
[fintype α]
(a : α)
[fintype ↥{x : α | x ≠ a}] :
{x : α | x ≠ a}.to_finset = finset.univ.erase a
theorem
set.card_ne_eq
{α : Type u}
[fintype α]
(a : α)
[fintype ↥{x : α | x ≠ a}] :
fintype.card ↥{x : α | x ≠ a} = fintype.card α - 1
@[protected]
theorem
set.finite.bdd_above
{α : Type u}
[semilattice_sup α]
[nonempty α]
{s : set α}
(hs : s.finite) :
A finite set is bounded above.
@[protected]
theorem
set.finite.bdd_below
{α : Type u}
[semilattice_inf α]
[nonempty α]
{s : set α}
(hs : s.finite) :
A finite set is bounded below.
@[protected]
A finset is bounded above.
@[protected]
A finset is bounded below.
@[simp]
theorem
fintype.card_subtype_compl
{α : Type u}
[fintype α]
{p : α → Prop}
[decidable_pred p] :
fintype.card {x // ¬p x} = fintype.card α - fintype.card {x // p x}
theorem
fintype.card_compl_eq_card_compl
{α : Type u}
[fintype α]
{p q : α → Prop}
[decidable_pred p]
[decidable_pred q]
(h : fintype.card {x // p x} = fintype.card {x // q x}) :
fintype.card {x // ¬p x} = fintype.card {x // ¬q x}
If two subtypes of a fintype have equal cardinality, so do their complements.
theorem
set.finite_of_forall_between_eq_endpoints
{α : Type u_1}
[linear_order α]
(s : set α)
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∀ (z : α), z ∈ s → x ≤ y → y ≤ z → x = y ∨ y = z) :
s.finite
If a set s does not contain any elements between any pair of elements x, z ∈ s with x ≤ z
(i.e if given x, y, z ∈ s such that x ≤ y ≤ z, then y is either x or z), then s is
finite.