data.set.finite

# Finite sets

This file defines predicates finite : set α → Prop and infinite : set α → Prop and proves some basic facts about finite sets.

def set.finite {α : Type u} (s : set α) :
Prop

A set is finite if the subtype is a fintype, i.e. there is a list that enumerates its members.

Equations
def set.infinite {α : Type u} (s : set α) :
Prop

A set is infinite if it is not finite.

Equations
def set.finite.fintype {α : Type u} {s : set α} (h : s.finite) :

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
def set.finite.to_finset {α : Type u} {s : set α} (h : s.finite) :

Get a finset from a finite set

Equations
@[simp]
theorem set.finite.mem_to_finset {α : Type u} {s : set α} {h : s.finite} {a : α} :

@[simp]
theorem set.finite.to_finset.nonempty {α : Type u} {s : set α} (h : s.finite) :

@[simp]
theorem set.finite.coe_to_finset {α : Type u_1} {s : set α} (h : s.finite) :

theorem set.finite.exists_finset {α : Type u} {s : set α} :
s.finite(∃ (s' : finset α), ∀ (a : α), a s' a s)

theorem set.finite.exists_finset_coe {α : Type u} {s : set α} (hs : s.finite) :
∃ (s' : finset α), s' = s

@[instance]
def set.finset.can_lift {α : Type u} :
can_lift (set α) (finset α)

Finite sets can be lifted to finsets.

Equations
theorem set.finite_mem_finset {α : Type u} (s : finset α) :
{a : α | a s}.finite

theorem set.finite.of_fintype {α : Type u} [fintype α] (s : set α) :

theorem set.exists_finite_iff_finset {α : Type u} {p : set α → Prop} :
(∃ (s : set α), s.finite p s) ∃ (s : finset α), p s

def set.decidable_mem_of_fintype {α : Type u} [decidable_eq α] (s : set α) [fintype s] (a : α) :

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]
def set.fintype_empty {α : Type u} :

Equations
theorem set.empty_card {α : Type u} :

@[simp]
theorem set.empty_card' {α : Type u} {h : fintype } :

@[simp]
theorem set.finite_empty {α : Type u} :

@[instance]
def set.finite.inhabited {α : Type u} :
inhabited {s // s.finite}

Equations
def set.fintype_insert' {α : Type u} {a : α} (s : set α) [fintype s] (h : a s) :

A fintype structure on insert a s.

Equations
theorem set.card_fintype_insert' {α : Type u} {a : α} (s : set α) [fintype s] (h : a s) :

@[simp]
theorem set.card_insert {α : Type u} {a : α} (s : set α) [fintype s] (h : a s) {d : fintype (insert a s)} :

theorem set.card_image_of_inj_on {α : Type u} {β : Type v} {s : set α} [fintype s] {f : α → β} [fintype (f '' s)] (H : ∀ (x : α), x s∀ (y : α), y sf x = f yx = y) :

theorem set.card_image_of_injective {α : Type u} {β : Type v} (s : set α) [fintype s] {f : α → β} [fintype (f '' s)] (H : function.injective f) :

@[instance]
def set.fintype_insert {α : Type u} [decidable_eq α] (a : α) (s : set α) [fintype s] :

Equations
@[simp]
theorem set.finite.insert {α : Type u} (a : α) {s : set α} :
s.finite(insert a s).finite

theorem set.to_finset_insert {α : Type u} [decidable_eq α] {a : α} {s : set α} (hs : s.finite) :

theorem set.finite.induction_on {α : Type u} {C : set α → Prop} {s : set α} (h : s.finite) (H0 : C ) (H1 : ∀ {a : α} {s : set α}, a ss.finiteC sC (insert a s)) :
C s

theorem set.finite.dinduction_on {α : Type u} {C : Π (s : set α), s.finite → Prop} {s : set α} (h : s.finite) (H0 : C set.finite_empty) (H1 : ∀ {a : α} {s : set α}, a s∀ (h : s.finite), C s hC (insert a s) _) :
C s h

@[instance]
def set.fintype_singleton {α : Type u} (a : α) :

Equations
@[simp]
theorem set.card_singleton {α : Type u} (a : α) :
= 1

@[simp]
theorem set.finite_singleton {α : Type u} (a : α) :
{a}.finite

@[instance]
def set.fintype_pure {α : Type u} (a : α) :

Equations
theorem set.finite_pure {α : Type u} (a : α) :

@[instance]
def set.fintype_univ {α : Type u} [fintype α] :

Equations
theorem set.finite_univ {α : Type u} [fintype α] :

theorem set.infinite_univ_iff {α : Type u} :

theorem set.infinite_univ {α : Type u} [h : infinite α] :

theorem set.infinite_coe_iff {α : Type u} {s : set α} :

theorem set.infinite.to_subtype {α : Type u} {s : set α} (h : s.infinite) :

def set.infinite.nat_embedding {α : Type u} (s : set α) (h : s.infinite) :

Embedding of ℕ into an infinite set.

Equations
theorem set.infinite.exists_subset_card_eq {α : Type u} {s : set α} (hs : s.infinite) (n : ) :
∃ (t : finset α), t s t.card = n

@[instance]
def set.fintype_union {α : Type u} [decidable_eq α] (s t : set α) [fintype s] [fintype t] :

Equations
• = _
theorem set.finite.union {α : Type u} {s t : set α} :
s.finitet.finite(s t).finite

@[instance]
def set.fintype_sep {α : Type u} (s : set α) (p : α → Prop) [fintype s]  :
fintype {a ∈ s | p a}

Equations
@[instance]
def set.fintype_inter {α : Type u} (s t : set α) [fintype s]  :

Equations
def set.fintype_subset {α : Type u} (s : set α) {t : set α} [fintype s] (h : t s) :

A fintype structure on a set defines a fintype structure on its subset.

Equations
theorem set.finite.subset {α : Type u} {s : set α} :
s.finite∀ {t : set α}, t s → t.finite

theorem set.infinite_mono {α : Type u} {s t : set α} (h : s t) :

@[instance]
def set.fintype_image {α : Type u} {β : Type v} [decidable_eq β] (s : set α) (f : α → β) [fintype s] :

Equations
@[instance]
def set.fintype_range {α : Type u} {β : Type v} [decidable_eq β] (f : α → β) [fintype α] :

Equations
theorem set.finite_range {α : Type u} {β : Type v} (f : α → β) [fintype α] :

theorem set.finite.image {α : Type u} {β : Type v} {s : set α} (f : α → β) :
s.finite(f '' s).finite

theorem set.infinite_of_infinite_image {α : Type u} {β : Type v} (f : α → β) {s : set α} (hs : (f '' s).infinite) :

theorem set.finite.dependent_image {α : Type u} {β : Type v} {s : set α} (hs : s.finite) {F : Π (i : α), i s → β} {t : set β} (H : ∀ (y : β), y t(∃ (x : α) (hx : x s), y = F x hx)) :

@[instance]
def set.fintype_map {α β : Type u_1} [decidable_eq β] (s : set α) (f : α → β) [fintype s] :

Equations
theorem set.finite.map {α β : Type u_1} {s : set α} (f : α → β) :
s.finite(f <\$> s).finite

def set.fintype_of_fintype_image {α : Type u} {β : Type v} (s : set α) {f : α → β} {g : β → } (I : 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
theorem set.finite_of_finite_image {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : s) :
(f '' s).finite → s.finite

theorem set.finite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : s) :

theorem set.infinite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α → β} (hi : s) :

theorem set.infinite_of_inj_on_maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} (hi : s) (hm : s t) (hs : s.infinite) :

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

theorem set.finite.preimage {α : Type u} {β : Type v} {s : set β} {f : α → β} (I : (f ⁻¹' s)) (h : s.finite) :

theorem set.finite.preimage_embedding {α : Type u} {β : Type v} {s : set β} (f : α β) (h : s.finite) :

@[instance]
def set.fintype_Union {α : Type u} [decidable_eq α] {ι : Type u_1} [fintype ι] (f : ι → set α) [Π (i : ι), fintype (f i)] :
fintype (⋃ (i : ι), f i)

Equations
theorem set.finite_Union {α : Type u} {ι : Type u_1} [fintype ι] {f : ι → set α} (H : ∀ (i : ι), (f i).finite) :
(⋃ (i : ι), f i).finite

def set.fintype_set_bUnion {α : Type u} [decidable_eq α] {ι : Type u_1} {s : set ι} [fintype s] (f : ι → set α) (H : Π (i : ι), i sfintype (f i)) :
fintype (⋃ (i : ι) (H : i s), f i)

A union of sets with fintype structure over a set with fintype structure has a fintype structure.

Equations
@[instance]
def set.fintype_set_bUnion' {α : Type u} [decidable_eq α] {ι : Type u_1} {s : set ι} [fintype s] (f : ι → set α) [H : Π (i : ι), fintype (f i)] :
fintype (⋃ (i : ι) (H : i s), f i)

Equations
theorem set.finite.sUnion {α : Type u} {s : set (set α)} (h : s.finite) (H : ∀ (t : set α), t s → t.finite) :

theorem set.finite.bUnion {α : Type u_1} {ι : Type u_2} {s : set ι} {f : Π (i : ι), i sset α} :
s.finite(∀ (i : ι) (H : i s), (f i H).finite)(⋃ (i : ι) (H : i s), f i H).finite

@[instance]
def set.fintype_lt_nat (n : ) :
fintype {i : | i < n}

Equations
@[instance]
def set.fintype_le_nat (n : ) :
fintype {i : | i n}

Equations
theorem set.finite_le_nat (n : ) :
{i : | i n}.finite

theorem set.finite_lt_nat (n : ) :
{i : | i < n}.finite

@[instance]
def set.fintype_prod {α : Type u} {β : Type v} (s : set α) (t : set β) [fintype s] [fintype t] :

Equations
theorem set.finite.prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
s.finitet.finite(s.prod t).finite

@[instance]
def set.fintype_image2 {α : Type u} {β : Type v} {γ : Type x} [decidable_eq γ] (f : α → β → γ) (s : set α) (t : set β) [hs : fintype s] [ht : fintype t] :

image2 f s t is finitype if s and t are.

Equations
theorem set.finite.image2 {α : Type u} {β : Type v} {γ : Type x} (f : α → β → γ) {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
s t).finite

def set.fintype_bUnion {α β : Type u_1} [decidable_eq β] (s : set α) [fintype s] (f : α → set β) (H : Π (a : α), a sfintype (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
@[instance]
def set.fintype_bUnion' {α β : Type u_1} [decidable_eq β] (s : set α) [fintype s] (f : α → set β) [H : Π (a : α), fintype (f a)] :

Equations
• = (λ (i : α) (_x : i s), H i)
theorem set.finite_bUnion {α β : Type u_1} {s : set α} {f : α → set β} :
s.finite(∀ (a : α), a s(f a).finite)(s >>= f).finite

@[instance]
def set.fintype_seq {α β : Type u} [decidable_eq β] (f : set (α → β)) (s : set α) [fintype f] [fintype s] :

Equations
theorem set.finite.seq {α β : Type u} {f : set (α → β)} {s : set α} :
f.finites.finite(f <*> s).finite

theorem set.finite.finite_subsets {α : Type u} {a : set α} (h : a.finite) :
{b : set α | b a}.finite

There are finitely many subsets of a given finite set

theorem set.exists_min_image {α : Type u} {β : Type v} [linear_order β] (s : set α) (f : α → β) (h1 : s.finite) :
s.nonempty(∃ (a : α) (H : a s), ∀ (b : α), b sf a f b)

theorem set.exists_max_image {α : Type u} {β : Type v} [linear_order β] (s : set α) (f : α → β) (h1 : s.finite) :
s.nonempty(∃ (a : α) (H : a s), ∀ (b : α), b sf b f a)

theorem finset.finite_to_set {α : Type u} (s : finset α) :

@[simp]
theorem finset.coe_bUnion {α : Type u} {β : Type v} [decidable_eq β] {s : finset α} {f : α → } :
(s.bUnion f) = ⋃ (x : α) (H : x s), (f x)

@[simp]
theorem finset.finite_to_set_to_finset {α : Type u_1} (s : finset α) :

theorem set.finite_subset_Union {α : Type u} {s : set α} (hs : s.finite) {ι : Type u_1} {t : ι → set α} (h : s ⋃ (i : ι), t i) :
∃ (I : set ι), I.finite s ⋃ (i : ι) (H : i I), t i

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) :
∃ (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

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.

@[instance]

Equations
theorem set.seq_of_forall_finite_exists {γ : Type u_1} {P : γ → set γ → Prop} (h : ∀ (t : set γ), t.finite(∃ (c : γ), P c t)) :
∃ (u : → γ), ∀ (n : ), P (u n) (u '' set.Iio n)

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} {f g : α → β} (hf : (set.range f).finite) (hg : (set.range g).finite) :
(set.range (λ (x : α), ite (p x) (f x) (g x))).finite

theorem set.finite_range_const {α : Type u} {β : Type v} {c : β} :
(set.range (λ (x : α), c)).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.card_lt_card {α : Type u} {s t : set α} [fintype s] [fintype t] (h : s t) :

theorem set.card_le_of_subset {α : Type u} {s t : set α} [fintype s] [fintype t] (hsub : s t) :

theorem set.eq_of_subset_of_card_le {α : Type u} {s t : set α} [fintype s] [fintype t] (hsub : s t) (hcard : ) :
s = t

theorem set.subset_iff_to_finset_subset {α : Type u} (s t : set α) [fintype s] [fintype t] :
s t

theorem set.card_range_of_injective {α : Type u} {β : Type v} [fintype α] {f : α → β} (hf : function.injective f) [fintype (set.range f)] :

theorem set.finite.exists_maximal_wrt {α : Type u} {β : Type v} (f : α → β) (s : set α) (h : s.finite) :
s.nonempty(∃ (a : α) (H : a s), ∀ (a' : α), a' sf a f a'f a = f a')

theorem set.finite.card_to_finset {α : Type u} {s : set α} [fintype s] (h : s.finite) :

theorem set.to_finset_compl {α : Type u_1} [fintype α] (s : set α) :

theorem set.to_finset_inter {α : Type u_1} [fintype α] (s t : set α) :
(s t).to_finset =

theorem set.to_finset_union {α : Type u_1} [fintype α] (s t : set α) :
(s t).to_finset =

theorem set.finite.bdd_above {α : Type u} [nonempty α] {s : set α} (hs : s.finite) :

A finite set is bounded above.

theorem set.finite.bdd_above_bUnion {α : Type u} {β : Type v} [nonempty α] {I : set β} {S : β → set α} (H : I.finite) :
bdd_above (⋃ (i : β) (H : i I), S i) ∀ (i : β), i Ibdd_above (S i)

A finite union of sets which are all bounded above is still bounded above.

theorem set.finite.bdd_below {α : Type u} [nonempty α] {s : set α} (hs : s.finite) :

A finite set is bounded below.

theorem set.finite.bdd_below_bUnion {α : Type u} {β : Type v} [nonempty α] {I : set β} {S : β → set α} (H : I.finite) :
bdd_below (⋃ (i : β) (H : i I), S i) ∀ (i : β), i Ibdd_below (S i)

A finite union of sets which are all bounded below is still bounded below.

theorem finset.bdd_above {α : Type u} [nonempty α] (s : finset α) :

A finset is bounded above.

theorem finset.bdd_below {α : Type u} [nonempty α] (s : finset α) :

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₀