data.set.finite

# Finite sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines predicates for finite and infinite sets and provides `fintype` instances for many set constructions. It also proves basic facts about finite sets and gives ways to manipulate `set.finite` expressions.

## Main definitions #

• `set.finite : set α → Prop`
• `set.infinite : set α → Prop`
• `set.to_finite` to prove `set.finite` for a `set` from a `finite` instance.
• `set.finite.to_finset` to noncomputably produce a `finset` from a `set.finite` proof. (See `set.to_finset` for a computable version.)

## Implementation #

A finite set is defined to be a set whose coercion to a type has a `fintype` instance. Since `set.finite` is `Prop`-valued, this is the mere fact that the `fintype` instance exists.

There are two components to finiteness constructions. The first is `fintype` instances for each construction. This gives a way to actually compute a `finset` that represents the set, and these may be accessed using `set.to_finset`. This gets the `finset` in the correct form, since otherwise `finset.univ : finset s` is a `finset` for the subtype for `s`. The second component is "constructors" for `set.finite` that give proofs that `fintype` instances exist classically given other `set.finite` proofs. Unlike the `fintype` instances, these do not use any decidability instances since they do not compute anything.

## Tags #

finite sets

@[protected]
inductive set.finite {α : Type u} (s : set α) :
Prop

A set is finite if there is a `finset` with the same elements. This is represented as there being a `fintype` instance for the set coerced to a type.

Note: this is a custom inductive type rather than `nonempty (fintype s)` so that it won't be frozen as a local instance.

Instances for `set.finite`
theorem set.finite_def {α : Type u} {s : set α} :
theorem set.finite.nonempty_fintype {α : Type u} {s : set α} :

Alias of the forward direction of `set.finite_def`.

theorem set.finite_coe_iff {α : Type u} {s : set α} :
theorem set.to_finite {α : Type u} (s : set α) [finite s] :

Constructor for `set.finite` using a `finite` instance.

@[protected]
theorem set.finite.of_finset {α : Type u} {p : set α} (s : finset α) (H : (x : α), x s x p) :

Construct a `finite` instance for a `set` from a `finset` with the same elements.

@[protected]
theorem set.finite.to_subtype {α : Type u} {s : set α} (h : s.finite) :

Projection of `set.finite` to its `finite` instance. This is intended to be used with dot notation. See also `set.finite.fintype` and `set.finite.nonempty_fintype`.

@[protected]
noncomputable def set.finite.fintype {α : Type u} {s : set α} (h : s.finite) :

A finite set coerced to a type is a `fintype`. This is the `fintype` projection for a `set.finite`.

Note that because `finite` isn't a typeclass, this definition will not fire if it is made into an instance

Equations
@[protected]
noncomputable def set.finite.to_finset {α : Type u} {s : set α} (h : s.finite) :

Using choice, get the `finset` that represents this `set.`

Equations
theorem set.finite.to_finset_eq_to_finset {α : Type u} {s : set α} [fintype s] (h : s.finite) :
@[simp]
theorem set.to_finite_to_finset {α : Type u} (s : set α) [fintype s] :
theorem set.finite.exists_finset {α : Type u} {s : set α} (h : s.finite) :
(s' : finset α), (a : α), a s' a s
theorem set.finite.exists_finset_coe {α : Type u} {s : set α} (h : s.finite) :
(s' : finset α), s' = s
@[protected, instance]

Finite sets can be lifted to finsets.

Equations
@[protected]
def set.infinite {α : Type u} (s : set α) :
Prop

A set is infinite if it is not finite.

This is protected so that it does not conflict with global `infinite`.

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

Alias of the reverse direction of `set.not_infinite`.

@[protected]
theorem set.finite_or_infinite {α : Type u} (s : set α) :

See also `finite_or_infinite`, `fintype_or_infinite`.

@[protected]
theorem set.infinite_or_finite {α : Type u} (s : set α) :

### Basic properties of `set.finite.to_finset`#

@[protected, simp]
theorem set.finite.mem_to_finset {α : Type u} {s : set α} {a : α} (h : s.finite) :
@[protected, simp]
theorem set.finite.coe_to_finset {α : Type u} {s : set α} (h : s.finite) :
@[protected, simp]
theorem set.finite.to_finset_nonempty {α : Type u} {s : set α} (h : s.finite) :
theorem set.finite.coe_sort_to_finset {α : Type u} {s : set α} (h : s.finite) :

Note that this is an equality of types not holding definitionally. Use wisely.

@[protected, simp]
theorem set.finite.to_finset_inj {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
@[simp]
theorem set.finite.to_finset_subset {α : Type u} {s : set α} {hs : s.finite} {t : finset α} :
@[simp]
theorem set.finite.to_finset_ssubset {α : Type u} {s : set α} {hs : s.finite} {t : finset α} :
@[simp]
theorem set.finite.subset_to_finset {α : Type u} {t : set α} {ht : t.finite} {s : finset α} :
@[simp]
theorem set.finite.ssubset_to_finset {α : Type u} {t : set α} {ht : t.finite} {s : finset α} :
@[protected]
theorem set.finite.to_finset_subset_to_finset {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
@[protected]
theorem set.finite.to_finset_ssubset_to_finset {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
@[protected]
theorem set.finite.to_finset_mono {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :

Alias of the reverse direction of `set.finite.to_finset_subset_to_finset`.

@[protected]
theorem set.finite.to_finset_strict_mono {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :

Alias of the reverse direction of `set.finite.to_finset_ssubset_to_finset`.

@[protected, simp]
theorem set.finite.to_finset_set_of {α : Type u} [fintype α] (p : α Prop) (h : {x : α | p x}.finite) :
@[simp]
theorem set.finite.disjoint_to_finset {α : Type u} {s t : set α} {hs : s.finite} {ht : t.finite} :
@[protected]
theorem set.finite.to_finset_inter {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s t).finite) :
@[protected]
theorem set.finite.to_finset_union {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s t).finite) :
@[protected]
theorem set.finite.to_finset_diff {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s \ t).finite) :
@[protected]
theorem set.finite.to_finset_symm_diff {α : Type u} {s t : set α} [decidable_eq α] (hs : s.finite) (ht : t.finite) (h : (s t).finite) :
@[protected]
theorem set.finite.to_finset_compl {α : Type u} {s : set α} [decidable_eq α] [fintype α] (hs : s.finite) (h : s.finite) :
@[protected, simp]
theorem set.finite.to_finset_empty {α : Type u} (h : .finite) :
@[protected, simp]
theorem set.finite.to_finset_univ {α : Type u} [fintype α] (h : set.univ.finite) :
@[protected, simp]
theorem set.finite.to_finset_eq_empty {α : Type u} {s : set α} {h : s.finite} :
s =
@[protected, simp]
theorem set.finite.to_finset_eq_univ {α : Type u} {s : set α} [fintype α] {h : s.finite} :
@[protected]
theorem set.finite.to_finset_image {α : Type u} {β : Type v} {s : set α} [decidable_eq β] (f : α β) (hs : s.finite) (h : (f '' s).finite) :
@[protected, simp]
theorem set.finite.to_finset_range {α : Type u} {β : Type v} [decidable_eq α] [fintype β] (f : β α) (h : (set.range f).finite) :

### Fintype instances #

Every instance here should have a corresponding `set.finite` constructor in the next section.

@[protected, instance]
def set.fintype_univ {α : Type u} [fintype α] :
Equations
noncomputable def set.fintype_of_finite_univ {α : Type u} (H : set.univ.finite) :

If `(set.univ : set α)` is finite then `α` is a finite type.

Equations
@[protected, instance]
def set.fintype_union {α : Type u} [decidable_eq α] (s t : set α) [fintype s] [fintype t] :
Equations
• = _
@[protected, instance]
def set.fintype_sep {α : Type u} (s : set α) (p : α Prop) [fintype s]  :
fintype {a ∈ s | p a}
Equations
@[protected, instance]
def set.fintype_inter {α : Type u} (s t : set α) [decidable_eq α] [fintype s] [fintype t] :
Equations
• = _
@[protected, instance]
def set.fintype_inter_of_left {α : Type u} (s t : set α) [fintype s] [decidable_pred (λ (_x : α), _x t)] :

A `fintype` instance for set intersection where the left set has a `fintype` instance.

Equations
@[protected, instance]
def set.fintype_inter_of_right {α : Type u} (s t : set α) [fintype t] [decidable_pred (λ (_x : α), _x s)] :

A `fintype` instance for set intersection where the right set has a `fintype` instance.

Equations
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
@[protected, instance]
def set.fintype_diff {α : Type u} [decidable_eq α] (s t : set α) [fintype s] [fintype t] :
Equations
@[protected, instance]
def set.fintype_diff_left {α : Type u} (s t : set α) [fintype s] [decidable_pred (λ (_x : α), _x t)] :
Equations
@[protected, instance]
def set.fintype_Union {α : Type u} {ι : Sort w} [decidable_eq α] [fintype (plift ι)] (f : ι set α) [Π (i : ι), fintype (f i)] :
fintype ( (i : ι), f i)
Equations
@[protected, instance]
def set.fintype_sUnion {α : Type u} [decidable_eq α] {s : set (set α)} [fintype s] [H : Π (t : s), ] :
Equations
def set.fintype_bUnion {α : Type u} [decidable_eq α] {ι : Type u_1} (s : set ι) [fintype s] (t : ι set α) (H : Π (i : ι), i s fintype (t i)) :
fintype ( (x : ι) (H : x s), t x)

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

Equations
@[protected, instance]
def set.fintype_bUnion' {α : Type u} [decidable_eq α] {ι : Type u_1} (s : set ι) [fintype s] (t : ι set α) [Π (i : ι), fintype (t i)] :
fintype ( (x : ι) (H : x s), t x)
Equations
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
@[protected, instance]
def set.fintype_bind' {α β : Type u_1} [decidable_eq β] (s : set α) [fintype s] (f : α set β) [H : Π (a : α), fintype (f a)] :
Equations
@[protected, instance]
def set.fintype_empty {α : Type u} :
Equations
@[protected, instance]
def set.fintype_singleton {α : Type u} (a : α) :
Equations
@[protected, instance]
def set.fintype_pure {α : Type u} (a : α) :
Equations
@[protected, instance]
def set.fintype_insert {α : Type u} (a : α) (s : set α) [decidable_eq α] [fintype s] :

A `fintype` instance for inserting an element into a `set` using the corresponding `insert` function on `finset`. This requires `decidable_eq α`. There is also `set.fintype_insert'` when `a ∈ s` is decidable.

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

A `fintype` structure on `insert a s` when inserting a new element.

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

A `fintype` structure on `insert a s` when inserting a pre-existing element.

Equations
@[protected, instance]
def set.fintype_insert' {α : Type u} (a : α) (s : set α) [decidable (a s)] [fintype s] :

The `set.fintype_insert` instance requires decidable equality, but when `a ∈ s` is decidable for this particular `a` we can still get a `fintype` instance by using `set.fintype_insert_of_not_mem` or `set.fintype_insert_of_mem`.

This instance pre-dates `set.fintype_insert`, and it is less efficient. When `decidable_mem_of_fintype` is made a local instance, then this instance would override `set.fintype_insert` if not for the fact that its priority has been adjusted. See Note [lower instance priority].

Equations
@[protected, instance]
def set.fintype_image {α : Type u} {β : Type v} [decidable_eq β] (s : set α) (f : α β) [fintype s] :
Equations
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
@[protected, instance]
def set.fintype_range {α : Type u} {ι : Sort w} [decidable_eq α] (f : ι α) [fintype (plift ι)] :
Equations
@[protected, instance]
def set.fintype_map {α β : Type u_1} [decidable_eq β] (s : set α) (f : α β) [fintype s] :
Equations
@[protected, instance]
def set.fintype_lt_nat (n : ) :
fintype {i : | i < n}
Equations
@[protected, instance]
def set.fintype_le_nat (n : ) :
fintype {i : | i n}
Equations

This is not an instance so that it does not conflict with the one in src/order/locally_finite.

Equations
@[protected, instance]
def set.fintype_prod {α : Type u} {β : Type v} (s : set α) (t : set β) [fintype s] [fintype t] :
Equations
@[protected, instance]
def set.fintype_off_diag {α : Type u} [decidable_eq α] (s : set α) [fintype s] :
Equations
@[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] :

`image2 f s t` is `fintype` if `s` and `t` are.

Equations
@[protected, instance]
def set.fintype_seq {α : Type u} {β : Type v} [decidable_eq β] (f : set β)) (s : set α) [fintype f] [fintype s] :
Equations
@[protected, instance]
def set.fintype_seq' {α β : Type u} [decidable_eq β] (f : set β)) (s : set α) [fintype f] [fintype s] :
Equations
@[protected, instance]
def set.fintype_mem_finset {α : Type u} (s : finset α) :
fintype {a : α | a s}
Equations
theorem equiv.set_finite_iff {α : Type u} {β : Type v} {s : set α} {t : set β} (hst : s t) :

### Finset #

@[simp]
theorem finset.finite_to_set {α : Type u} (s : finset α) :

Gives a `set.finite` for the `finset` coerced to a `set`. This is a wrapper around `set.to_finite`.

@[simp]
theorem finset.finite_to_set_to_finset {α : Type u} (s : finset α) :
@[simp]
theorem multiset.finite_to_set {α : Type u} (s : multiset α) :
{x : α | x s}.finite
@[simp]
theorem multiset.finite_to_set_to_finset {α : Type u} [decidable_eq α] (s : multiset α) :
@[simp]
theorem list.finite_to_set {α : Type u} (l : list α) :
{x : α | x l}.finite

### 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.

@[protected, instance]
def finite.set.finite_union {α : Type u} (s t : set α) [finite s] [finite t] :
@[protected, instance]
def finite.set.finite_sep {α : Type u} (s : set α) (p : α Prop) [finite s] :
finite {a ∈ s | p a}
@[protected]
theorem finite.set.subset {α : Type u} (s : set α) {t : set α} [finite s] (h : t s) :
@[protected, instance]
def finite.set.finite_inter_of_right {α : Type u} (s t : set α) [finite t] :
@[protected, instance]
def finite.set.finite_inter_of_left {α : Type u} (s t : set α) [finite s] :
@[protected, instance]
def finite.set.finite_diff {α : Type u} (s t : set α) [finite s] :
finite (s \ t)
@[protected, instance]
def finite.set.finite_range {α : Type u} {ι : Sort w} (f : ι α) [finite ι] :
@[protected, instance]
def finite.set.finite_Union {α : Type u} {ι : Sort w} [finite ι] (f : ι set α) [ (i : ι), finite (f i)] :
finite ( (i : ι), f i)
@[protected, instance]
def finite.set.finite_sUnion {α : Type u} {s : set (set α)} [finite s] [H : (t : s), ] :
theorem finite.set.finite_bUnion {α : Type u} {ι : Type u_1} (s : set ι) [finite s] (t : ι set α) (H : (i : ι), i s finite (t i)) :
finite ( (x : ι) (H : x s), t x)
@[protected, instance]
def finite.set.finite_bUnion' {α : Type u} {ι : Type u_1} (s : set ι) [finite s] (t : ι set α) [ (i : ι), finite (t i)] :
finite ( (x : ι) (H : x s), t x)
@[protected, instance]
def finite.set.finite_bUnion'' {α : Type u} {ι : Type u_1} (p : ι Prop) [h : finite {x : ι | p x}] (t : ι set α) [ (i : ι), finite (t i)] :
finite ( (x : ι) (h : p x), t x)

Example: `finite (⋃ (i < n), f i)` where `f : ℕ → set α` and `[∀ i, finite (f i)]` (when given instances from `data.nat.interval`).

@[protected, instance]
def finite.set.finite_Inter {α : Type u} {ι : Sort u_1} [nonempty ι] (t : ι set α) [ (i : ι), finite (t i)] :
finite ( (i : ι), t i)
@[protected, instance]
def finite.set.finite_insert {α : Type u} (a : α) (s : set α) [finite s] :
@[protected, instance]
def finite.set.finite_image {α : Type u} {β : Type v} (s : set α) (f : α β) [finite s] :
@[protected, instance]
def finite.set.finite_replacement {α : Type u} {β : Type v} [finite α] (f : α β) :
finite {_x : β | (x : α), f x = _x}
@[protected, instance]
def finite.set.finite_prod {α : Type u} {β : Type v} (s : set α) (t : set β) [finite s] [finite t] :
@[protected, instance]
def finite.set.finite_image2 {α : Type u} {β : Type v} {γ : Type x} (f : α β γ) (s : set α) (t : set β) [finite s] [finite t] :
finite s t)
@[protected, instance]
def finite.set.finite_seq {α : Type u} {β : Type v} (f : set β)) (s : set α) [finite f] [finite s] :

### 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.to_finite`, after possibly setting up some `fintype` and classical `decidable` instances.

theorem set.finite.of_subsingleton {α : Type u} [subsingleton α] (s : set α) :
theorem set.finite_univ {α : Type u} [finite α] :
theorem set.finite_univ_iff {α : Type u} :
theorem finite.of_finite_univ {α : Type u} :

Alias of the forward direction of `set.finite_univ_iff`.

theorem set.finite.union {α : Type u} {s t : set α} (hs : s.finite) (ht : t.finite) :
(s t).finite
theorem set.finite.finite_of_compl {α : Type u} {s : set α} (hs : s.finite) (hsc : s.finite) :
theorem set.finite.sup {α : Type u} {s t : set α} :
theorem set.finite.sep {α : Type u} {s : set α} (hs : s.finite) (p : α Prop) :
{a ∈ s | p a}.finite
theorem set.finite.inter_of_left {α : Type u} {s : set α} (hs : s.finite) (t : set α) :
(s t).finite
theorem set.finite.inter_of_right {α : Type u} {s : set α} (hs : s.finite) (t : set α) :
(t s).finite
theorem set.finite.inf_of_left {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(s t).finite
theorem set.finite.inf_of_right {α : Type u} {s : set α} (h : s.finite) (t : set α) :
(t s).finite
theorem set.finite.subset {α : Type u} {s : set α} (hs : s.finite) {t : set α} (ht : t s) :
theorem set.finite.diff {α : Type u} {s : set α} (hs : s.finite) (t : set α) :
(s \ t).finite
theorem set.finite.of_diff {α : Type u} {s t : set α} (hd : (s \ t).finite) (ht : t.finite) :
theorem set.finite_Union {α : Type u} {ι : Sort w} [finite ι] {f : ι set α} (H : (i : ι), (f i).finite) :
( (i : ι), f i).finite
theorem set.finite.sUnion {α : Type u} {s : set (set α)} (hs : s.finite) (H : (t : set α), t s t.finite) :
theorem set.finite.bUnion {α : Type u} {ι : Type u_1} {s : set ι} (hs : s.finite) {t : ι set α} (ht : (i : ι), i s (t i).finite) :
( (i : ι) (H : i s), t i).finite
theorem set.finite.bUnion' {α : Type u} {ι : Type u_1} {s : set ι} (hs : s.finite) {t : Π (i : ι), i s set α} (ht : (i : ι) (H : i s), (t i H).finite) :
( (i : ι) (H : i s), t i H).finite

Dependent version of `finite.bUnion`.

theorem set.finite.sInter {α : Type u_1} {s : set (set α)} {t : set α} (ht : t s) (hf : t.finite) :
theorem set.finite.Union {α : Type u} {ι : Type u_1} {s : ι set α} {t : set ι} (ht : t.finite) (hs : (i : ι), i t (s i).finite) (he : (i : ι), i t s i = ) :
( (i : ι), s i).finite

If sets `s i` are finite for all `i` from a finite set `t` and are empty for `i ∉ t`, then the union `⋃ i, s i` is a finite set.

theorem set.finite.bind {α β : Type u_1} {s : set α} {f : α set β} (h : s.finite) (hf : (a : α), a s (f a).finite) :
(s >>= f).finite
@[simp]
theorem set.finite_empty {α : Type u} :
@[protected]
theorem set.infinite.nonempty {α : Type u} {s : set α} (h : s.infinite) :
@[simp]
theorem set.finite_singleton {α : Type u} (a : α) :
{a}.finite
theorem set.finite_pure {α : Type u} (a : α) :
@[simp]
theorem set.finite.insert {α : Type u} (a : α) {s : set α} (hs : s.finite) :
s).finite
theorem set.finite.image {α : Type u} {β : Type v} {s : set α} (f : α β) (hs : s.finite) :
(f '' s).finite
theorem set.finite_range {α : Type u} {ι : Sort w} (f : ι α) [finite ι] :
theorem set.finite.dependent_image {α : Type u} {β : Type v} {s : set α} (hs : s.finite) (F : Π (i : α), i s β) :
{y : β | (x : α) (hx : x s), y = F x hx}.finite
theorem set.finite.map {α β : Type u_1} {s : set α} (f : α β) :
theorem set.finite.of_finite_image {α : Type u} {β : Type v} {s : set α} {f : α β} (h : (f '' s).finite) (hi : s) :
theorem set.finite_of_finite_preimage {α : Type u} {β : Type v} {f : α β} {s : set β} (h : (f ⁻¹' s).finite) (hs : s ) :
theorem set.finite.of_preimage {α : Type u} {β : Type v} {f : α β} {s : set β} (h : (f ⁻¹' s).finite) (hf : function.surjective f) :
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) :
theorem set.finite_lt_nat (n : ) :
{i : | i < n}.finite
theorem set.finite_le_nat (n : ) :
{i : | i n}.finite
@[protected]
theorem set.finite.prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
(s ×ˢ t).finite
theorem set.finite.of_prod_left {α : Type u} {β : Type v} {s : set α} {t : set β} (h : (s ×ˢ t).finite) :
theorem set.finite.of_prod_right {α : Type u} {β : Type v} {s : set α} {t : set β} (h : (s ×ˢ t).finite) :
@[protected]
theorem set.infinite.prod_left {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : s.infinite) (ht : t.nonempty) :
@[protected]
theorem set.infinite.prod_right {α : Type u} {β : Type v} {s : set α} {t : set β} (ht : t.infinite) (hs : s.nonempty) :
@[protected]
theorem set.infinite_prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
theorem set.finite_prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
(s ×ˢ t).finite (s.finite t = ) (t.finite s = )
@[protected]
theorem set.finite.off_diag {α : Type u} {s : set α} (hs : s.finite) :
@[protected]
theorem set.finite.image2 {α : Type u} {β : Type v} {γ : Type x} {s : set α} {t : set β} (f : α β γ) (hs : s.finite) (ht : t.finite) :
s t).finite
theorem set.finite.seq {α : Type u} {β : Type v} {f : set β)} {s : set α} (hf : f.finite) (hs : s.finite) :
(f.seq s).finite
theorem set.finite.seq' {α β : Type u} {f : set β)} {s : set α} (hf : f.finite) (hs : s.finite) :
(f <*> s).finite
theorem set.finite_mem_finset {α : Type u} (s : finset α) :
{a : α | a s}.finite
theorem set.subsingleton.finite {α : Type u} {s : set α} (h : s.subsingleton) :
theorem set.finite_preimage_inl_and_inr {α : Type u} {β : Type v} {s : set β)} :
theorem set.exists_finite_iff_finset {α : Type u} {p : set α Prop} :
( (s : set α), s.finite p s) (s : finset α), p s
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.finite.pi {δ : Type u_1} [finite δ] {κ : δ Type u_2} {t : Π (d : δ), set (κ d)} (ht : (d : δ), (t d).finite) :

Finite product of finite sets is finite

theorem set.union_finset_finite_of_range_finite {α : Type u} {β : Type v} (f : α ) (h : (set.range f).finite) :
( (a : α), (f a)).finite

A finite union of finsets is finite.

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

### Properties #

@[protected, instance]
def set.finite.inhabited {α : Type u} :
inhabited {s // s.finite}
Equations
@[simp]
theorem set.finite_union {α : Type u} {s t : set α} :
theorem set.finite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α β} (hi : s) :
@[simp]
theorem set.finite.to_finset_singleton {α : Type u} {a : α} (ha : {a}.finite := _) :
= {a}
@[simp]
theorem set.finite.to_finset_insert {α : Type u} [decidable_eq α] {s : set α} {a : α} (hs : s).finite) :
theorem set.finite.to_finset_insert' {α : Type u} [decidable_eq α] {a : α} {s : set α} (hs : s.finite) :
theorem set.finite.to_finset_prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
theorem set.finite.to_finset_off_diag {α : Type u} {s : set α} [decidable_eq α] (hs : s.finite) :
theorem set.finite.fin_embedding {α : Type u} {s : set α} (h : s.finite) :
(n : ) (f : fin n α), = s
theorem set.finite.fin_param {α : Type u} {s : set α} (h : s.finite) :
(n : ) (f : fin n α),
theorem set.finite_option {α : Type u} {s : set (option α)} :
s.finite {x : α | s}.finite
theorem set.finite_image_fst_and_snd_iff {α : Type u} {β : Type v} {s : set × β)} :
theorem set.forall_finite_image_eval_iff {δ : Type u_1} [finite δ] {κ : δ Type u_2} {s : set (Π (d : δ), κ d)} :
( (d : δ), '' s).finite) s.finite
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.finite.induction_on {α : Type u} {C : set α Prop} {s : set α} (h : s.finite) (H0 : C ) (H1 : {a : α} {s : set α}, a s s.finite C s C s)) :
C s
theorem set.finite.induction_on' {α : Type u} {C : set α Prop} {S : set α} (h : S.finite) (H0 : C ) (H1 : {a : α} {s : set α}, a S s S a s C s C s)) :
C S

Analogous to `finset.induction_on'`.

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 h C s) _) :
C s h
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.)

### Cardinality #

theorem set.empty_card {α : Type u} :
@[simp]
theorem set.empty_card' {α : Type u} {h : fintype } :
theorem set.card_fintype_insert_of_not_mem {α : 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 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 s f x = f y x = y) :
theorem set.card_image_of_injective {α : Type u} {β : Type v} (s : set α) [fintype s] {f : α β} [fintype (f '' s)] (H : function.injective f) :
@[simp]
theorem set.card_singleton {α : Type u} (a : α) :
= 1
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.card_range_of_injective {α : Type u} {β : Type v} [fintype α] {f : α β} (hf : function.injective f) [fintype (set.range f)] :
theorem set.finite.card_to_finset {α : Type u} {s : set α} [fintype s] (h : s.finite) :
theorem set.card_ne_eq {α : Type u} [fintype α] (a : α) [fintype {x : α | x a}] :
fintype.card {x : α | x a} =

### Infinite sets #

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 α} :

Alias of the reverse direction of `set.infinite_coe_iff`.

noncomputable 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
theorem set.infinite_of_finite_compl {α : Type u} [infinite α] {s : set α} (hs : s.finite) :
theorem set.finite.infinite_compl {α : Type u} [infinite α] {s : set α} (hs : s.finite) :
@[protected]
theorem set.infinite.mono {α : Type u} {s t : set α} (h : s t) :
theorem set.infinite.diff {α : Type u} {s t : set α} (hs : s.infinite) (ht : t.finite) :
(s \ t).infinite
@[simp]
theorem set.infinite_union {α : Type u} {s t : set α} :
theorem set.infinite.of_image {α : Type u} {β : Type v} (f : α β) {s : set α} (hs : (f '' s).infinite) :
theorem set.infinite_image_iff {α : Type u} {β : Type v} {s : set α} {f : α β} (hi : s) :
@[protected]
theorem set.infinite.image {α : Type u} {β : Type v} {s : set α} {f : α β} (hi : s) :

Alias of the reverse direction of `set.infinite_image_iff`.

@[protected]
theorem set.infinite.image2_left {α : Type u} {β : Type v} {γ : Type x} {f : α β γ} {s : set α} {t : set β} {b : β} (hs : s.infinite) (hb : b t) (hf : set.inj_on (λ (a : α), f a b) s) :
s t).infinite
@[protected]
theorem set.infinite.image2_right {α : Type u} {β : Type v} {γ : Type x} {f : α β γ} {s : set α} {t : set β} {a : α} (ht : t.infinite) (ha : a s) (hf : set.inj_on (f a) t) :
s t).infinite
theorem set.infinite_image2 {α : Type u} {β : Type v} {γ : Type x} {f : α β γ} {s : set α} {t : set β} (hfs : (b : β), b t set.inj_on (λ (a : α), f a b) s) (hft : (a : α), a s set.inj_on (f a) t) :
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.exists_ne_map_eq_of_maps_to {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α β} (hs : s.infinite) (hf : s t) (ht : t.finite) :
(x : α) (H : x s) (y : α) (H : y s), x y f x = f y
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.infinite.exists_not_mem_finset {α : Type u} {s : set α} (hs : s.infinite) (f : finset α) :
(a : α) (H : a s), a f
theorem set.not_inj_on_infinite_finite_image {α : Type u} {β : Type v} {f : α β} {s : set α} (h_inf : s.infinite) (h_fin : (f '' s).finite) :
¬ s

### Order properties #

theorem set.infinite_of_forall_exists_gt {α : Type u} [preorder α] [nonempty α] {s : set α} (h : (a : α), (b : α) (H : b s), a < b) :
theorem set.infinite_of_forall_exists_lt {α : Type u} [preorder α] [nonempty α] {s : set α} (h : (a : α), (b : α) (H : b s), b < a) :
theorem set.finite_is_top (α : Type u_1)  :
{x : α | is_top x}.finite
theorem set.finite_is_bot (α : Type u_1)  :
{x : α | is_bot x}.finite
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 : s t) (ht : t.finite) :
(x : α) (H : x s) (y : α) (H : y s), x < y f x = f y
theorem set.finite.exists_lt_map_eq_of_forall_mem {α : Type u} {β : Type v} [linear_order α] [infinite α] {t : set β} {f : α β} (hf : (a : α), f a t) (ht : t.finite) :
(a b : α), a < b f a = f b
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 s f 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 s f b f a)
theorem set.exists_lower_bound_image {α : Type u} {β : Type v} [hα : nonempty α] [linear_order β] (s : set α) (f : α β) (h : s.finite) :
(a : α), (b : α), b s f a f b
theorem set.exists_upper_bound_image {α : Type u} {β : Type v} [hα : nonempty α] [linear_order β] (s : set α) (f : α β) (h : s.finite) :
(a : α), (b : α), b s f b f a
theorem set.finite.supr_binfi_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] [ has_le.le] [order.frame α] {s : set ι} (hs : s.finite) {f : ι ι' α} (hf : (i : ι), i s monotone (f i)) :
( (j : ι'), (i : ι) (H : i s), f i j) = (i : ι) (H : i s), (j : ι'), f i j
theorem set.finite.supr_binfi_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] [order.frame α] {s : set ι} (hs : s.finite) {f : ι ι' α} (hf : (i : ι), i s antitone (f i)) :
( (j : ι'), (i : ι) (H : i s), f i j) = (i : ι) (H : i s), (j : ι'), f i j
theorem set.finite.infi_bsupr_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] {s : set ι} (hs : s.finite) {f : ι ι' α} (hf : (i : ι), i s monotone (f i)) :
( (j : ι'), (i : ι) (H : i s), f i j) = (i : ι) (H : i s), (j : ι'), f i j
theorem set.finite.infi_bsupr_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [preorder ι'] [nonempty ι'] [ has_le.le] {s : set ι} (hs : s.finite) {f : ι ι' α} (hf : (i : ι), i s antitone (f i)) :
( (j : ι'), (i : ι) (H : i s), f i j) = (i : ι) (H : i s), (j : ι'), f i j
theorem supr_infi_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] [ has_le.le] [order.frame α] {f : ι ι' α} (hf : (i : ι), monotone (f i)) :
( (j : ι'), (i : ι), f i j) = (i : ι), (j : ι'), f i j
theorem supr_infi_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] [order.frame α] {f : ι ι' α} (hf : (i : ι), antitone (f i)) :
( (j : ι'), (i : ι), f i j) = (i : ι), (j : ι'), f i j
theorem infi_supr_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] {f : ι ι' α} (hf : (i : ι), monotone (f i)) :
( (j : ι'), (i : ι), f i j) = (i : ι), (j : ι'), f i j
theorem infi_supr_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [nonempty ι'] [ has_le.le] {f : ι ι' α} (hf : (i : ι), antitone (f i)) :
( (j : ι'), (i : ι), f i j) = (i : ι), (j : ι'), f i j
theorem set.Union_Inter_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [ has_le.le] [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.Union_Inter_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [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.Inter_Union_of_monotone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [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.Inter_Union_of_antitone {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [finite ι] [preorder ι'] [ has_le.le] [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.Union_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [linear_order ι'] [nonempty ι'] {α : ι Type u_3} {I : set ι} {s : Π (i : ι), ι' set (α i)} (hI : I.finite) (hs : (i : ι), i I monotone (s i)) :
( (j : ι'), I.pi (λ (i : ι), s i j)) = I.pi (λ (i : ι), (j : ι'), s i j)
theorem set.Union_univ_pi_of_monotone {ι : Type u_1} {ι' : Type u_2} [linear_order ι'] [nonempty ι'] [finite ι] {α : ι Type u_3} {s : Π (i : ι), ι' set (α i)} (hs : (i : ι), monotone (s i)) :
( (j : ι'), set.univ.pi (λ (i : ι), s i j)) = set.univ.pi (λ (i : ι), (j : ι'), s i j)
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.finite.exists_maximal_wrt {α : Type u} {β : Type v} (f : α β) (s : set α) (h : s.finite) :
s.nonempty ( (a : α) (H : a s), (a' : α), a' s f a f a' f a = f a')
@[protected]
theorem set.finite.bdd_above {α : Type u} [preorder α] [nonempty α] {s : set α} (hs : s.finite) :

A finite set is bounded above.

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

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

theorem set.infinite_of_not_bdd_above {α : Type u} [preorder α] [nonempty α] {s : set α} :
@[protected]
theorem set.finite.bdd_below {α : Type u} [preorder α] [ ge] [nonempty α] {s : set α} (hs : s.finite) :

A finite set is bounded below.

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

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

theorem set.infinite_of_not_bdd_below {α : Type u} [preorder α] [ ge] [nonempty α] {s : set α} :
@[protected]
theorem finset.bdd_above {α : Type u} [nonempty α] (s : finset α) :

A finset is bounded above.

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

A finset is bounded below.

theorem finite.of_forall_not_lt_lt {α : Type u} [linear_order α] (h : ⦃x y z : α⦄, x < y y < z false) :

If a linear order does not contain any triple of elements `x < y < z`, then this type is finite.

theorem set.finite_of_forall_not_lt_lt {α : Type u} [linear_order α] {s : set α} (h : (x : α), x s (y : α), y s (z : α), z s x < y y < z false) :

If a set `s` does not contain any triple of elements `x < y < z`, then `s` is finite.

theorem set.finite_diff_Union_Ioo {α : Type u} [linear_order α] (s : set α) :
(s \ (x : α) (H : x s) (y : α) (H : y s), y).finite
theorem set.finite_diff_Union_Ioo' {α : Type u} [linear_order α] (s : set α) :
(s \ (x : s × s), set.Ioo (x.fst) (x.snd)).finite