Documentation

Mathlib.Data.Set.Finite.Basic

Finite sets #

This file provides Fintype instances for many set constructions. It also proves basic facts about finite sets and gives ways to manipulate Set.Finite expressions.

Note that the instances in this file are selected somewhat arbitrarily on the basis of them not needing any imports beyond Data.Fintype.Card (which is required by Finite.ofFinset); they can certainly be organized better.

Main definitions #

Set.Finite.toFinset to noncomputably produce a Finset from a Set.Finite proof. (See Set.toFinset for a computable version.)

Implementation #

A finite set is defined to be a set whose coercion to a type has a Finite instance.

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

theorem Set.finite_def {α : Type u} {s : Set α} :

s.Finite ↔ Nonempty (Fintype ↑s)

theorem Set.Finite.nonempty_fintype {α : Type u} {s : Set α} :

s.Finite → Nonempty (Fintype ↑s)

Alias of the forward direction of Set.finite_def.

theorem Set.Finite.ofFinset {α : Type u} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :

p.Finite

Construct a Finite instance for a Set from a Finset with the same elements.

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

h.fintype = ⋯.some

noncomputable def Set.Finite.toFinset {α : Type u} {s : Set α} (h : s.Finite) :

Using choice, get the Finset that represents this Set.

Equations

h.toFinset = s.toFinset

theorem Set.Finite.toFinset_eq_toFinset {α : Type u} {s : Set α} [Fintype ↑s] (h : s.Finite) :

h.toFinset = s.toFinset

@[simp]

theorem Set.toFinite_toFinset {α : Type u} (s : Set α) [Fintype ↑s] :

⋯.toFinset = s.toFinset

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

instance Set.instCanLiftFinsetToSetFinite {α : Type u} :

CanLift (Set α) (Finset α) Finset.toSet Set.Finite

Finite sets can be lifted to finsets.

Basic properties of `Set.Finite.toFinset` #

@[simp]

theorem Set.Finite.mem_toFinset {α : Type u} {s : Set α} {a : α} (hs : s.Finite) :

a ∈ hs.toFinset ↔ a ∈ s

@[simp]

theorem Set.Finite.coe_toFinset {α : Type u} {s : Set α} (hs : s.Finite) :

↑hs.toFinset = s

@[simp]

theorem Set.Finite.toFinset_nonempty {α : Type u} {s : Set α} (hs : s.Finite) :

hs.toFinset.Nonempty ↔ s.Nonempty

theorem Set.Finite.coeSort_toFinset {α : Type u} {s : Set α} (hs : s.Finite) :

{ x : α // x ∈ hs.toFinset } = ↑s

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

def Set.Finite.subtypeEquivToFinset {α : Type u} {s : Set α} (hs : s.Finite) :

{ x : α // x ∈ s } ≃ { x : α // x ∈ hs.toFinset }

The identity map, bundled as an equivalence between the subtypes of s : Set α and of h.toFinset : Finset α, where h is a proof of finiteness of s.

Equations

hs.subtypeEquivToFinset = (Equiv.refl α).subtypeEquiv ⋯

@[simp]

theorem Set.Finite.subtypeEquivToFinset_apply_coe {α : Type u} {s : Set α} (hs : s.Finite) (a : { a : α // a ∈ s }) :

↑(hs.subtypeEquivToFinset a) = ↑a

@[simp]

theorem Set.Finite.subtypeEquivToFinset_symm_apply_coe {α : Type u} {s : Set α} (hs : s.Finite) (b : { b : α // b ∈ hs.toFinset }) :

↑(hs.subtypeEquivToFinset.symm b) = ↑b

@[simp]

theorem Set.Finite.toFinset_inj {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} :

hs.toFinset = ht.toFinset ↔ s = t

@[simp]

theorem Set.Finite.toFinset_subset {α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α} :

hs.toFinset ⊆ t ↔ s ⊆ ↑t

@[simp]

theorem Set.Finite.toFinset_ssubset {α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α} :

hs.toFinset ⊂ t ↔ s ⊂ ↑t

@[simp]

theorem Set.Finite.subset_toFinset {α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α} :

s ⊆ ht.toFinset ↔ ↑s ⊆ t

@[simp]

theorem Set.Finite.ssubset_toFinset {α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α} :

s ⊂ ht.toFinset ↔ ↑s ⊂ t

theorem Set.Finite.toFinset_subset_toFinset {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} :

hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t

theorem Set.Finite.toFinset_ssubset_toFinset {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} :

hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t

theorem Set.Finite.toFinset_mono {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} :

s ⊆ t → hs.toFinset ⊆ ht.toFinset

Alias of the reverse direction of Set.Finite.toFinset_subset_toFinset.

theorem Set.Finite.toFinset_strictMono {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} :

s ⊂ t → hs.toFinset ⊂ ht.toFinset

Alias of the reverse direction of Set.Finite.toFinset_ssubset_toFinset.

@[simp]

theorem Set.Finite.toFinset_setOf {α : Type u} [Fintype α] (p : α → Prop) [DecidablePred p] (h : {x : α | p x}.Finite) :

h.toFinset = Finset.filter p Finset.univ

@[simp]

theorem Set.Finite.disjoint_toFinset {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} :

Disjoint hs.toFinset ht.toFinset ↔ Disjoint s t

theorem Set.Finite.toFinset_inter {α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∩ t).Finite) :

h.toFinset = hs.toFinset ∩ ht.toFinset

theorem Set.Finite.toFinset_union {α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∪ t).Finite) :

h.toFinset = hs.toFinset ∪ ht.toFinset

theorem Set.Finite.toFinset_diff {α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s \ t).Finite) :

h.toFinset = hs.toFinset \ ht.toFinset

theorem Set.Finite.toFinset_symmDiff {α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (_root_.symmDiff s t).Finite) :

h.toFinset = _root_.symmDiff hs.toFinset ht.toFinset

theorem Set.Finite.toFinset_compl {α : Type u} {s : Set α} [DecidableEq α] [Fintype α] (hs : s.Finite) (h : sᶜ.Finite) :

h.toFinset = hs.toFinsetᶜ

theorem Set.Finite.toFinset_univ {α : Type u} [Fintype α] (h : univ.Finite) :

h.toFinset = Finset.univ

@[simp]

theorem Set.Finite.toFinset_eq_empty {α : Type u} {s : Set α} {h : s.Finite} :

h.toFinset = ∅ ↔ s = ∅

theorem Set.Finite.toFinset_empty {α : Type u} (h : ∅.Finite) :

h.toFinset = ∅

@[simp]

theorem Set.Finite.toFinset_eq_univ {α : Type u} {s : Set α} [Fintype α] {h : s.Finite} :

h.toFinset = Finset.univ ↔ s = univ

theorem Set.Finite.toFinset_image {α : Type u} {β : Type v} {s : Set α} [DecidableEq β] (f : α → β) (hs : s.Finite) (h : (f '' s).Finite) :

h.toFinset = Finset.image f hs.toFinset

theorem Set.Finite.toFinset_range {α : Type u} {β : Type v} [DecidableEq α] [Fintype β] (f : β → α) (h : (range f).Finite) :

h.toFinset = Finset.image f Finset.univ

Fintype instances #

Every instance here should have a corresponding Set.Finite constructor in the next section.

instance Set.fintypeUniv {α : Type u} [Fintype α] :

Fintype ↑univ

Equations

Set.fintypeUniv = Fintype.ofEquiv α (Equiv.Set.univ α).symm

instance Set.fintypeTop {α : Type u} [Fintype α] :

Equations

Set.fintypeTop = inferInstanceAs (Fintype ↑Set.univ)

noncomputable def Set.fintypeOfFiniteUniv {α : Type u} (H : univ.Finite) :

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

Equations

Set.fintypeOfFiniteUniv H = Fintype.ofEquiv (↑Set.univ) (Equiv.Set.univ α)

instance Set.fintypeUnion {α : Type u} [DecidableEq α] (s t : Set α) [Fintype ↑s] [Fintype ↑t] :

Fintype ↑(s ∪ t)

Equations

s.fintypeUnion t = Fintype.ofFinset (s.toFinset ∪ t.toFinset) ⋯

instance Set.fintypeSep {α : Type u} (s : Set α) (p : α → Prop) [Fintype ↑s] [DecidablePred p] :

Fintype ↑{a : α | a ∈ s ∧ p a}

Equations

s.fintypeSep p = Fintype.ofFinset (Finset.filter p s.toFinset) ⋯

instance Set.fintypeInter {α : Type u} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] :

Fintype ↑(s ∩ t)

Equations

s.fintypeInter t = Fintype.ofFinset (s.toFinset ∩ t.toFinset) ⋯

instance Set.fintypeInterOfLeft {α : Type u} (s t : Set α) [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ t] :

Fintype ↑(s ∩ t)

A Fintype instance for set intersection where the left set has a Fintype instance.

Equations

s.fintypeInterOfLeft t = Fintype.ofFinset (Finset.filter (fun (x : α) => x ∈ t) s.toFinset) ⋯

instance Set.fintypeInterOfRight {α : Type u} (s t : Set α) [Fintype ↑t] [DecidablePred fun (x : α) => x ∈ s] :

Fintype ↑(s ∩ t)

A Fintype instance for set intersection where the right set has a Fintype instance.

Equations

s.fintypeInterOfRight t = Fintype.ofFinset (Finset.filter (fun (x : α) => x ∈ s) t.toFinset) ⋯

def Set.fintypeSubset {α : Type u} (s : Set α) {t : Set α} [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ t] (h : t ⊆ s) :

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

Equations

s.fintypeSubset h = ⋯.mpr (s.fintypeInterOfLeft t)

instance Set.fintypeDiff {α : Type u} [DecidableEq α] (s t : Set α) [Fintype ↑s] [Fintype ↑t] :

Fintype ↑(s \ t)

Equations

s.fintypeDiff t = Fintype.ofFinset (s.toFinset \ t.toFinset) ⋯

instance Set.fintypeDiffLeft {α : Type u} (s t : Set α) [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ t] :

Fintype ↑(s \ t)

Equations

s.fintypeDiffLeft t = s.fintypeSep fun (x : α) => x ∈ tᶜ

def Set.fintypeBiUnion {α : Type u} [DecidableEq α] {ι : Type u_1} (s : Set ι) [Fintype ↑s] (t : ι → Set α) (H : (i : ι) → i ∈ s → Fintype ↑(t i)) :

Fintype ↑(⋃ x ∈ s, t x)

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

Equations

s.fintypeBiUnion t H = Fintype.ofFinset (s.toFinset.attach.biUnion fun (x : { x : ι // x ∈ s.toFinset }) => (t ↑x).toFinset) ⋯

instance Set.fintypeBiUnion' {α : Type u} [DecidableEq α] {ι : Type u_1} (s : Set ι) [Fintype ↑s] (t : ι → Set α) [(i : ι) → Fintype ↑(t i)] :

Fintype ↑(⋃ x ∈ s, t x)

Equations

s.fintypeBiUnion' t = Fintype.ofFinset (s.toFinset.biUnion fun (x : ι) => (t x).toFinset) ⋯

instance Set.fintypeEmpty {α : Type u} :

Equations

Set.fintypeEmpty = Fintype.ofFinset ∅ ⋯

instance Set.fintypeSingleton {α : Type u} (a : α) :

Fintype ↑{a}

Equations

Set.fintypeSingleton a = Fintype.ofFinset {a} ⋯

instance Set.fintypeInsert {α : Type u} (a : α) (s : Set α) [DecidableEq α] [Fintype ↑s] :

Fintype ↑(insert a s)

A Fintype instance for inserting an element into a Set using the corresponding insert function on Finset. This requires DecidableEq α. There is also Set.fintypeInsert' when a ∈ s is decidable.

Equations

Set.fintypeInsert a s = Fintype.ofFinset (insert a s.toFinset) ⋯

def Set.fintypeInsertOfNotMem {α : Type u} {a : α} (s : Set α) [Fintype ↑s] (h : a ∉ s) :

Fintype ↑(insert a s)

A Fintype structure on insert a s when inserting a new element.

Equations

s.fintypeInsertOfNotMem h = Fintype.ofFinset { val := a ::ₘ s.toFinset.val, nodup := ⋯ } ⋯

def Set.fintypeInsertOfMem {α : Type u} {a : α} (s : Set α) [Fintype ↑s] (h : a ∈ s) :

Fintype ↑(insert a s)

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

Equations

s.fintypeInsertOfMem h = Fintype.ofFinset s.toFinset ⋯

@[instance 100]

instance Set.fintypeInsert' {α : Type u} (a : α) (s : Set α) [Decidable (a ∈ s)] [Fintype ↑s] :

Fintype ↑(insert a s)

The Set.fintypeInsert instance requires decidable equality, but when a ∈ s is decidable for this particular a we can still get a Fintype instance by using Set.fintypeInsertOfNotMem or Set.fintypeInsertOfMem.

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

Equations

Set.fintypeInsert' a s = if h : a ∈ s then s.fintypeInsertOfMem h else s.fintypeInsertOfNotMem h

instance Set.fintypeImage {α : Type u} {β : Type v} [DecidableEq β] (s : Set α) (f : α → β) [Fintype ↑s] :

Fintype ↑(f '' s)

Equations

s.fintypeImage f = Fintype.ofFinset (Finset.image f s.toFinset) ⋯

def Set.fintypeOfFintypeImage {α : Type u} {β : Type v} (s : Set α) {f : α → β} {g : β → Option α} (I : Function.IsPartialInv f g) [Fintype ↑(f '' s)] :

If a function f has a partial inverse g and the image of s under f is a set with a Fintype instance, then s has a Fintype structure as well.

Equations

s.fintypeOfFintypeImage I = Fintype.ofFinset { val := Multiset.filterMap g (f '' s).toFinset.val, nodup := ⋯ } ⋯

instance Set.fintypeMap {α β : Type u_1} [DecidableEq β] (s : Set α) (f : α → β) [Fintype ↑s] :

Fintype ↑(f <$> s)

Equations

Set.fintypeMap = Set.fintypeImage

instance Set.fintypeLTNat (n : ℕ) :

Fintype ↑{i : ℕ | i < n}

Equations

Set.fintypeLTNat n = Fintype.ofFinset (Finset.range n) ⋯

instance Set.fintypeLENat (n : ℕ) :

Fintype ↑{i : ℕ | i ≤ n}

Equations

Set.fintypeLENat n = id (⋯.mp (Set.fintypeLTNat (n + 1)))

def Set.Nat.fintypeIio (n : ℕ) :

Fintype ↑(Iio n)

This is not an instance so that it does not conflict with the one in Mathlib/Order/LocallyFinite.lean.

Equations

Set.Nat.fintypeIio n = Set.fintypeLTNat n

instance Set.fintypeMemFinset {α : Type u} (s : Finset α) :

Fintype ↑{a : α | a ∈ s}

Equations

Set.fintypeMemFinset s = s.fintypeCoeSort

Finset #

@[simp]

theorem Finset.finite_toSet {α : Type u} (s : Finset α) :

(↑s).Finite

Gives a Set.Finite for the Finset coerced to a Set. This is a wrapper around Set.toFinite.

theorem Finset.finite_toSet_toFinset {α : Type u} (s : Finset α) :

⋯.toFinset = s

@[simp]

theorem Multiset.finite_toSet {α : Type u} (s : Multiset α) :

{x : α | x ∈ s}.Finite

@[simp]

theorem Multiset.finite_toSet_toFinset {α : Type u} [DecidableEq α] (s : Multiset α) :

⋯.toFinset = s.toFinset

@[simp]

theorem List.finite_toSet {α : 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.

instance Finite.Set.finite_union {α : Type u} (s t : Set α) [Finite ↑s] [Finite ↑t] :

Finite ↑(s ∪ t)

instance Finite.Set.finite_sep {α : Type u} (s : Set α) (p : α → Prop) [Finite ↑s] :

Finite ↑{a : α | a ∈ s ∧ p a}

theorem Finite.Set.subset {α : Type u} (s : Set α) {t : Set α} [Finite ↑s] (h : t ⊆ s) :

instance Finite.Set.finite_inter_of_right {α : Type u} (s t : Set α) [Finite ↑t] :

Finite ↑(s ∩ t)

instance Finite.Set.finite_inter_of_left {α : Type u} (s t : Set α) [Finite ↑s] :

Finite ↑(s ∩ t)

instance Finite.Set.finite_diff {α : Type u} (s t : Set α) [Finite ↑s] :

Finite ↑(s \ t)

instance Finite.Set.finite_insert {α : Type u} (a : α) (s : Set α) [Finite ↑s] :

Finite ↑(insert a s)

instance Finite.Set.finite_image {α : Type u} {β : Type v} (s : Set α) (f : α → β) [Finite ↑s] :

Finite ↑(f '' 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.toFinite, after possibly setting up some Fintype and classical Decidable instances.

theorem Set.Finite.of_subsingleton {α : Type u} [Subsingleton α] (s : Set α) :

s.Finite

theorem Set.finite_univ {α : Type u} [Finite α] :

univ.Finite

theorem Set.finite_univ_iff {α : Type u} :

univ.Finite ↔ Finite α

theorem Finite.of_finite_univ {α : Type u} :

Set.univ.Finite → Finite α

Alias of the forward direction of Set.finite_univ_iff.

theorem Set.Finite.subset {α : Type u} {s : Set α} (hs : s.Finite) {t : Set α} (ht : t ⊆ s) :

t.Finite

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

s.Finite → t.Finite → (s ⊔ t).Finite

theorem Set.Finite.sep {α : Type u} {s : Set α} (hs : s.Finite) (p : α → Prop) :

{a : α | 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.Infinite.mono {α : Type u} {s t : Set α} (h : s ⊆ t) :

s.Infinite → t.Infinite

theorem Set.Finite.diff {α : Type u} {s t : Set α} (hs : s.Finite) :

(s \ t).Finite

theorem Set.Finite.of_diff {α : Type u} {s t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) :

s.Finite

theorem Set.Finite.symmDiff {α : Type u} {s t : Set α} (hs : s.Finite) (ht : t.Finite) :

(_root_.symmDiff s t).Finite

theorem Set.Finite.symmDiff_congr {α : Type u} {s t u : Set α} (hst : (_root_.symmDiff s t).Finite) :

(_root_.symmDiff s u).Finite ↔ (_root_.symmDiff t u).Finite

@[simp]

theorem Set.finite_empty {α : Type u} :

∅.Finite

theorem Set.Infinite.nonempty {α : Type u} {s : Set α} (h : s.Infinite) :

s.Nonempty

@[simp]

theorem Set.finite_singleton {α : Type u} (a : α) :

{a}.Finite

@[simp]

theorem Set.Finite.insert {α : Type u} (a : α) {s : Set α} (hs : s.Finite) :

(insert a s).Finite

theorem Set.Finite.image {α : Type u} {β : Type v} {s : Set α} (f : α → β) (hs : s.Finite) :

(f '' s).Finite

theorem Set.Finite.of_surjOn {α : Type u} {β : Type v} {s : Set α} {t : Set β} (f : α → β) (hf : SurjOn f s t) (hs : s.Finite) :

t.Finite

theorem Set.Finite.map {α β : Type u_1} {s : Set α} (f : α → β) :

s.Finite → (f <$> s).Finite

theorem Set.Finite.of_finite_image {α : Type u} {β : Type v} {s : Set α} {f : α → β} (h : (f '' s).Finite) (hi : InjOn f s) :

s.Finite

theorem Set.finite_of_finite_preimage {α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : (f ⁻¹' s).Finite) (hs : s ⊆ range f) :

s.Finite

theorem Set.Finite.of_preimage {α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : (f ⁻¹' s).Finite) (hf : Function.Surjective f) :

s.Finite

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

(f ⁻¹' s).Finite

theorem Set.Infinite.preimage {α : Type u} {β : Type v} {f : α → β} {s : Set β} (hs : s.Infinite) (hf : s ⊆ range f) :

(f ⁻¹' s).Infinite

theorem Set.Infinite.preimage' {α : Type u} {β : Type v} {f : α → β} {s : Set β} (hs : (s ∩ range f).Infinite) :

(f ⁻¹' s).Infinite

theorem Set.Finite.preimage_embedding {α : Type u} {β : Type v} {s : Set β} (f : α ↪ β) (h : s.Finite) :

(⇑f ⁻¹' s).Finite

theorem Set.finite_lt_nat (n : ℕ) :

{i : ℕ | i < n}.Finite

theorem Set.finite_le_nat (n : ℕ) :

{i : ℕ | i ≤ n}.Finite

theorem Set.Finite.surjOn_iff_bijOn_of_mapsTo {α : Type u} {s : Set α} {f : α → α} (hs : s.Finite) (hm : MapsTo f s s) :

SurjOn f s s ↔ BijOn f s s

theorem Set.Finite.injOn_iff_bijOn_of_mapsTo {α : Type u} {s : Set α} {f : α → α} (hs : s.Finite) (hm : MapsTo f s s) :

InjOn f s ↔ BijOn f s s

theorem Set.finite_mem_finset {α : Type u} (s : Finset α) :

{a : α | a ∈ s}.Finite

theorem Set.Subsingleton.finite {α : Type u} {s : Set α} (h : s.Subsingleton) :

s.Finite

theorem Set.Infinite.nontrivial {α : Type u} {s : Set α} (hs : s.Infinite) :

s.Nontrivial

theorem Set.finite_preimage_inl_and_inr {α : Type u} {β : Type v} {s : Set (α ⊕ β)} :

(Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite

theorem Set.exists_finite_iff_finset {α : Type u} {p : Set α → Prop} :

(∃ (s : Set α), s.Finite ∧ p s) ↔ ∃ (s : Finset α), p ↑s

theorem Set.exists_subset_image_finite_and {α : Type u} {β : Type v} {f : α → β} {s : Set α} {p : Set β → Prop} :

(∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

theorem Set.finite_range_ite {α : Type u} {β : Type v} {p : α → Prop} [DecidablePred p] {f g : α → β} (hf : (range f).Finite) (hg : (range g).Finite) :

(range fun (x : α) => if p x then f x else g x).Finite

theorem Set.finite_range_const {α : Type u} {β : Type v} {c : β} :

(range fun (x : α) => c).Finite

Properties #

instance Set.Finite.inhabited {α : Type u} :

Inhabited { s : Set α // s.Finite }

Equations

Set.Finite.inhabited = { default := ⟨∅, ⋯⟩ }

@[simp]

theorem Set.finite_union {α : Type u} {s t : Set α} :

(s ∪ t).Finite ↔ s.Finite ∧ t.Finite

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

(f '' s).Finite ↔ s.Finite

theorem Set.univ_finite_iff_nonempty_fintype {α : Type u} :

univ.Finite ↔ Nonempty (Fintype α)

theorem Set.Finite.toFinset_singleton {α : Type u} {a : α} (ha : {a}.Finite := ⋯) :

Finite.toFinset ha = {a}

@[simp]

theorem Set.Finite.toFinset_insert {α : Type u} [DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite) :

hs.toFinset = insert a ⋯.toFinset

theorem Set.Finite.toFinset_insert' {α : Type u} [DecidableEq α] {a : α} {s : Set α} (hs : s.Finite) :

⋯.toFinset = insert a hs.toFinset

theorem Set.finite_option {α : Type u} {s : Set (Option α)} :

s.Finite ↔ {x : α | some x ∈ s}.Finite

theorem Set.Finite.induction_on {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ ⋯) (insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (insert a s) ⋯) :

motive s hs

Induction principle for finite sets: To prove a property motive of a finite set s, it's enough to prove for the empty set and to prove that motive t → motive ({a} ∪ t) for all t.

See also Set.Finite.induction_on for the version requiring to check motive t → motive ({a} ∪ t) only for t ⊆ s.

theorem Set.Finite.induction_on_subset {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ ⋯) (insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (insert a t) ⋯) :

motive s hs

Induction principle for finite sets: To prove a property C of a finite set s, it's enough to prove for the empty set and to prove that C t → C ({a} ∪ t) for all t ⊆ s.

This is analogous to Finset.induction_on'. See also Set.Finite.induction_on for the version requiring C t → C ({a} ∪ t) for all t.

@[deprecated Set.Finite.induction_on_subset (since := "2025-01-03")]

theorem Set.Finite.induction_on' {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ ⋯) (insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (insert a t) ⋯) :

motive s hs

Alias of Set.Finite.induction_on_subset.

Induction principle for finite sets: To prove a property C of a finite set s, it's enough to prove for the empty set and to prove that C t → C ({a} ∪ t) for all t ⊆ s.

This is analogous to Finset.induction_on'. See also Set.Finite.induction_on for the version requiring C t → C ({a} ∪ t) for all t.

@[deprecated Set.Finite.induction_on (since := "2025-01-03")]

theorem Set.Finite.dinduction_on {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ ⋯) (insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (insert a s) ⋯) :

motive s hs

Alias of Set.Finite.induction_on.

Induction principle for finite sets: To prove a property motive of a finite set s, it's enough to prove for the empty set and to prove that motive t → motive ({a} ∪ t) for all t.

See also Set.Finite.induction_on for the version requiring to check motive t → motive ({a} ∪ t) only for t ⊆ s.

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

Fintype.card ↑∅ = 0

theorem Set.empty_card' {α : Type u} {h : Fintype ↑∅} :

Fintype.card ↑∅ = 0

theorem Set.card_fintypeInsertOfNotMem {α : Type u} {a : α} (s : Set α) [Fintype ↑s] (h : a ∉ s) :

Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

@[simp]

theorem Set.card_insert {α : Type u} {a : α} (s : Set α) [Fintype ↑s] (h : a ∉ s) {d : Fintype ↑(insert a s)} :

Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

theorem Set.card_image_of_inj_on {α : Type u} {β : Type v} {s : Set α} [Fintype ↑s] {f : α → β} [Fintype ↑(f '' s)] (H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) :

Fintype.card ↑(f '' s) = Fintype.card ↑s

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

@[simp]

theorem Set.card_singleton {α : Type u} (a : α) :

Fintype.card ↑{a} = 1

theorem Set.card_lt_card {α : Type u} {s t : Set α} [Fintype ↑s] [Fintype ↑t] (h : s ⊂ t) :

Fintype.card ↑s < Fintype.card ↑t

theorem Set.card_le_card {α : Type u} {s t : Set α} [Fintype ↑s] [Fintype ↑t] (hsub : 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] (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 ↑(range f)] :

Fintype.card ↑(range f) = Fintype.card α

theorem Set.Finite.card_toFinset {α : Type u} {s : Set α} [Fintype ↑s] (h : s.Finite) :

h.toFinset.card = Fintype.card ↑s

theorem Set.card_ne_eq {α : Type u} [Fintype α] (a : α) [Fintype ↑{x : α | x ≠ a}] :

Fintype.card ↑{x : α | x ≠ a} = Fintype.card α - 1

Infinite sets #

theorem Set.infinite_univ_iff {α : Type u} :

univ.Infinite ↔ Infinite α

theorem Set.infinite_univ {α : Type u} [h : Infinite α] :

univ.Infinite

theorem Set.Infinite.exists_not_mem_finite {α : Type u} {s t : Set α} (hs : s.Infinite) (ht : t.Finite) :

∃ a ∈ s, a ∉ t

theorem Set.Infinite.exists_not_mem_finset {α : Type u} {s : Set α} (hs : s.Infinite) (t : Finset α) :

∃ a ∈ s, a ∉ t

theorem Set.Finite.exists_not_mem {α : Type u} {s : Set α} [Infinite α] (hs : s.Finite) :

∃ (a : α), a ∉ s

theorem Finset.exists_not_mem {α : Type u} [Infinite α] (s : Finset α) :

∃ (a : α), a ∉ s

noncomputable def Set.Infinite.natEmbedding {α : Type u} (s : Set α) (h : s.Infinite) :

ℕ ↪ ↑s

Embedding of ℕ into an infinite set.

Equations

Set.Infinite.natEmbedding s h = Infinite.natEmbedding ↑s

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

s.Infinite

theorem Set.Finite.infinite_compl {α : Type u} [Infinite α] {s : Set α} (hs : s.Finite) :

sᶜ.Infinite

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

(s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

theorem Set.Infinite.of_image {α : Type u} {β : Type v} (f : α → β) {s : Set α} (hs : (f '' s).Infinite) :

s.Infinite

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

(f '' s).Infinite ↔ s.Infinite

theorem Set.infinite_range_iff {α : Type u} {β : Type v} {f : α → β} (hi : Function.Injective f) :

(range f).Infinite ↔ Infinite α

theorem Set.Infinite.image {α : Type u} {β : Type v} {s : Set α} {f : α → β} (hi : InjOn f s) :

s.Infinite → (f '' s).Infinite

Alias of the reverse direction of Set.infinite_image_iff.

theorem Set.infinite_of_injOn_mapsTo {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hi : InjOn f s) (hm : MapsTo f s t) (hs : s.Infinite) :

t.Infinite

theorem Set.Infinite.exists_ne_map_eq_of_mapsTo {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite) (hf : MapsTo f s t) (ht : t.Finite) :

∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

theorem Set.infinite_range_of_injective {α : Type u} {β : Type v} [Infinite α] {f : α → β} (hi : Function.Injective f) :

(range f).Infinite

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.not_injOn_infinite_finite_image {α : Type u} {β : Type v} {f : α → β} {s : Set α} (h_inf : s.Infinite) (h_fin : (f '' s).Finite) :

Order properties #

theorem Set.infinite_of_forall_exists_gt {α : Type u} [Preorder α] [Nonempty α] {s : Set α} (h : ∀ (a : α), ∃ b ∈ s, a < b) :

s.Infinite

theorem Set.infinite_of_forall_exists_lt {α : Type u} [Preorder α] [Nonempty α] {s : Set α} (h : ∀ (a : α), ∃ b ∈ s, b < a) :

s.Infinite

theorem Set.finite_isTop (α : Type u_1) [PartialOrder α] :

{x : α | IsTop x}.Finite

theorem Set.finite_isBot (α : Type u_1) [PartialOrder α] :

{x : α | IsBot x}.Finite

theorem Set.Infinite.exists_lt_map_eq_of_mapsTo {α : Type u} {β : Type v} [LinearOrder α] {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite) (hf : MapsTo f s t) (ht : t.Finite) :

∃ x ∈ s, ∃ y ∈ s, x < y ∧ f x = f y

theorem Set.Finite.exists_lt_map_eq_of_forall_mem {α : Type u} {β : Type v} [LinearOrder α] [Infinite α] {t : Set β} {f : α → β} (hf : ∀ (a : α), f a ∈ t) (ht : t.Finite) :

∃ (a : α) (b : α), a < b ∧ f a = f b

theorem Set.finite_range_findGreatest {α : Type u} {P : α → ℕ → Prop} [(x : α) → DecidablePred (P x)] {b : ℕ} :

(range fun (x : α) => Nat.findGreatest (P x) b).Finite

theorem Set.Finite.exists_maximal_wrt {α : Type u} {β : Type v} [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite) (hs : s.Nonempty) :

∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

theorem Set.Finite.exists_maximal_wrt' {α : Type u} {β : Type v} [PartialOrder β] (f : α → β) (s : Set α) (h : (f '' s).Finite) (hs : s.Nonempty) :

∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

A version of Finite.exists_maximal_wrt with the (weaker) hypothesis that the image of s is finite rather than s itself.

theorem Set.Finite.exists_minimal_wrt {α : Type u} {β : Type v} [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite) (hs : s.Nonempty) :

∃ a ∈ s, ∀ a' ∈ s, f a' ≤ f a → f a = f a'

theorem Set.Finite.exists_minimal_wrt' {α : Type u} {β : Type v} [PartialOrder β] (f : α → β) (s : Set α) (h : (f '' s).Finite) (hs : s.Nonempty) :

∃ a ∈ s, ∀ a' ∈ s, f a' ≤ f a → f a = f a'

A version of Finite.exists_minimal_wrt with the (weaker) hypothesis that the image of s is finite rather than s itself.

theorem Finset.exists_card_eq {α : Type u} [Infinite α] (n : ℕ) :

∃ (s : Finset α), s.card = n

theorem Finite.of_forall_not_lt_lt {α : Type u} [LinearOrder α] (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} [LinearOrder α] {s : Set α} (h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) :

s.Finite

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

theorem Directed.exists_mem_subset_of_finset_subset_biUnion {α : Type u_1} {ι : Type u_2} [Nonempty ι] {f : ι → Set α} (h : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) f) {s : Finset α} (hs : ↑s ⊆ ⋃ (i : ι), f i) :

∃ (i : ι), ↑s ⊆ f i