Mathlib.Data.Set.Finite.Basic

Set.finite_def theorem

{s : Set α} : s.Finite ↔ Nonempty (Fintype s)

Full source

theorem finite_def {s : Set α} : s.Finite ↔ Nonempty (Fintype s) :=
  finite_iff_nonempty_fintype s

Equivalence of Set Finiteness and Existence of Fintype Instance

Informal description

A set $s$ in a type $\alpha$ is finite if and only if there exists a `Fintype` instance for $s$, meaning that $s$ can be represented as a finite type.

Set.Finite.ofFinset theorem

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

Full source

/-- Construct a `Finite` instance for a `Set` from a `Finset` with the same elements. -/
protected theorem Finite.ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ sx ∈ s ↔ x ∈ p) : p.Finite :=
  have := Fintype.ofFinset s H; p.toFinite

Finite Set Construction from Finset Membership Condition

Informal description

Given a set $p$ in a type $\alpha$ and a finite set $s$ of elements of $\alpha$ such that for every $x \in \alpha$, $x$ belongs to $s$ if and only if $x$ belongs to $p$, then $p$ is finite.

Set.Finite.fintype definition

{s : Set α} (h : s.Finite) : Fintype s

Full source

/-- 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 -/
protected noncomputable def Finite.fintype {s : Set α} (h : s.Finite) : Fintype s :=
  h.nonempty_fintype.some

Fintype instance for a finite set

Informal description

Given a finite set $s$ in a type $\alpha$, this definition constructs a `Fintype` instance for $s$, allowing $s$ to be treated as a finite type.

Set.Finite.toFinset definition

{s : Set α} (h : s.Finite) : Finset α

Full source

/-- Using choice, get the `Finset` that represents this `Set`. -/
protected noncomputable def Finite.toFinset {s : Set α} (h : s.Finite) : Finset α :=
  @Set.toFinset _ _ h.fintype

Finset representation of a finite set

Informal description

Given a finite set $s$ in a type $\alpha$, this definition noncomputably constructs a finset representing $s$ using the axiom of choice. The resulting finset has the same elements as $s$.

Set.Finite.toFinset_eq_toFinset theorem

{s : Set α} [Fintype s] (h : s.Finite) : h.toFinset = s.toFinset

Full source

theorem Finite.toFinset_eq_toFinset {s : Set α} [Fintype s] (h : s.Finite) :
    h.toFinset = s.toFinset := by
  rw [Finite.toFinset, Subsingleton.elim h.fintype]

Equality of Finset Constructions for Finite Sets

Informal description

For any finite set $s$ in a type $\alpha$ with a `Fintype` instance, the finset obtained from the `Set.Finite` proof $h$ is equal to the finset obtained directly from $s$.

Set.toFinite_toFinset theorem

(s : Set α) [Fintype s] : s.toFinite.toFinset = s.toFinset

Full source

@[simp]
theorem toFinite_toFinset (s : Set α) [Fintype s] : s.toFinite.toFinset = s.toFinset :=
  s.toFinite.toFinset_eq_toFinset

Equality of Finset Conversions for Finite Sets

Informal description

For any set $s$ in a type $\alpha$ with a `Fintype` instance, the finset obtained by first converting $s$ to a finite set (via `toFinite`) and then to a finset (via `toFinset`) is equal to the finset obtained directly from $s$ (via `toFinset`).

Set.Finite.exists_finset theorem

{s : Set α} (h : s.Finite) : ∃ s' : Finset α, ∀ a : α, a ∈ s' ↔ a ∈ s

Full source

theorem Finite.exists_finset {s : Set α} (h : s.Finite) :
    ∃ s' : Finset α, ∀ a : α, a ∈ s' ↔ a ∈ s := by
  cases h.nonempty_fintype
  exact ⟨s.toFinset, fun _ => mem_toFinset⟩

Existence of Finset Representing a Finite Set

Informal description

For any finite set $s$ in a type $\alpha$, there exists a finset $s'$ such that for every element $a \in \alpha$, $a$ belongs to $s'$ if and only if $a$ belongs to $s$.

Set.Finite.exists_finset_coe theorem

{s : Set α} (h : s.Finite) : ∃ s' : Finset α, ↑s' = s

Full source

theorem Finite.exists_finset_coe {s : Set α} (h : s.Finite) : ∃ s' : Finset α, ↑s' = s := by
  cases h.nonempty_fintype
  exact ⟨s.toFinset, s.coe_toFinset⟩

Existence of Finset Representation for Finite Sets

Informal description

For any finite set $s$ in a type $\alpha$, there exists a finset $s'$ (a finite set with decidable membership) such that the underlying set of $s'$ is equal to $s$.

Set.instCanLiftFinsetToSetFinite instance

: CanLift (Set α) (Finset α) (↑) Set.Finite

Full source

/-- Finite sets can be lifted to finsets. -/
instance : CanLift (Set α) (Finset α) (↑) Set.Finite where prf _ hs := hs.exists_finset_coe

Lifting Finite Sets to Finsets

Informal description

For any type $\alpha$, finite sets in $\alpha$ can be lifted to finsets via the canonical coercion function from finsets to sets.

Set.Finite.mem_toFinset theorem

: a ∈ hs.toFinset ↔ a ∈ s

Full source

@[simp]
protected theorem mem_toFinset : a ∈ hs.toFinseta ∈ hs.toFinset ↔ a ∈ s :=
  @mem_toFinset _ _ hs.fintype _

Membership in Finset Representation of Finite Set

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ in $\alpha$ with proof $hs$ of finiteness, the element $a$ belongs to the finset representation of $s$ (constructed via `hs.toFinset`) if and only if $a$ belongs to the set $s$.

Set.Finite.coe_toFinset theorem

: (hs.toFinset : Set α) = s

Full source

@[simp]
protected theorem coe_toFinset : (hs.toFinset : Set α) = s :=
  @coe_toFinset _ _ hs.fintype

Finset Representation Preserves Underlying Set for Finite Sets

Informal description

For any finite set $s$ in a type $\alpha$ with a proof $hs$ of finiteness, the underlying set of the finset representation `hs.toFinset` is equal to $s$.

Set.Finite.toFinset_nonempty theorem

: hs.toFinset.Nonempty ↔ s.Nonempty

Full source

@[simp]
protected theorem toFinset_nonempty : hs.toFinset.Nonempty ↔ s.Nonempty := by
  rw [← Finset.coe_nonempty, Finite.coe_toFinset]

Nonemptiness of Finset Representation for Finite Sets

Informal description

For any finite set $s$ in a type $\alpha$ with a proof $hs$ of finiteness, the finset representation `hs.toFinset` is nonempty if and only if the set $s$ itself is nonempty.

Set.Finite.coeSort_toFinset theorem

: ↥hs.toFinset = ↥s

Full source

/-- Note that this is an equality of types not holding definitionally. Use wisely. -/
theorem coeSort_toFinset : ↥hs.toFinset = ↥s := by
  rw [← Finset.coe_sort_coe _, hs.coe_toFinset]

Equality of Subtypes for Finite Set and its Finset Representation

Informal description

For a finite set $s$ in a type $\alpha$ with a finiteness proof $hs$, the subtype of elements in the finset representation `hs.toFinset` is equal to the subtype of elements in $s$, i.e., $\{x \mid x \in hs.\text{toFinset}\} = \{x \mid x \in s\}$.

Set.Finite.subtypeEquivToFinset definition

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

Full source

/-- 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`. -/
@[simps!] def subtypeEquivToFinset : {x // x ∈ s}{x // x ∈ s} ≃ {x // x ∈ hs.toFinset} :=
  (Equiv.refl α).subtypeEquiv fun _ ↦ hs.mem_toFinset.symm

Equivalence between Subtype of Finite Set and its Finset Representation

Informal description

Given a finite set $ s $ in a type $ \alpha $ with a proof $ hs $ of finiteness, the equivalence between the subtype $ \{x \in \alpha \mid x \in s\} $ and the subtype $ \{x \in \alpha \mid x \in hs.\text{toFinset}\} $, where $ hs.\text{toFinset} $ is the finset representation of $ s $. This equivalence is constructed using the identity map on $ \alpha $, adjusted by the fact that membership in $ s $ is equivalent to membership in $ hs.\text{toFinset} $.

Set.Finite.toFinset_inj theorem

: hs.toFinset = ht.toFinset ↔ s = t

Full source

@[simp]
protected theorem toFinset_inj : hs.toFinset = ht.toFinset ↔ s = t :=
  @toFinset_inj _ _ _ hs.fintype ht.fintype

Equality of Finite Sets via Finset Representation

Informal description

For any two finite sets $s$ and $t$ in a type $\alpha$, the finsets obtained from their finite representations are equal if and only if the sets themselves are equal, i.e., $hs.\text{toFinset} = ht.\text{toFinset} \leftrightarrow s = t$.

Set.Finite.toFinset_subset theorem

{t : Finset α} : hs.toFinset ⊆ t ↔ s ⊆ t

Full source

@[simp]
theorem toFinset_subset {t : Finset α} : hs.toFinset ⊆ ths.toFinset ⊆ t ↔ s ⊆ t := by
  rw [← Finset.coe_subset, Finite.coe_toFinset]

Subset Correspondence between Finite Set and Finset Representation

Informal description

For any finite set $s$ in a type $\alpha$ with a proof $hs$ of finiteness, and for any finset $t$ of $\alpha$, the finset representation $hs.\text{toFinset}$ is a subset of $t$ if and only if $s$ is a subset of the underlying set of $t$.

Set.Finite.toFinset_ssubset theorem

{t : Finset α} : hs.toFinset ⊂ t ↔ s ⊂ t

Full source

@[simp]
theorem toFinset_ssubset {t : Finset α} : hs.toFinset ⊂ ths.toFinset ⊂ t ↔ s ⊂ t := by
  rw [← Finset.coe_ssubset, Finite.coe_toFinset]

Strict Subset Correspondence between Finite Set and Finset Representation

Informal description

For any finite set $s$ in a type $\alpha$ with a proof $hs$ of finiteness, and for any finset $t$ of $\alpha$, the finset representation `hs.toFinset` is a strict subset of $t$ if and only if $s$ is a strict subset of the underlying set of $t$.

Set.Finite.subset_toFinset theorem

{s : Finset α} : s ⊆ ht.toFinset ↔ ↑s ⊆ t

Full source

@[simp]
theorem subset_toFinset {s : Finset α} : s ⊆ ht.toFinsets ⊆ ht.toFinset ↔ ↑s ⊆ t := by
  rw [← Finset.coe_subset, Finite.coe_toFinset]

Subset Relation between Finset and Finite Set Representation

Informal description

For any finite set $t$ in a type $\alpha$ with a proof $ht$ of finiteness, and for any finset $s$ of $\alpha$, the finset $s$ is a subset of the finset representation $ht.\text{toFinset}$ if and only if the underlying set of $s$ is a subset of $t$.

Set.Finite.ssubset_toFinset theorem

{s : Finset α} : s ⊂ ht.toFinset ↔ ↑s ⊂ t

Full source

@[simp]
theorem ssubset_toFinset {s : Finset α} : s ⊂ ht.toFinsets ⊂ ht.toFinset ↔ ↑s ⊂ t := by
  rw [← Finset.coe_ssubset, Finite.coe_toFinset]

Strict Subset Relation between Finset and Finite Set Representation

Informal description

For any finite set $t$ in a type $\alpha$ with a proof $ht$ of finiteness, and for any finset $s$ of $\alpha$, the finset $s$ is a strict subset of the finset representation `ht.toFinset` if and only if the underlying set of $s$ is a strict subset of $t$.

Set.Finite.toFinset_subset_toFinset theorem

: hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t

Full source

@[mono]
protected theorem toFinset_subset_toFinset : hs.toFinset ⊆ ht.toFinseths.toFinset ⊆ ht.toFinset ↔ s ⊆ t := by
  simp only [← Finset.coe_subset, Finite.coe_toFinset]

Subset Relation between Finset Representations of Finite Sets

Informal description

For any two finite sets $s$ and $t$ in a type $\alpha$ with proofs $hs$ and $ht$ of finiteness respectively, the finset representation of $s$ is a subset of the finset representation of $t$ if and only if $s$ is a subset of $t$. In other words, $hs.\text{toFinset} \subseteq ht.\text{toFinset} \leftrightarrow s \subseteq t$.

Set.Finite.toFinset_ssubset_toFinset theorem

: hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t

Full source

@[mono]
protected theorem toFinset_ssubset_toFinset : hs.toFinset ⊂ ht.toFinseths.toFinset ⊂ ht.toFinset ↔ s ⊂ t := by
  simp only [← Finset.coe_ssubset, Finite.coe_toFinset]

Strict Subset Relation between Finset Representations of Finite Sets

Informal description

For any two finite sets $s$ and $t$ in a type $\alpha$ with proofs $hs$ and $ht$ of finiteness respectively, the finset representation of $s$ is a strict subset of the finset representation of $t$ if and only if $s$ is a strict subset of $t$. In other words, $hs.\text{toFinset} \subset ht.\text{toFinset} \leftrightarrow s \subset t$.

Set.Finite.toFinset_setOf theorem

[Fintype α] (p : α → Prop) [DecidablePred p] (h : {x | p x}.Finite) : h.toFinset = ({x | p x} : Finset α)

Full source

@[simp high]
protected theorem toFinset_setOf [Fintype α] (p : α → Prop) [DecidablePred p]
    (h : { x | p x }.Finite) : h.toFinset = ({x | p x} : Finset α) := by simp

Equality of Finset Representations for Finite Predicate Sets

Informal description

For a finite type $\alpha$ with a decidable predicate $p : \alpha \to \mathrm{Prop}$, if the set $\{x \mid p(x)\}$ is finite, then the finset representation of this set (via `h.toFinset`) is equal to the finset $\{x \mid p(x)\}$ constructed directly.

Set.Finite.disjoint_toFinset theorem

{hs : s.Finite} {ht : t.Finite} : Disjoint hs.toFinset ht.toFinset ↔ Disjoint s t

Full source

@[simp]
nonrec theorem disjoint_toFinset {hs : s.Finite} {ht : t.Finite} :
    DisjointDisjoint hs.toFinset ht.toFinset ↔ Disjoint s t :=
  @disjoint_toFinset _ _ _ hs.fintype ht.fintype

Disjointness of Finset Representations of Finite Sets

Informal description

For any finite sets $s$ and $t$ in a type $\alpha$ with finiteness proofs $hs$ and $ht$ respectively, the finset representations $hs.\text{toFinset}$ and $ht.\text{toFinset}$ are disjoint if and only if the sets $s$ and $t$ themselves are disjoint.

Set.Finite.toFinset_inter theorem

[DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∩ t).Finite) : h.toFinset = hs.toFinset ∩ ht.toFinset

Full source

protected theorem toFinset_inter [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s ∩ t).Finite) : h.toFinset = hs.toFinset ∩ ht.toFinset := by
  ext
  simp

Finset Representation of Finite Set Intersection

Informal description

For any sets $s$ and $t$ in a type $\alpha$ with decidable equality, if $s$, $t$, and their intersection $s \cap t$ are all finite, then the finset representation of $s \cap t$ is equal to the intersection of the finset representations of $s$ and $t$. That is, $(s \cap t).\text{toFinset} = s.\text{toFinset} \cap t.\text{toFinset}$.

Set.Finite.toFinset_union theorem

[DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∪ t).Finite) : h.toFinset = hs.toFinset ∪ ht.toFinset

Full source

protected theorem toFinset_union [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s ∪ t).Finite) : h.toFinset = hs.toFinset ∪ ht.toFinset := by
  ext
  simp

Finset Representation of Finite Set Union

Informal description

For any sets $s$ and $t$ in a type $\alpha$ with decidable equality, if $s$, $t$, and their union $s \cup t$ are all finite, then the finset representation of $s \cup t$ is equal to the union of the finset representations of $s$ and $t$. That is, $(s \cup t).\text{toFinset} = s.\text{toFinset} \cup t.\text{toFinset}$.

Set.Finite.toFinset_diff theorem

[DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s \ t).Finite) : h.toFinset = hs.toFinset \ ht.toFinset

Full source

protected theorem toFinset_diff [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s \ t).Finite) : h.toFinset = hs.toFinset \ ht.toFinset := by
  ext
  simp

Finset Representation of Finite Set Difference

Informal description

For any sets $s$ and $t$ in a type $\alpha$ with decidable equality, if $s$, $t$, and their set difference $s \setminus t$ are all finite, then the finset representation of $s \setminus t$ is equal to the set difference of the finset representations of $s$ and $t$. That is, $(s \setminus t).\text{toFinset} = s.\text{toFinset} \setminus t.\text{toFinset}$.

Set.Finite.toFinset_symmDiff theorem

[DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∆ t).Finite) : h.toFinset = hs.toFinset ∆ ht.toFinset

Full source

protected theorem toFinset_symmDiff [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s ∆ t).Finite) : h.toFinset = hs.toFinset ∆ ht.toFinset := by
  ext
  simp [mem_symmDiff, Finset.mem_symmDiff]

Finset Representation of Finite Symmetric Difference

Informal description

For any sets $s$ and $t$ in a type $\alpha$ with decidable equality, if $s$, $t$, and their symmetric difference $s \triangle t$ are all finite, then the finset representation of $s \triangle t$ is equal to the symmetric difference of the finset representations of $s$ and $t$. That is, $(s \triangle t).\text{toFinset} = s.\text{toFinset} \triangle t.\text{toFinset}$.

Set.Finite.toFinset_compl theorem

[DecidableEq α] [Fintype α] (hs : s.Finite) (h : sᶜ.Finite) : h.toFinset = hs.toFinsetᶜ

Full source

protected theorem toFinset_compl [DecidableEq α] [Fintype α] (hs : s.Finite) (h : sᶜ.Finite) :
    h.toFinset = hs.toFinsetᶜ := by
  ext
  simp

Complement of Finite Set's Finset Representation

Informal description

Let $\alpha$ be a type with decidable equality and a finite type instance. For any finite subset $s$ of $\alpha$ such that its complement $s^\complement$ is also finite, the finset representation of $s^\complement$ equals the complement of the finset representation of $s$. That is, $h.\text{toFinset} = \text{hs.toFinset}^\complement$.

Set.Finite.toFinset_univ theorem

[Fintype α] (h : (Set.univ : Set α).Finite) : h.toFinset = Finset.univ

Full source

protected theorem toFinset_univ [Fintype α] (h : (Set.univ : Set α).Finite) :
    h.toFinset = Finset.univ := by
  simp

Universal Set to Universal Finset Conversion

Informal description

For a finite type $\alpha$, the finset representation of the universal set $\text{univ}$ (with a proof of its finiteness) is equal to the universal finset $\text{Finset.univ}$.

Set.Finite.toFinset_eq_empty theorem

{h : s.Finite} : h.toFinset = ∅ ↔ s = ∅

Full source

@[simp]
protected theorem toFinset_eq_empty {h : s.Finite} : h.toFinset = ∅ ↔ s = ∅ :=
  @toFinset_eq_empty _ _ h.fintype

Finset Representation of Finite Set is Empty iff Set is Empty

Informal description

For any finite set $s$ in a type $\alpha$, the finset representation of $s$ is empty if and only if $s$ itself is the empty set. In other words, $h.\text{toFinset} = \emptyset \leftrightarrow s = \emptyset$.

Set.Finite.toFinset_empty theorem

(h : (∅ : Set α).Finite) : h.toFinset = ∅

Full source

protected theorem toFinset_empty (h : (∅ : Set α).Finite) : h.toFinset = ∅ := by
  simp

Empty Set to Empty Finset Conversion

Informal description

For any type $\alpha$, the `toFinset` construction applied to the empty set $\emptyset$ (with a proof of its finiteness) yields the empty finset $\emptyset$.

Set.Finite.toFinset_eq_univ theorem

[Fintype α] {h : s.Finite} : h.toFinset = Finset.univ ↔ s = univ

Full source

@[simp]
protected theorem toFinset_eq_univ [Fintype α] {h : s.Finite} :
    h.toFinset = Finset.univ ↔ s = univ :=
  @toFinset_eq_univ _ _ _ h.fintype

Finset Representation Equals Universal Finset iff Set is Universal Set

Informal description

For a finite type $\alpha$ and a finite subset $s \subseteq \alpha$, the finset representation of $s$ is equal to the universal finset (containing all elements of $\alpha$) if and only if $s$ is the universal set $\alpha$. In other words: $$ \text{toFinset}(s) = \text{univ} \leftrightarrow s = \text{univ} $$

Set.Finite.toFinset_image theorem

[DecidableEq β] (f : α → β) (hs : s.Finite) (h : (f '' s).Finite) : h.toFinset = hs.toFinset.image f

Full source

protected theorem toFinset_image [DecidableEq β] (f : α → β) (hs : s.Finite) (h : (f '' s).Finite) :
    h.toFinset = hs.toFinset.image f := by
  ext
  simp

Image of Finite Set Under Function Preserves Finset Representation

Informal description

Let $f : \alpha \to \beta$ be a function between types with decidable equality on $\beta$, and let $s$ be a finite subset of $\alpha$. If the image $f(s)$ is finite, then the finset representation of $f(s)$ is equal to the image of the finset representation of $s$ under $f$. In other words, we have: $$ \text{toFinset}(f(s)) = \text{image}\, f\, (\text{toFinset}(s)) $$

Set.Finite.toFinset_range theorem

[DecidableEq α] [Fintype β] (f : β → α) (h : (range f).Finite) : h.toFinset = Finset.univ.image f

Full source

protected theorem toFinset_range [DecidableEq α] [Fintype β] (f : β → α) (h : (range f).Finite) :
    h.toFinset = Finset.univ.image f := by
  ext
  simp

Finset Representation of Range Equals Image of Universal Finset

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$ and $\beta$ being finite. For any function $f : \beta \to \alpha$ with finite range, the finset representation of the range of $f$ is equal to the image of the universal finset of $\beta$ under $f$. That is: $$ \text{toFinset}(\text{range}\, f) = \text{image}\, f\, (\text{Finset.univ}) $$

Set.Finite.toFinset_nontrivial theorem

(h : s.Finite) : h.toFinset.Nontrivial ↔ s.Nontrivial

Full source

@[simp]
protected theorem toFinset_nontrivial (h : s.Finite) : h.toFinset.Nontrivial ↔ s.Nontrivial := by
  rw [Finset.Nontrivial, h.coe_toFinset]

Nontriviality of Finite Set Preserved in Finset Representation

Informal description

For any finite set $s$ in a type $\alpha$ with a proof $h$ of finiteness, the finset representation `h.toFinset` is nontrivial (contains at least two distinct elements) if and only if the set $s$ itself is nontrivial.

Set.fintypeUniv instance

[Fintype α] : Fintype (@univ α)

Full source

instance fintypeUniv [Fintype α] : Fintype (@univ α) :=
  Fintype.ofEquiv α (Equiv.Set.univ α).symm

Finite Universal Set for Finite Types

Informal description

For any finite type $\alpha$, the universal set $\text{univ} \alpha$ is also finite.

Set.fintypeTop instance

[Fintype α] : Fintype (⊤ : Set α)

Full source

instance fintypeTop [Fintype α] : Fintype (⊤ : Set α) := inferInstanceAs (Fintype (univ : Set α))

Finiteness of the Universal Set in Finite Types

Informal description

For any finite type $\alpha$, the top element $\top$ in the set lattice of $\alpha$ (which is the universal set) is finite.

Set.fintypeOfFiniteUniv definition

(H : (univ (α := α)).Finite) : Fintype α

Full source

/-- If `(Set.univ : Set α)` is finite then `α` is a finite type. -/
noncomputable def fintypeOfFiniteUniv (H : (univ (α := α)).Finite) : Fintype α :=
  @Fintype.ofEquiv _ (univ : Set α) H.fintype (Equiv.Set.univ _)

Finite type from finite universal set

Informal description

If the universal set of a type $\alpha$ is finite, then $\alpha$ itself is a finite type. This is established by constructing a bijection between $\alpha$ and its universal set, leveraging the existing `Fintype` instance for the universal set.

Set.fintypeUnion instance

[DecidableEq α] (s t : Set α) [Fintype s] [Fintype t] : Fintype (s ∪ t : Set α)

Full source

instance fintypeUnion [DecidableEq α] (s t : Set α) [Fintype s] [Fintype t] :
    Fintype (s ∪ t : Set α) :=
  Fintype.ofFinset (s.toFinset ∪ t.toFinset) <| by simp

Finite Union of Finite Sets

Informal description

For any type $\alpha$ with decidable equality, and any two finite subsets $s$ and $t$ of $\alpha$, the union $s \cup t$ is also finite.

Set.fintypeSep instance

(s : Set α) (p : α → Prop) [Fintype s] [DecidablePred p] : Fintype ({a ∈ s | p a} : Set α)

Full source

instance fintypeSep (s : Set α) (p : α → Prop) [Fintype s] [DecidablePred p] :
    Fintype ({ a ∈ s | p a } : Set α) :=
  Fintype.ofFinset {a ∈ s.toFinset | p a} <| by simp

Finite Subset Defined by a Predicate

Informal description

For any finite subset $s$ of a type $\alpha$ and any decidable predicate $p$ on $\alpha$, the subset $\{a \in s \mid p(a)\}$ is also finite.

Set.fintypeInter instance

(s t : Set α) [DecidableEq α] [Fintype s] [Fintype t] : Fintype (s ∩ t : Set α)

Full source

instance fintypeInter (s t : Set α) [DecidableEq α] [Fintype s] [Fintype t] :
    Fintype (s ∩ t : Set α) :=
  Fintype.ofFinset (s.toFinset ∩ t.toFinset) <| by simp

Finite Intersection of Finite Sets

Informal description

For any type $\alpha$ with decidable equality and any two finite subsets $s$ and $t$ of $\alpha$, the intersection $s \cap t$ is also finite.

Set.fintypeInterOfLeft instance

(s t : Set α) [Fintype s] [DecidablePred (· ∈ t)] : Fintype (s ∩ t : Set α)

Full source

/-- A `Fintype` instance for set intersection where the left set has a `Fintype` instance. -/
instance fintypeInterOfLeft (s t : Set α) [Fintype s] [DecidablePred (· ∈ t)] :
    Fintype (s ∩ t : Set α) :=
  Fintype.ofFinset {a ∈ s.toFinset | a ∈ t} <| by simp

Finite Intersection with Decidable Membership

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $s$ is finite and membership in $t$ is decidable, then the intersection $s \cap t$ is finite.

Set.fintypeInterOfRight instance

(s t : Set α) [Fintype t] [DecidablePred (· ∈ s)] : Fintype (s ∩ t : Set α)

Full source

/-- A `Fintype` instance for set intersection where the right set has a `Fintype` instance. -/
instance fintypeInterOfRight (s t : Set α) [Fintype t] [DecidablePred (· ∈ s)] :
    Fintype (s ∩ t : Set α) :=
  Fintype.ofFinset {a ∈ t.toFinset | a ∈ s} <| by simp [and_comm]

Finiteness of Intersection with a Finite Set

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $t$ is finite and membership in $s$ is decidable, then the intersection $s \cap t$ is finite.

Set.fintypeSubset definition

(s : Set α) {t : Set α} [Fintype s] [DecidablePred (· ∈ t)] (h : t ⊆ s) : Fintype t

Full source

/-- A `Fintype` structure on a set defines a `Fintype` structure on its subset. -/
def fintypeSubset (s : Set α) {t : Set α} [Fintype s] [DecidablePred (· ∈ t)] (h : t ⊆ s) :
    Fintype t := by
  rw [← inter_eq_self_of_subset_right h]
  apply Set.fintypeInterOfLeft

Finiteness of subsets of a finite set

Informal description

Given a finite set $s$ in a type $\alpha$ and a subset $t \subseteq s$ with decidable membership, the subset $t$ is also finite. This is established by observing that $t$ can be written as the intersection $s \cap t$ (since $t \subseteq s$), and then applying the finiteness of intersections with decidable membership.

Set.fintypeDiff instance

[DecidableEq α] (s t : Set α) [Fintype s] [Fintype t] : Fintype (s \ t : Set α)

Full source

instance fintypeDiff [DecidableEq α] (s t : Set α) [Fintype s] [Fintype t] :
    Fintype (s \ t : Set α) :=
  Fintype.ofFinset (s.toFinset \ t.toFinset) <| by simp

Finite Set Difference of Finite Sets

Informal description

For any type $\alpha$ with decidable equality, and any two finite sets $s$ and $t$ in $\alpha$, the set difference $s \setminus t$ is also finite.

Set.fintypeDiffLeft instance

(s t : Set α) [Fintype s] [DecidablePred (· ∈ t)] : Fintype (s \ t : Set α)

Full source

instance fintypeDiffLeft (s t : Set α) [Fintype s] [DecidablePred (· ∈ t)] :
    Fintype (s \ t : Set α) :=
  Set.fintypeSep s (· ∈ tᶜ)

Finite Set Difference with Decidable Membership

Informal description

For any finite set $s$ in a type $\alpha$ and any set $t$ with a decidable membership predicate, the set difference $s \setminus t$ is finite.

Set.fintypeEmpty instance

: Fintype (∅ : Set α)

Full source

instance fintypeEmpty : Fintype (∅ : Set α) :=
  Fintype.ofFinset ∅ <| by simp

Finite Empty Set

Informal description

The empty set $\emptyset$ is finite.

Set.fintypeSingleton instance

(a : α) : Fintype ({ a } : Set α)

Full source

instance fintypeSingleton (a : α) : Fintype ({a} : Set α) :=
  Fintype.ofFinset {a} <| by simp

Finite Singleton Sets

Informal description

For any element $a$ of type $\alpha$, the singleton set $\{a\}$ is finite.

Set.fintypeInsert instance

(a : α) (s : Set α) [DecidableEq α] [Fintype s] : Fintype (insert a s : Set α)

Full source

/-- 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. -/
instance fintypeInsert (a : α) (s : Set α) [DecidableEq α] [Fintype s] :
    Fintype (insert a s : Set α) :=
  Fintype.ofFinset (insert a s.toFinset) <| by simp

Finite Insertion of an Element into a Finite Set

Informal description

For any type $\alpha$ with decidable equality and any finite set $s \subseteq \alpha$, the set $\text{insert}(a, s) = \{a\} \cup s$ is finite.

Set.fintypeInsertOfNotMem definition

{a : α} (s : Set α) [Fintype s] (h : a ∉ s) : Fintype (insert a s : Set α)

Full source

/-- A `Fintype` structure on `insert a s` when inserting a new element. -/
def fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) :
    Fintype (insert a s : Set α) :=
  Fintype.ofFinset ⟨a ::ₘ s.toFinset.1, s.toFinset.nodup.cons (by simp [h])⟩ <| by simp

Finite structure for inserting a new element into a finite set

Informal description

Given a finite set $s$ of type $\alpha$ and an element $a \notin s$, the structure `Fintype` is defined for the set $\text{insert } a \text{ } s = \{a\} \cup s$, which is finite since $s$ is finite and $a$ is a new element.

Set.fintypeInsertOfMem definition

{a : α} (s : Set α) [Fintype s] (h : a ∈ s) : Fintype (insert a s : Set α)

Full source

/-- A `Fintype` structure on `insert a s` when inserting a pre-existing element. -/
def fintypeInsertOfMem {a : α} (s : Set α) [Fintype s] (h : a ∈ s) : Fintype (insert a s : Set α) :=
  Fintype.ofFinset s.toFinset <| by simp [h]

Finite structure for inserting an existing element into a finite set

Informal description

Given a finite set $s$ of type $\alpha$ and an element $a \in s$, the structure `Fintype` is defined for the set $\text{insert } a \text{ } s$, which is equal to $s$ since $a$ is already in $s$.

Set.fintypeInsert' instance

(a : α) (s : Set α) [Decidable <| a ∈ s] [Fintype s] : Fintype (insert a s : Set α)

Full source

/-- 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]. -/
instance (priority := 100) fintypeInsert' (a : α) (s : Set α) [Decidable <| a ∈ s] [Fintype s] :
    Fintype (insert a s : Set α) :=
  if h : a ∈ s then fintypeInsertOfMem s h else fintypeInsertOfNotMem s h

Finiteness of Insertion into Finite Sets

Informal description

For any element $a$ of type $\alpha$ and a finite set $s \subseteq \alpha$ with decidable membership for $a$, the set $\{a\} \cup s$ is finite.

Set.fintypeImage instance

[DecidableEq β] (s : Set α) (f : α → β) [Fintype s] : Fintype (f '' s)

Full source

instance fintypeImage [DecidableEq β] (s : Set α) (f : α → β) [Fintype s] : Fintype (f '' s) :=
  Fintype.ofFinset (s.toFinset.image f) <| by simp

Finite Image of a Finite Set

Informal description

For any set $s$ in a type $\alpha$ with a finite type structure, and any function $f : \alpha \to \beta$ where $\beta$ has decidable equality, the image $f(s)$ is also a finite set.

Set.fintypeOfFintypeImage definition

(s : Set α) {f : α → β} {g} (I : IsPartialInv f g) [Fintype (f '' s)] : Fintype s

Full source

/-- 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. -/
def fintypeOfFintypeImage (s : Set α) {f : α → β} {g} (I : IsPartialInv f g) [Fintype (f '' s)] :
    Fintype s :=
  Fintype.ofFinset ⟨_, (f '' s).toFinset.2.filterMap g <| injective_of_isPartialInv_right I⟩
    fun a => by
    suffices (∃ b x, f x = b ∧ g b = some a ∧ x ∈ s) ↔ a ∈ s by
      simpa [exists_and_left.symm, and_comm, and_left_comm, and_assoc]
    rw [exists_swap]
    suffices (∃ x, x ∈ s ∧ g (f x) = some a) ↔ a ∈ s by simpa [and_comm, and_left_comm, and_assoc]
    simp [I _, (injective_of_isPartialInv I).eq_iff]

Finiteness of a set via finiteness of its image under a partially invertible function

Informal description

Given a set $ s \subseteq \alpha $, a function $ f : \alpha \to \beta $, and a partial inverse $ g $ of $ f $ (i.e., $ g $ satisfies $ g(y) = \text{some }x $ if and only if $ f(x) = y $), if the image $ f(s) $ is finite, then $ s $ itself is finite.

Set.fintypeMap instance

{α β} [DecidableEq β] : ∀ (s : Set α) (f : α → β) [Fintype s], Fintype (f <$> s)

Full source

instance fintypeMap {α β} [DecidableEq β] :
    ∀ (s : Set α) (f : α → β) [Fintype s], Fintype (f <$> s) :=
  Set.fintypeImage

Finite Image under Functorial Map

Informal description

For any set $s$ in a type $\alpha$ with a finite type structure, and any function $f : \alpha \to \beta$ where $\beta$ has decidable equality, the image of $s$ under the functorial action of $f$ (denoted $f <$>$ s$) is also a finite set.

Set.fintypeLTNat instance

(n : ℕ) : Fintype {i | i < n}

Full source

instance fintypeLTNat (n : ℕ) : Fintype { i | i < n } :=
  Fintype.ofFinset (Finset.range n) <| by simp

Finite Set of Natural Numbers Less Than $n$

Informal description

For any natural number $n$, the set $\{i \mid i < n\}$ is finite.

Set.fintypeLENat instance

(n : ℕ) : Fintype {i | i ≤ n}

Full source

instance fintypeLENat (n : ℕ) : Fintype { i | i ≤ n } := by
  simpa [Nat.lt_succ_iff] using Set.fintypeLTNat (n + 1)

Finite Set of Natural Numbers Less Than or Equal to $n$

Informal description

For any natural number $n$, the set $\{i \mid i \leq n\}$ is finite.

Set.Nat.fintypeIio definition

(n : ℕ) : Fintype (Iio n)

Full source

/-- This is not an instance so that it does not conflict with the one
in `Mathlib/Order/LocallyFinite.lean`. -/
def Nat.fintypeIio (n : ℕ) : Fintype (Iio n) :=
  Set.fintypeLTNat n

Finiteness of the natural numbers less than $n$

Informal description

For any natural number $n$, the set $\{i \mid i < n\}$ is finite, where $\operatorname{Iio}(n)$ denotes the left-infinite right-open interval $(-\infty, n)$ of natural numbers.

Set.fintypeMemFinset instance

(s : Finset α) : Fintype {a | a ∈ s}

Full source

instance fintypeMemFinset (s : Finset α) : Fintype { a | a ∈ s } :=
  Finset.fintypeCoeSort s

Finiteness of the Underlying Set of a Finset

Informal description

For any finset $s$ of type $\alpha$, the set $\{a \mid a \in s\}$ is finite.

Finset.finite_toSet theorem

(s : Finset α) : (s : Set α).Finite

Full source

/-- Gives a `Set.Finite` for the `Finset` coerced to a `Set`.
This is a wrapper around `Set.toFinite`. -/
@[simp]
theorem finite_toSet (s : Finset α) : (s : Set α).Finite :=
  Set.toFinite _

Finiteness of the Underlying Set of a Finset

Informal description

For any finset $s$ of type $\alpha$, the underlying set of $s$ is finite.

Finset.finite_toSet_toFinset theorem

(s : Finset α) : s.finite_toSet.toFinset = s

Full source

theorem finite_toSet_toFinset (s : Finset α) : s.finite_toSet.toFinset = s := by
  rw [toFinite_toFinset, toFinset_coe]

Finset Conversion from Underlying Set Preserves Equality

Informal description

For any finset $s$ of type $\alpha$, the finset obtained by converting the underlying set of $s$ to a finite set and then to a finset is equal to $s$ itself.

Finset.forall theorem

{p : Finset α → Prop} : (∀ s, p s) ↔ ∀ (s : Set α) (hs : s.Finite), p hs.toFinset

Full source

/-- This is a kind of induction principle. See `Finset.induction` for the usual induction principle
for finsets. -/
lemma «forall» {p : Finset α → Prop} :
    (∀ s, p s) ↔ ∀ (s : Set α) (hs : s.Finite), p hs.toFinset where
  mp h s hs := h _
  mpr h s := by simpa using h s s.finite_toSet

Universal Quantification over Finsets via Finite Sets

Informal description

For any predicate $p$ on finsets of type $\alpha$, the universal quantification $\forall s, p(s)$ holds if and only if for every finite set $s$ in $\alpha$ (with a proof $hs$ of its finiteness), the predicate $p$ holds for the finset obtained from $s$ via `toFinset`.

Finset.exists theorem

{p : Finset α → Prop} : (∃ s, p s) ↔ ∃ (s : Set α) (hs : s.Finite), p hs.toFinset

Full source

lemma «exists» {p : Finset α → Prop} :
    (∃ s, p s) ↔ ∃ (s : Set α) (hs : s.Finite), p hs.toFinset where
  mp := fun ⟨s, hs⟩ ↦ ⟨s, s.finite_toSet, by simpa⟩
  mpr := fun ⟨s, hs, hs'⟩ ↦ ⟨hs.toFinset, hs'⟩

Existence of Finset Satisfying Predicate via Finite Set Conversion

Informal description

For any predicate $p$ on finsets of type $\alpha$, there exists a finset satisfying $p$ if and only if there exists a finite set $s$ in $\alpha$ such that the finset obtained from $s$ via `Set.Finite.toFinset` satisfies $p$.

Multiset.finite_toSet theorem

(s : Multiset α) : {x | x ∈ s}.Finite

Full source

@[simp]
theorem finite_toSet (s : Multiset α) : { x | x ∈ s }.Finite := by
  classical simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet

Finiteness of the Underlying Set of a Multiset

Informal description

For any multiset $s$ of type $\alpha$, the set $\{x \mid x \in s\}$ is finite.

Multiset.finite_toSet_toFinset theorem

[DecidableEq α] (s : Multiset α) : s.finite_toSet.toFinset = s.toFinset

Full source

@[simp]
theorem finite_toSet_toFinset [DecidableEq α] (s : Multiset α) :
    s.finite_toSet.toFinset = s.toFinset := by
  ext x
  simp

Equality of Finset Constructions from Multiset and Its Underlying Set

Informal description

For any multiset $s$ of elements of type $\alpha$ (with decidable equality), the finset obtained from the finite set $\{x \mid x \in s\}$ via `Set.Finite.toFinset` is equal to the finset obtained directly from $s$ via `Multiset.toFinset$.

List.finite_toSet theorem

(l : List α) : {x | x ∈ l}.Finite

Full source

@[simp]
theorem List.finite_toSet (l : List α) : { x | x ∈ l }.Finite :=
  (show Multiset α from ⟦l⟧).finite_toSet

Finiteness of the Underlying Set of a List

Informal description

For any list $l$ of elements of type $\alpha$, the set $\{x \mid x \in l\}$ is finite.

Finite.Set.finite_union instance

(s t : Set α) [Finite s] [Finite t] : Finite (s ∪ t : Set α)

Full source

instance finite_union (s t : Set α) [Finite s] [Finite t] : Finite (s ∪ t : Set α) := by
  cases nonempty_fintype s
  cases nonempty_fintype t
  classical
  infer_instance

Finite Union of Finite Sets

Informal description

For any type $\alpha$ and any two finite subsets $s$ and $t$ of $\alpha$, the union $s \cup t$ is also finite.

Finite.Set.finite_sep instance

(s : Set α) (p : α → Prop) [Finite s] : Finite ({a ∈ s | p a} : Set α)

Full source

instance finite_sep (s : Set α) (p : α → Prop) [Finite s] : Finite ({ a ∈ s | p a } : Set α) := by
  cases nonempty_fintype s
  classical
  infer_instance

Finite Subsets Defined by Predicates are Finite

Informal description

For any finite subset $s$ of a type $\alpha$ and any predicate $p$ on $\alpha$, the subset $\{a \in s \mid p(a)\}$ is also finite.

Finite.Set.subset theorem

(s : Set α) {t : Set α} [Finite s] (h : t ⊆ s) : Finite t

Full source

protected theorem subset (s : Set α) {t : Set α} [Finite s] (h : t ⊆ s) : Finite t := by
  rw [← sep_eq_of_subset h]
  infer_instance

Subsets of Finite Sets are Finite

Informal description

For any finite subset $s$ of a type $\alpha$, any subset $t$ of $s$ is also finite.

Finite.Set.finite_inter_of_right instance

(s t : Set α) [Finite t] : Finite (s ∩ t : Set α)

Full source

instance finite_inter_of_right (s t : Set α) [Finite t] : Finite (s ∩ t : Set α) :=
  Finite.Set.subset t inter_subset_right

Finite Intersection of a Set with a Finite Set

Informal description

For any subsets $s$ and $t$ of a type $\alpha$, if $t$ is finite, then the intersection $s \cap t$ is also finite.

Finite.Set.finite_inter_of_left instance

(s t : Set α) [Finite s] : Finite (s ∩ t : Set α)

Full source

instance finite_inter_of_left (s t : Set α) [Finite s] : Finite (s ∩ t : Set α) :=
  Finite.Set.subset s inter_subset_left

Finite Intersection of a Finite Set with Any Set

Informal description

For any subsets $s$ and $t$ of a type $\alpha$, if $s$ is finite, then the intersection $s \cap t$ is also finite.

Finite.Set.finite_diff instance

(s t : Set α) [Finite s] : Finite (s \ t : Set α)

Full source

instance finite_diff (s t : Set α) [Finite s] : Finite (s \ t : Set α) :=
  Finite.Set.subset s diff_subset

Finite Difference of Finite Sets

Informal description

For any finite subset $s$ of a type $\alpha$ and any subset $t$ of $\alpha$, the difference set $s \setminus t$ is also finite.

Finite.Set.finite_insert instance

(a : α) (s : Set α) [Finite s] : Finite (insert a s : Set α)

Full source

instance finite_insert (a : α) (s : Set α) [Finite s] : Finite (insert a s : Set α) :=
  Finite.Set.finite_union {a} s

Finite Insertion of an Element into a Finite Set

Informal description

For any element $a$ of type $\alpha$ and any finite subset $s$ of $\alpha$, the set obtained by inserting $a$ into $s$ is also finite.

Finite.Set.finite_image instance

(s : Set α) (f : α → β) [Finite s] : Finite (f '' s)

Full source

instance finite_image (s : Set α) (f : α → β) [Finite s] : Finite (f '' s) := by
  cases nonempty_fintype s
  classical
  infer_instance

Images of Finite Sets are Finite

Informal description

For any finite set $s$ in a type $\alpha$ and any function $f : \alpha \to \beta$, the image $f(s)$ is also finite.

Set.Finite.of_subsingleton theorem

[Subsingleton α] (s : Set α) : s.Finite

Full source

@[nontriviality]
theorem Finite.of_subsingleton [Subsingleton α] (s : Set α) : s.Finite :=
  s.toFinite

Finite Subsets of a Subsingleton

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements are equal), any subset $s$ of $\alpha$ is finite.

Set.finite_univ theorem

[Finite α] : (@univ α).Finite

Full source

theorem finite_univ [Finite α] : (@univ α).Finite :=
  Set.toFinite _

Universality of Finite Types: $\text{univ}$ is Finite

Informal description

For any finite type $\alpha$, the universal set $\text{univ} = \{x \mid x \in \alpha\}$ is finite.

Set.finite_univ_iff theorem

: (@univ α).Finite ↔ Finite α

Full source

theorem finite_univ_iff : (@univ α).Finite ↔ Finite α := (Equiv.Set.univ α).finite_iff

Finite Universal Set Equivalence

Informal description

The universal set of a type $\alpha$ is finite if and only if the type $\alpha$ itself is finite.

Set.Finite.subset theorem

{s : Set α} (hs : s.Finite) {t : Set α} (ht : t ⊆ s) : t.Finite

Full source

theorem Finite.subset {s : Set α} (hs : s.Finite) {t : Set α} (ht : t ⊆ s) : t.Finite := by
  have := hs.to_subtype
  exact Finite.Set.subset _ ht

Subsets of Finite Sets are Finite

Informal description

For any finite subset $s$ of a type $\alpha$, any subset $t$ of $s$ is also finite.

Set.Finite.union theorem

(hs : s.Finite) (ht : t.Finite) : (s ∪ t).Finite

Full source

theorem Finite.union (hs : s.Finite) (ht : t.Finite) : (s ∪ t).Finite := by
  rw [Set.Finite] at hs ht
  apply toFinite

Union of Finite Sets is Finite

Informal description

For any type $\alpha$ and any two finite subsets $s$ and $t$ of $\alpha$, the union $s \cup t$ is also finite.

Set.Finite.finite_of_compl theorem

{s : Set α} (hs : s.Finite) (hsc : sᶜ.Finite) : Finite α

Full source

theorem Finite.finite_of_compl {s : Set α} (hs : s.Finite) (hsc : sᶜ.Finite) : Finite α := by
  rw [← finite_univ_iff, ← union_compl_self s]
  exact hs.union hsc

Finiteness of Type from Finite Set and Complement

Informal description

For any subset $s$ of a type $\alpha$, if both $s$ and its complement $s^c$ are finite, then the type $\alpha$ itself is finite.

Set.Finite.sup theorem

{s t : Set α} : s.Finite → t.Finite → (s ⊔ t).Finite

Full source

theorem Finite.sup {s t : Set α} : s.Finite → t.Finite → (s ⊔ t).Finite :=
  Finite.union

Finiteness of the Supremum of Two Finite Sets

Informal description

For any two subsets $s$ and $t$ of a type $\alpha$, if $s$ is finite and $t$ is finite, then their supremum $s \sqcup t$ (which corresponds to their union in the lattice of subsets) is finite.

Set.Finite.sep theorem

{s : Set α} (hs : s.Finite) (p : α → Prop) : {a ∈ s | p a}.Finite

Full source

theorem Finite.sep {s : Set α} (hs : s.Finite) (p : α → Prop) : { a ∈ s | p a }.Finite :=
  hs.subset <| sep_subset _ _

Separation of Finite Sets Preserves Finiteness

Informal description

For any finite subset $s$ of a type $\alpha$ and any predicate $p$ on $\alpha$, the subset $\{a \in s \mid p(a)\}$ is finite.

Set.Finite.inter_of_left theorem

{s : Set α} (hs : s.Finite) (t : Set α) : (s ∩ t).Finite

Full source

theorem Finite.inter_of_left {s : Set α} (hs : s.Finite) (t : Set α) : (s ∩ t).Finite :=
  hs.subset inter_subset_left

Finite Intersection Property: Left Intersection with Finite Set is Finite

Informal description

For any finite subset $s$ of a type $\alpha$ and any subset $t$ of $\alpha$, the intersection $s \cap t$ is finite.

Set.Finite.inter_of_right theorem

{s : Set α} (hs : s.Finite) (t : Set α) : (t ∩ s).Finite

Full source

theorem Finite.inter_of_right {s : Set α} (hs : s.Finite) (t : Set α) : (t ∩ s).Finite :=
  hs.subset inter_subset_right

Finite Intersection Property: Right Intersection with Finite Set is Finite

Informal description

For any finite subset $s$ of a type $\alpha$ and any subset $t$ of $\alpha$, the intersection $t \cap s$ is finite.

Set.Finite.inf_of_left theorem

{s : Set α} (h : s.Finite) (t : Set α) : (s ⊓ t).Finite

Full source

theorem Finite.inf_of_left {s : Set α} (h : s.Finite) (t : Set α) : (s ⊓ t).Finite :=
  h.inter_of_left t

Finite Intersection Property: Left Infimum with Finite Set is Finite

Informal description

For any finite subset $s$ of a type $\alpha$ and any subset $t$ of $\alpha$, the infimum (intersection) $s \sqcap t$ is finite.

Set.Finite.inf_of_right theorem

{s : Set α} (h : s.Finite) (t : Set α) : (t ⊓ s).Finite

Full source

theorem Finite.inf_of_right {s : Set α} (h : s.Finite) (t : Set α) : (t ⊓ s).Finite :=
  h.inter_of_right t

Finite Intersection Property: Left Intersection with Finite Set is Finite

Informal description

For any finite subset $s$ of a type $\alpha$ and any subset $t$ of $\alpha$, the intersection $t \cap s$ is finite.

Set.Infinite.mono theorem

{s t : Set α} (h : s ⊆ t) : s.Infinite → t.Infinite

Full source

protected lemma Infinite.mono {s t : Set α} (h : s ⊆ t) : s.Infinite → t.Infinite :=
  mt fun ht ↦ ht.subset h

Infinite Sets are Monotone Under Inclusion

Informal description

For any sets $s$ and $t$ of a type $\alpha$, if $s$ is infinite and $s \subseteq t$, then $t$ is also infinite.

Set.Finite.diff theorem

(hs : s.Finite) : (s \ t).Finite

Full source

theorem Finite.diff (hs : s.Finite) : (s \ t).Finite := hs.subset diff_subset

Finite Difference of Sets

Informal description

For any finite set $s$ and any set $t$ (both subsets of a type $\alpha$), the set difference $s \setminus t$ is finite.

Set.Finite.of_diff theorem

{s t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) : s.Finite

Full source

theorem Finite.of_diff {s t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) : s.Finite :=
  (hd.union ht).subset <| subset_diff_union _ _

Finite Union of Finite Difference and Finite Set

Informal description

For any sets $s$ and $t$ of a type $\alpha$, if the set difference $s \setminus t$ is finite and $t$ is finite, then $s$ is finite.

Set.Finite.symmDiff theorem

(hs : s.Finite) (ht : t.Finite) : (s ∆ t).Finite

Full source

lemma Finite.symmDiff (hs : s.Finite) (ht : t.Finite) : (s ∆ t).Finite := hs.diff.union ht.diff

Finiteness of Symmetric Difference of Finite Sets

Informal description

For any finite sets $s$ and $t$ (both subsets of a type $\alpha$), the symmetric difference $s \triangle t$ is finite.

Set.Finite.symmDiff_congr theorem

(hst : (s ∆ t).Finite) : (s ∆ u).Finite ↔ (t ∆ u).Finite

Full source

lemma Finite.symmDiff_congr (hst : (s ∆ t).Finite) : (s ∆ u).Finite ↔ (t ∆ u).Finite where
  mp hsu := (hst.union hsu).subset (symmDiff_comm s t ▸ symmDiff_triangle ..)
  mpr htu := (hst.union htu).subset (symmDiff_triangle ..)

Finite Symmetric Difference Congruence: $s \triangle u$ finite iff $t \triangle u$ finite when $s \triangle t$ is finite

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if the symmetric difference $s \triangle t$ is finite, then the symmetric difference $s \triangle u$ is finite if and only if the symmetric difference $t \triangle u$ is finite.

Set.finite_empty theorem

: (∅ : Set α).Finite

Full source

@[simp]
theorem finite_empty : (∅ : Set α).Finite :=
  toFinite _

Finiteness of the Empty Set

Informal description

The empty set $\emptyset$ in any type $\alpha$ is finite.

Set.Infinite.nonempty theorem

{s : Set α} (h : s.Infinite) : s.Nonempty

Full source

protected theorem Infinite.nonempty {s : Set α} (h : s.Infinite) : s.Nonempty :=
  nonempty_iff_ne_empty.2 <| by
    rintro rfl
    exact h finite_empty

Nonemptiness of Infinite Sets

Informal description

For any infinite set $s$ in a type $\alpha$, the set $s$ is nonempty.

Set.finite_singleton theorem

(a : α) : ({ a } : Set α).Finite

Full source

@[simp]
theorem finite_singleton (a : α) : ({a} : Set α).Finite :=
  toFinite _

Finiteness of Singleton Sets

Informal description

For any element $a$ of a type $\alpha$, the singleton set $\{a\}$ is finite.

Set.Finite.insert theorem

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

Full source

@[simp]
protected theorem Finite.insert (a : α) {s : Set α} (hs : s.Finite) : (insert a s).Finite :=
  (finite_singleton a).union hs

Finiteness of Insertion into Finite Set

Informal description

For any element $a$ of a type $\alpha$ and any finite subset $s$ of $\alpha$, the set obtained by inserting $a$ into $s$ (denoted as $\{a\} \cup s$) is finite.

Set.Finite.image theorem

{s : Set α} (f : α → β) (hs : s.Finite) : (f '' s).Finite

Full source

theorem Finite.image {s : Set α} (f : α → β) (hs : s.Finite) : (f '' s).Finite := by
  have := hs.to_subtype
  apply toFinite

Image of Finite Set is Finite

Informal description

For any finite set $s \subseteq \alpha$ and any function $f : \alpha \to \beta$, the image $f(s)$ is finite.

Set.Finite.of_surjOn theorem

{s : Set α} {t : Set β} (f : α → β) (hf : SurjOn f s t) (hs : s.Finite) : t.Finite

Full source

lemma Finite.of_surjOn {s : Set α} {t : Set β} (f : α → β) (hf : SurjOn f s t) (hs : s.Finite) :
    t.Finite := (hs.image _).subset hf

Surjective Image of Finite Set is Finite

Informal description

For any function $f \colon \alpha \to \beta$, if $f$ is surjective from a finite set $s \subseteq \alpha$ to a set $t \subseteq \beta$, then $t$ is finite.

Set.Finite.map theorem

{α β} {s : Set α} : ∀ f : α → β, s.Finite → (f <$> s).Finite

Full source

theorem Finite.map {α β} {s : Set α} : ∀ f : α → β, s.Finite → (f <$> s).Finite :=
  Finite.image

Finite Image under Function Mapping

Informal description

For any function $f : \alpha \to \beta$ and any finite set $s \subseteq \alpha$, the image of $s$ under $f$ (denoted $f <$> $s$) is finite.

Set.Finite.of_finite_image theorem

{s : Set α} {f : α → β} (h : (f '' s).Finite) (hi : Set.InjOn f s) : s.Finite

Full source

theorem Finite.of_finite_image {s : Set α} {f : α → β} (h : (f '' s).Finite) (hi : Set.InjOn f s) :
    s.Finite :=
  have := h.to_subtype
  .of_injective _ hi.bijOn_image.bijective.injective

Finite Image with Injectivity Implies Finite Domain

Informal description

For any set $s \subseteq \alpha$ and function $f : \alpha \to \beta$, if the image $f(s)$ is finite and $f$ is injective on $s$, then $s$ is finite.

Set.finite_of_finite_preimage theorem

(h : (f ⁻¹' s).Finite) (hs : s ⊆ range f) : s.Finite

Full source

theorem finite_of_finite_preimage (h : (f ⁻¹' s).Finite) (hs : s ⊆ range f) : s.Finite := by
  rw [← image_preimage_eq_of_subset hs]
  exact Finite.image f h

Finite Preimage Implies Finite Subset in Range

Informal description

For any function $f : \alpha \to \beta$ and subset $s \subseteq \beta$ contained in the range of $f$, if the preimage $f^{-1}(s)$ is finite, then $s$ is finite.

Set.Finite.of_preimage theorem

(h : (f ⁻¹' s).Finite) (hf : Surjective f) : s.Finite

Full source

theorem Finite.of_preimage (h : (f ⁻¹' s).Finite) (hf : Surjective f) : s.Finite :=
  hf.image_preimage s ▸ h.image _

Finite image under surjective map implies finite codomain subset

Informal description

Let $f : \alpha \to \beta$ be a surjective function and $s \subseteq \beta$ a subset. If the preimage $f^{-1}(s)$ is finite, then $s$ is finite.

Set.Finite.preimage theorem

(I : Set.InjOn f (f ⁻¹' s)) (h : s.Finite) : (f ⁻¹' s).Finite

Full source

theorem Finite.preimage (I : Set.InjOn f (f ⁻¹' s)) (h : s.Finite) : (f ⁻¹' s).Finite :=
  (h.subset (image_preimage_subset f s)).of_finite_image I

Finite Preimage under Injective Restriction

Informal description

For any function $f : \alpha \to \beta$ and finite subset $s \subseteq \beta$, if $f$ is injective on the preimage $f^{-1}(s)$, then the preimage $f^{-1}(s)$ is finite.

Set.Infinite.preimage theorem

(hs : s.Infinite) (hf : s ⊆ range f) : (f ⁻¹' s).Infinite

Full source

protected lemma Infinite.preimage (hs : s.Infinite) (hf : s ⊆ range f) : (f ⁻¹' s).Infinite :=
  fun h ↦ hs <| finite_of_finite_preimage h hf

Infinite Preimage of Infinite Subset in Range

Informal description

For any infinite subset $s \subseteq \beta$ that is contained in the range of a function $f : \alpha \to \beta$, the preimage $f^{-1}(s)$ is infinite.

Set.Infinite.preimage' theorem

(hs : (s ∩ range f).Infinite) : (f ⁻¹' s).Infinite

Full source

lemma Infinite.preimage' (hs : (s ∩ range f).Infinite) : (f ⁻¹' s).Infinite :=
  (hs.preimage inter_subset_right).mono <| preimage_mono inter_subset_left

Infinite Preimage of Infinite Intersection with Range

Informal description

For any set $s \subseteq \beta$ such that the intersection $s \cap \text{range}(f)$ is infinite, the preimage $f^{-1}(s)$ is infinite.

Set.Finite.preimage_embedding theorem

{s : Set β} (f : α ↪ β) (h : s.Finite) : (f ⁻¹' s).Finite

Full source

theorem Finite.preimage_embedding {s : Set β} (f : α ↪ β) (h : s.Finite) : (f ⁻¹' s).Finite :=
  h.preimage fun _ _ _ _ h' => f.injective h'

Finiteness of Preimage under Injective Embedding

Informal description

For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ and any finite subset $s \subseteq \beta$, the preimage $f^{-1}(s)$ is finite.

Set.finite_lt_nat theorem

(n : ℕ) : Set.Finite {i | i < n}

Full source

theorem finite_lt_nat (n : ℕ) : Set.Finite { i | i < n } :=
  toFinite _

Finiteness of Natural Numbers Below a Given Bound

Informal description

For any natural number $n$, the set $\{i \in \mathbb{N} \mid i < n\}$ is finite.

Set.finite_le_nat theorem

(n : ℕ) : Set.Finite {i | i ≤ n}

Full source

theorem finite_le_nat (n : ℕ) : Set.Finite { i | i ≤ n } :=
  toFinite _

Finiteness of Natural Numbers Up to a Given Bound

Informal description

For any natural number $n$, the set $\{i \in \mathbb{N} \mid i \leq n\}$ is finite.

Set.Finite.surjOn_iff_bijOn_of_mapsTo theorem

(hs : s.Finite) (hm : MapsTo f s s) : SurjOn f s s ↔ BijOn f s s

Full source

theorem Finite.surjOn_iff_bijOn_of_mapsTo (hs : s.Finite) (hm : MapsTo f s s) :
    SurjOnSurjOn f s s ↔ BijOn f s s := by
  refine ⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩
  have : Finite s := finite_coe_iff.mpr hs
  exact hm.restrict_inj.mp (Finite.injective_iff_surjective.mpr <| hm.restrict_surjective_iff.mpr h)

Surjectivity Implies Bijectivity for Finite Endomaps

Informal description

Let $s$ be a finite set and $f : s \to s$ be a function that maps $s$ to itself. Then $f$ is surjective on $s$ if and only if $f$ is bijective on $s$.

Set.Finite.injOn_iff_bijOn_of_mapsTo theorem

(hs : s.Finite) (hm : MapsTo f s s) : InjOn f s ↔ BijOn f s s

Full source

theorem Finite.injOn_iff_bijOn_of_mapsTo (hs : s.Finite) (hm : MapsTo f s s) :
    InjOnInjOn f s ↔ BijOn f s s := by
  refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩
  have : Finite s := finite_coe_iff.mpr hs
  exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

Injectivity Implies Bijectivity for Finite Endomaps

Informal description

Let $s$ be a finite set and $f : \alpha \to \alpha$ be a function that maps $s$ into itself. Then $f$ is injective on $s$ if and only if $f$ is bijective on $s$.

Set.finite_mem_finset theorem

(s : Finset α) : {a | a ∈ s}.Finite

Full source

theorem finite_mem_finset (s : Finset α) : { a | a ∈ s }.Finite :=
  toFinite _

Finiteness of the Underlying Set of a Finset

Informal description

For any finset $s$ of type $\alpha$, the set $\{a \mid a \in s\}$ is finite.

Set.Subsingleton.finite theorem

{s : Set α} (h : s.Subsingleton) : s.Finite

Full source

theorem Subsingleton.finite {s : Set α} (h : s.Subsingleton) : s.Finite :=
  h.induction_on finite_empty finite_singleton

Finiteness of Subsingleton Sets

Informal description

For any set $s$ in a type $\alpha$, if $s$ is a subsingleton (i.e., contains at most one element), then $s$ is finite.

Set.Infinite.nontrivial theorem

{s : Set α} (hs : s.Infinite) : s.Nontrivial

Full source

theorem Infinite.nontrivial {s : Set α} (hs : s.Infinite) : s.Nontrivial :=
  not_subsingleton_iff.1 <| mt Subsingleton.finite hs

Infinite Sets Are Nontrivial

Informal description

For any infinite set $s$ in a type $\alpha$, the set $s$ is nontrivial, meaning it contains at least two distinct elements.

Set.finite_preimage_inl_and_inr theorem

{s : Set (α ⊕ β)} : (Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite

Full source

theorem finite_preimage_inl_and_inr {s : Set (α ⊕ β)} :
    (Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite(Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite :=
  ⟨fun h => image_preimage_inl_union_image_preimage_inr s ▸ (h.1.image _).union (h.2.image _),
    fun h => ⟨h.preimage Sum.inl_injective.injOn, h.preimage Sum.inr_injective.injOn⟩⟩

Finite Preimages of Left and Right Inclusions Characterize Finite Sets in Disjoint Union

Informal description

For any set $s$ in the disjoint union $\alpha \oplus \beta$, the following are equivalent: 1. The preimages of $s$ under both the left inclusion $\text{inl} : \alpha \to \alpha \oplus \beta$ and the right inclusion $\text{inr} : \beta \to \alpha \oplus \beta$ are finite. 2. The set $s$ itself is finite.

Set.exists_finite_iff_finset theorem

{p : Set α → Prop} : (∃ s : Set α, s.Finite ∧ p s) ↔ ∃ s : Finset α, p ↑s

Full source

theorem exists_finite_iff_finset {p : Set α → Prop} :
    (∃ s : Set α, s.Finite ∧ p s) ↔ ∃ s : Finset α, p ↑s :=
  ⟨fun ⟨_, hs, hps⟩ => ⟨hs.toFinset, hs.coe_toFinset.symm ▸ hps⟩, fun ⟨s, hs⟩ =>
    ⟨s, s.finite_toSet, hs⟩⟩

Equivalence of Finite Subset and Finset Existence for Predicates

Informal description

For any predicate $p$ on subsets of a type $\alpha$, there exists a finite subset $s \subseteq \alpha$ satisfying $p(s)$ if and only if there exists a finset $s$ (of type `Finset α`) such that $p$ holds for the underlying set of $s$.

Set.exists_subset_image_finite_and theorem

 {f : α → β} {s : Set α} {p : Set β → Prop} : (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Full source

theorem exists_subset_image_finite_and {f : α → β} {s : Set α} {p : Set β → Prop} :
    (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t) := by
  classical
  simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]
  aesop

Existence of Finite Subset in Image vs. Preimage

Informal description

For any function $f \colon \alpha \to \beta$, a subset $s \subseteq \alpha$, and a predicate $p$ on subsets of $\beta$, the following are equivalent: 1. There exists a finite subset $t \subseteq f(s)$ such that $p(t)$ holds. 2. There exists a finite subset $t \subseteq s$ such that $p(f(t))$ holds.

Set.finite_range_ite theorem

 {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

Full source

theorem finite_range_ite {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 :=
  (hf.union hg).subset range_ite_subset

Finite Range of Conditional Function

Informal description

Let $p \colon \alpha \to \text{Prop}$ be a decidable predicate, and let $f, g \colon \alpha \to \beta$ be functions with finite ranges. Then the range of the function defined by $x \mapsto \text{if } p(x) \text{ then } f(x) \text{ else } g(x)$ is also finite.

Set.finite_range_const theorem

{c : β} : (range fun _ : α => c).Finite

Full source

theorem finite_range_const {c : β} : (range fun _ : α => c).Finite :=
  (finite_singleton c).subset range_const_subset

Finite Range of Constant Function

Informal description

For any constant function $f \colon \alpha \to \beta$ defined by $f(x) = c$ for some fixed $c \in \beta$, the range of $f$ is finite.

Set.Finite.inhabited instance

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

Full source

instance Finite.inhabited : Inhabited { s : Set α // s.Finite } :=
  ⟨⟨∅, finite_empty⟩⟩

Nonempty Collection of Finite Subsets

Informal description

For any type $\alpha$, the collection of finite subsets of $\alpha$ is nonempty.

Set.finite_union theorem

{s t : Set α} : (s ∪ t).Finite ↔ s.Finite ∧ t.Finite

Full source

@[simp]
theorem finite_union {s t : Set α} : (s ∪ t).Finite ↔ s.Finite ∧ t.Finite :=
  ⟨fun h => ⟨h.subset subset_union_left, h.subset subset_union_right⟩, fun ⟨hs, ht⟩ =>
    hs.union ht⟩

Finite Union Characterization: $s \cup t$ is finite $\iff$ $s$ and $t$ are finite

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the union $s \cup t$ is finite if and only if both $s$ and $t$ are finite.

Set.finite_image_iff theorem

{s : Set α} {f : α → β} (hi : InjOn f s) : (f '' s).Finite ↔ s.Finite

Full source

theorem finite_image_iff {s : Set α} {f : α → β} (hi : InjOn f s) : (f '' s).Finite ↔ s.Finite :=
  ⟨fun h => h.of_finite_image hi, Finite.image _⟩

Finite Image Equivalence under Injectivity

Informal description

For any set $s \subseteq \alpha$ and function $f : \alpha \to \beta$, if $f$ is injective on $s$, then the image $f(s)$ is finite if and only if $s$ is finite.

Set.univ_finite_iff_nonempty_fintype theorem

: (univ : Set α).Finite ↔ Nonempty (Fintype α)

Full source

theorem univ_finite_iff_nonempty_fintype : (univ : Set α).Finite ↔ Nonempty (Fintype α) :=
  ⟨fun h => ⟨fintypeOfFiniteUniv h⟩, fun ⟨_i⟩ => finite_univ⟩

Finite Universal Set iff Finite Type Structure Exists

Informal description

The universal set $\text{univ} = \{x \mid x \in \alpha\}$ is finite if and only if there exists a finite type structure (Fintype) on $\alpha$.

Set.Finite.toFinset_insert theorem

 [DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite) :
  hs.toFinset = insert a (hs.subset <| subset_insert _ _).toFinset

Full source

@[simp]
theorem Finite.toFinset_insert [DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite) :
    hs.toFinset = insert a (hs.subset <| subset_insert _ _).toFinset :=
  Finset.ext <| by simp

Finset Representation of Insertion into Finite Set

Informal description

Let $\alpha$ be a type with decidable equality, $s$ be a finite subset of $\alpha$, and $a$ be an element of $\alpha$. If the set $\{a\} \cup s$ is finite, then the finset representation of $\{a\} \cup s$ is equal to the finset obtained by inserting $a$ into the finset representation of $s$.

Set.Finite.toFinset_insert' theorem

[DecidableEq α] {a : α} {s : Set α} (hs : s.Finite) : (hs.insert a).toFinset = insert a hs.toFinset

Full source

theorem Finite.toFinset_insert' [DecidableEq α] {a : α} {s : Set α} (hs : s.Finite) :
    (hs.insert a).toFinset = insert a hs.toFinset :=
  Finite.toFinset_insert _

Finset representation of insertion into finite set: $(hs.insert\ a).toFinset = insert\ a\ hs.toFinset$

Informal description

Let $\alpha$ be a type with decidable equality, $s$ be a finite subset of $\alpha$, and $a$ be an element of $\alpha$. The finset representation of the finite set $\{a\} \cup s$ is equal to the finset obtained by inserting $a$ into the finset representation of $s$.

Set.finite_option theorem

{s : Set (Option α)} : s.Finite ↔ {x : α | some x ∈ s}.Finite

Full source

theorem finite_option {s : Set (Option α)} : s.Finite ↔ { x : α | some x ∈ s }.Finite :=
  ⟨fun h => h.preimage_embedding Embedding.some, fun h =>
    ((h.image some).insert none).subset fun x =>
      x.casesOn (fun _ => Or.inl rfl) fun _ hx => Or.inr <| mem_image_of_mem _ hx⟩

Finiteness of Option Set via Preimage of Some

Informal description

A set $s$ of elements in $\operatorname{Option} \alpha$ is finite if and only if the set $\{x \in \alpha \mid \operatorname{some}(x) \in s\}$ is finite.

Set.Finite.induction_on theorem

 {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ finite_empty)
  (insert : ∀ {a s}, a ∉ s → ∀ hs : Set.Finite s, motive s hs → motive (insert a s) (hs.insert a)) : motive s hs

Full source

/-- 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`. -/
@[elab_as_elim]
theorem Finite.induction_on {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α) (hs : s.Finite)
    (empty : motive ∅ finite_empty)
    (insert : ∀ {a s}, a ∉ s →
      ∀ hs : Set.Finite s, motive s hs → motive (insert a s) (hs.insert a)) :
    motive s hs := by
  lift s to Finset α using id hs
  induction' s using Finset.cons_induction_on with a s ha ih
  · simpa
  · simpa using @insert a s ha (Set.toFinite _) (ih _)

Finite Set Induction Principle

Informal description

Let $\alpha$ be a type and let $motive$ be a property of finite subsets of $\alpha$. To prove that $motive(s)$ holds for every finite subset $s \subseteq \alpha$, it suffices to: 1. Prove $motive(\emptyset)$, and 2. For any element $a \in \alpha$ and any finite subset $s \subseteq \alpha$ with $a \notin s$, show that $motive(s)$ implies $motive(\{a\} \cup s)$.

Set.Finite.induction_on_subset theorem

 {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ finite_empty)
  (insert :
    ∀ {a t}, a ∈ s → ∀ hts : t ⊆ s, a ∉ t → motive t (hs.subset hts) → motive (insert a t) ((hs.subset hts).insert a)) :
  motive s hs

Full source

/-- 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`. -/
@[elab_as_elim]
theorem Finite.induction_on_subset {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α)
    (hs : s.Finite) (empty : motive ∅ finite_empty)
    (insert : ∀ {a t}, a ∈ s → ∀ hts : t ⊆ s, a ∉ t → motive t (hs.subset hts) →
      motive (insert a t) ((hs.subset hts).insert a)) : motive s hs := by
  refine Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs
    (fun _ => empty) ?_ .rfl
  intro a s has _ hCs haS
  rw [insert_subset_iff] at haS
  exact insert haS.1 haS.2 has (hCs haS.2)

Finite Set Induction Principle for Subsets

Informal description

Let $\alpha$ be a type and let $motive$ be a property of finite subsets of $\alpha$. To prove that $motive(s)$ holds for every finite subset $s \subseteq \alpha$, it suffices to: 1. Prove $motive(\emptyset)$, and 2. For any element $a \in s$ and any subset $t \subseteq s$ with $a \notin t$, show that $motive(t)$ implies $motive(\{a\} \cup t)$.

Set.seq_of_forall_finite_exists theorem

 {γ : Type*} {P : γ → Set γ → Prop} (h : ∀ t : Set γ, t.Finite → ∃ c, P c t) : ∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n)

Full source

/-- 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 seq_of_forall_finite_exists {γ : Type*} {P : γ → Set γ → Prop}
    (h : ∀ t : Set γ, t.Finite → ∃ c, P c t) : ∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n) := by
  haveI : Nonempty γ := (h ∅ finite_empty).nonempty
  choose! c hc using h
  set f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k : Iio n => g k.1 k.2)
  set u : ℕ → γ := fun n => Nat.strongRecOn' n f
  refine ⟨u, fun n => ?_⟩
  convert hc (u '' Iio n) ((finite_lt_nat _).image _)
  rw [image_eq_range]
  exact Nat.strongRecOn'_beta

Existence of Sequence Satisfying Finite Subset Relation

Informal description

Let $\gamma$ be a type and $P$ be a relation between elements of $\gamma$ and subsets of $\gamma$. Suppose that for every finite subset $t \subseteq \gamma$, there exists an element $c \in \gamma$ such that $P(c, t)$ holds. Then there exists a sequence $(u_n)_{n \in \mathbb{N}}$ in $\gamma$ such that for every natural number $n$, the relation $P(u_n, u(\{0, \dots, n-1\}))$ holds, where $u(\{0, \dots, n-1\})$ denotes the image of the set $\{0, \dots, n-1\}$ under $u$.

Set.card_empty theorem

: Fintype.card (∅ : Set α) = 0

Full source

theorem card_empty : Fintype.card (∅ : Set α) = 0 :=
  rfl

Cardinality of Empty Set is Zero

Informal description

The cardinality of the empty set $\emptyset$ is $0$.

Set.card_fintypeInsertOfNotMem theorem

{a : α} (s : Set α) [Fintype s] (h : a ∉ s) : @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1

Full source

theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) :
    @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1 := by
  simp [fintypeInsertOfNotMem, Fintype.card_ofFinset]

Cardinality of Insertion into Finite Set: $|\{a\} \cup s| = |s| + 1$ when $a \notin s$

Informal description

Let $s$ be a finite set of elements of type $\alpha$, and let $a \notin s$ be an element of $\alpha$. Then the cardinality of the set $\{a\} \cup s$ is equal to the cardinality of $s$ plus one.

Set.card_insert theorem

 {a : α} (s : Set α) [Fintype s] (h : a ∉ s) {d : Fintype (insert a s : Set α)} : @Fintype.card _ d = Fintype.card s + 1

Full source

@[simp]
theorem card_insert {a : α} (s : Set α) [Fintype s] (h : a ∉ s)
    {d : Fintype (insert a s : Set α)} : @Fintype.card _ d = Fintype.card s + 1 := by
  rw [← card_fintypeInsertOfNotMem s h]; congr!

Cardinality of Insertion into Finite Set: $|\{a\} \cup s| = |s| + 1$ when $a \notin s$

Informal description

For any finite set $s$ of elements of type $\alpha$ and any element $a \notin s$, the cardinality of the set $\{a\} \cup s$ is equal to the cardinality of $s$ plus one, i.e., $|\{a\} \cup s| = |s| + 1$.

Set.card_image_of_inj_on theorem

 {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

Full source

theorem card_image_of_inj_on {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 :=
  haveI := Classical.propDecidable
  calc
    Fintype.card (f '' s) = (s.toFinset.image f).card := Fintype.card_of_finset' _ (by simp)
    _ = s.toFinset.card :=
      Finset.card_image_of_injOn fun x hx y hy hxy =>
        H x (mem_toFinset.1 hx) y (mem_toFinset.1 hy) hxy
    _ = Fintype.card s := (Fintype.card_of_finset' _ fun _ => mem_toFinset).symm

Cardinality of Image under Injective Function on Finite Set

Informal description

Let $s$ be a finite set of elements of type $\alpha$, and let $f : \alpha \to \beta$ be a function. If $f$ is injective on $s$ (i.e., for any $x, y \in s$, $f(x) = f(y)$ implies $x = y$), then the cardinality of the image $f(s)$ equals the cardinality of $s$.

Set.card_image_of_injective theorem

 (s : Set α) [Fintype s] {f : α → β} [Fintype (f '' s)] (H : Function.Injective f) :
  Fintype.card (f '' s) = Fintype.card s

Full source

theorem card_image_of_injective (s : Set α) [Fintype s] {f : α → β} [Fintype (f '' s)]
    (H : Function.Injective f) : Fintype.card (f '' s) = Fintype.card s :=
  card_image_of_inj_on fun _ _ _ _ h => H h

Cardinality of Image under Injective Function on Finite Set

Informal description

Let $s$ be a finite set of elements of type $\alpha$, and let $f : \alpha \to \beta$ be an injective function. Then the cardinality of the image $f(s)$ equals the cardinality of $s$.

Set.card_singleton theorem

(a : α) : Fintype.card ({ a } : Set α) = 1

Full source

@[simp]
theorem card_singleton (a : α) : Fintype.card ({a} : Set α) = 1 :=
  Fintype.card_ofSubsingleton _

Cardinality of Singleton Set is One

Informal description

For any element $a$ of type $\alpha$, the cardinality of the singleton set $\{a\}$ is equal to $1$.

Set.card_lt_card theorem

{s t : Set α} [Fintype s] [Fintype t] (h : s ⊂ t) : Fintype.card s < Fintype.card t

Full source

theorem card_lt_card {s t : Set α} [Fintype s] [Fintype t] (h : s ⊂ t) :
    Fintype.card s < Fintype.card t :=
  Fintype.card_lt_of_injective_not_surjective (Set.inclusion h.1) (Set.inclusion_injective h.1)
    fun hst => (ssubset_iff_subset_ne.1 h).2 (eq_of_inclusion_surjective hst)

Cardinality Strictly Increases with Proper Subset in Finite Sets

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, if $s$ is a proper subset of $t$, then the cardinality of $s$ is strictly less than the cardinality of $t$.

Set.card_le_card theorem

{s t : Set α} [Fintype s] [Fintype t] (hsub : s ⊆ t) : Fintype.card s ≤ Fintype.card t

Full source

theorem card_le_card {s t : Set α} [Fintype s] [Fintype t] (hsub : s ⊆ t) :
    Fintype.card s ≤ Fintype.card t :=
  Fintype.card_le_of_injective (Set.inclusion hsub) (Set.inclusion_injective hsub)

Subset Cardinality Inequality for Finite Sets

Informal description

For any finite sets $s$ and $t$ in a type $\alpha$, if $s$ is a subset of $t$ ($s \subseteq t$), then the cardinality of $s$ is less than or equal to the cardinality of $t$ ($|s| \leq |t|$).

Set.card_range_of_injective theorem

[Fintype α] {f : α → β} (hf : Injective f) [Fintype (range f)] : Fintype.card (range f) = Fintype.card α

Full source

theorem card_range_of_injective [Fintype α] {f : α → β} (hf : Injective f) [Fintype (range f)] :
    Fintype.card (range f) = Fintype.card α :=
  Eq.symm <| Fintype.card_congr <| Equiv.ofInjective f hf

Cardinality of Range of Injective Function Equals Domain Cardinality

Informal description

For any finite type $\alpha$ and an injective function $f \colon \alpha \to \beta$, the cardinality of the range of $f$ is equal to the cardinality of $\alpha$, i.e., $$|\text{range } f| = |\alpha|.$$

Set.Finite.card_toFinset theorem

{s : Set α} [Fintype s] (h : s.Finite) : h.toFinset.card = Fintype.card s

Full source

theorem Finite.card_toFinset {s : Set α} [Fintype s] (h : s.Finite) :
    h.toFinset.card = Fintype.card s :=
  Eq.symm <| Fintype.card_of_finset' _ fun _ ↦ h.mem_toFinset

Cardinality of Finset Representation Equals Fintype Cardinality

Informal description

For any finite set $s$ in a type $\alpha$ with a `Fintype` instance for $s$, the cardinality of the finset representation of $s$ (constructed via `h.toFinset`) is equal to the cardinality of $s$ as a fintype, i.e., $$|\text{h.toFinset}| = |s|.$$

Set.card_ne_eq theorem

[Fintype α] (a : α) [Fintype {x : α | x ≠ a}] : Fintype.card {x : α | x ≠ a} = Fintype.card α - 1

Full source

theorem card_ne_eq [Fintype α] (a : α) [Fintype { x : α | x ≠ a }] :
    Fintype.card { x : α | x ≠ a } = Fintype.card α - 1 := by
  haveI := Classical.decEq α
  rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]

Cardinality of Complement of Singleton in Finite Type

Informal description

Let $\alpha$ be a finite type. For any element $a \in \alpha$, the cardinality of the set $\{x \in \alpha \mid x \neq a\}$ is equal to the cardinality of $\alpha$ minus 1, i.e., $$|\{x \in \alpha \mid x \neq a\}| = |\alpha| - 1.$$

Set.infinite_univ_iff theorem

: (@univ α).Infinite ↔ Infinite α

Full source

theorem infinite_univ_iff : (@univ α).Infinite ↔ Infinite α := by
  rw [Set.Infinite, finite_univ_iff, not_finite_iff_infinite]

Infinite Universal Set Equivalence

Informal description

The universal set of a type $\alpha$ is infinite if and only if the type $\alpha$ itself is infinite.

Set.infinite_univ theorem

[h : Infinite α] : (@univ α).Infinite

Full source

theorem infinite_univ [h : Infinite α] : (@univ α).Infinite :=
  infinite_univ_iff.2 h

Universality of Infinite Types

Informal description

If a type $\alpha$ is infinite, then the universal set of $\alpha$ is infinite.

Set.Infinite.exists_not_mem_finite theorem

(hs : s.Infinite) (ht : t.Finite) : ∃ a, a ∈ s ∧ a ∉ t

Full source

lemma Infinite.exists_not_mem_finite (hs : s.Infinite) (ht : t.Finite) : ∃ a, a ∈ s ∧ a ∉ t := by
  by_contra! h; exact hs <| ht.subset h

Existence of Element in Infinite Set Not in Finite Set

Informal description

For any infinite subset $s$ of a type $\alpha$ and any finite subset $t$ of $\alpha$, there exists an element $a \in s$ such that $a \notin t$.

Set.Infinite.exists_not_mem_finset theorem

(hs : s.Infinite) (t : Finset α) : ∃ a ∈ s, a ∉ t

Full source

lemma Infinite.exists_not_mem_finset (hs : s.Infinite) (t : Finset α) : ∃ a ∈ s, a ∉ t :=
  hs.exists_not_mem_finite t.finite_toSet

Existence of Element in Infinite Set Outside Given Finset

Informal description

For any infinite subset $s$ of a type $\alpha$ and any finite subset $t$ of $\alpha$ represented as a finset, there exists an element $a \in s$ such that $a \notin t$.

Set.Finite.exists_not_mem theorem

(hs : s.Finite) : ∃ a, a ∉ s

Full source

lemma Finite.exists_not_mem (hs : s.Finite) : ∃ a, a ∉ s := by
  by_contra! h; exact infinite_univ (hs.subset fun a _ ↦ h _)

Existence of Element Outside Finite Set

Informal description

For any finite subset $s$ of a type $\alpha$, there exists an element $a \in \alpha$ such that $a \notin s$.

Finset.exists_not_mem theorem

(s : Finset α) : ∃ a, a ∉ s

Full source

lemma _root_.Finset.exists_not_mem (s : Finset α) : ∃ a, a ∉ s := s.finite_toSet.exists_not_mem

Existence of Element Outside Finite Set (Finset Version)

Informal description

For any finite set $s$ represented as a finset of type $\alpha$, there exists an element $a \in \alpha$ such that $a \notin s$.

Set.Infinite.natEmbedding definition

(s : Set α) (h : s.Infinite) : ℕ ↪ s

Full source

/-- Embedding of `ℕ` into an infinite set. -/
noncomputable def Infinite.natEmbedding (s : Set α) (h : s.Infinite) : ℕℕ ↪ s :=
  h.to_subtype.natEmbedding

Embedding of natural numbers into an infinite set

Informal description

Given an infinite set $s$ of type $\alpha$, there exists an injective function embedding from the natural numbers $\mathbb{N}$ into $s$.

Set.Infinite.exists_subset_card_eq theorem

{s : Set α} (hs : s.Infinite) (n : ℕ) : ∃ t : Finset α, ↑t ⊆ s ∧ t.card = n

Full source

theorem Infinite.exists_subset_card_eq {s : Set α} (hs : s.Infinite) (n : ℕ) :
    ∃ t : Finset α, ↑t ⊆ s ∧ t.card = n :=
  ⟨((Finset.range n).map (hs.natEmbedding _)).map (Embedding.subtype _), by simp⟩

Existence of Finite Subsets with Arbitrary Cardinality in Infinite Sets

Informal description

For any infinite set $s$ of type $\alpha$ and any natural number $n$, there exists a finite subset $t$ of $s$ (represented as a `Finset`) such that the cardinality of $t$ is equal to $n$.

Set.infinite_of_finite_compl theorem

[Infinite α] {s : Set α} (hs : sᶜ.Finite) : s.Infinite

Full source

theorem infinite_of_finite_compl [Infinite α] {s : Set α} (hs : sᶜ.Finite) : s.Infinite := fun h =>
  Set.infinite_univ (α := α) (by simpa using hs.union h)

Infinite Set from Finite Complement

Informal description

For an infinite type $\alpha$ and a subset $s$ of $\alpha$, if the complement $s^c$ is finite, then $s$ is infinite.

Set.Finite.infinite_compl theorem

[Infinite α] {s : Set α} (hs : s.Finite) : sᶜ.Infinite

Full source

theorem Finite.infinite_compl [Infinite α] {s : Set α} (hs : s.Finite) : sᶜ.Infinite := fun h =>
  Set.infinite_univ (α := α) (by simpa using hs.union h)

Complement of Finite Subset in Infinite Type is Infinite

Informal description

For an infinite type $\alpha$ and a finite subset $s \subseteq \alpha$, the complement $s^c$ is infinite.

Set.Infinite.diff theorem

{s t : Set α} (hs : s.Infinite) (ht : t.Finite) : (s \ t).Infinite

Full source

theorem Infinite.diff {s t : Set α} (hs : s.Infinite) (ht : t.Finite) : (s \ t).Infinite := fun h =>
  hs <| h.of_diff ht

Infinite Set Difference with Finite Set is Infinite

Informal description

For any infinite set $s$ and finite set $t$ in a type $\alpha$, the set difference $s \setminus t$ is infinite.

Set.infinite_union theorem

{s t : Set α} : (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

Full source

@[simp]
theorem infinite_union {s t : Set α} : (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite := by
  simp only [Set.Infinite, finite_union, not_and_or]

Union of Sets is Infinite if and Only if at Least One Set is Infinite

Informal description

For any sets $s$ and $t$ in a type $\alpha$, the union $s \cup t$ is infinite if and only if at least one of $s$ or $t$ is infinite.

Set.Infinite.of_image theorem

(f : α → β) {s : Set α} (hs : (f '' s).Infinite) : s.Infinite

Full source

theorem Infinite.of_image (f : α → β) {s : Set α} (hs : (f '' s).Infinite) : s.Infinite :=
  mt (Finite.image f) hs

Preimage of Infinite Image is Infinite

Informal description

For any function $f : \alpha \to \beta$ and any set $s \subseteq \alpha$, if the image $f(s)$ is infinite, then $s$ is infinite.

Set.infinite_image_iff theorem

{s : Set α} {f : α → β} (hi : InjOn f s) : (f '' s).Infinite ↔ s.Infinite

Full source

theorem infinite_image_iff {s : Set α} {f : α → β} (hi : InjOn f s) :
    (f '' s).Infinite ↔ s.Infinite :=
  not_congr <| finite_image_iff hi

Infinite Image Equivalence under Injectivity

Informal description

For any set $s \subseteq \alpha$ and function $f \colon \alpha \to \beta$, if $f$ is injective on $s$, then the image $f(s)$ is infinite if and only if $s$ is infinite.

Set.infinite_range_iff theorem

{f : α → β} (hi : Injective f) : (range f).Infinite ↔ Infinite α

Full source

theorem infinite_range_iff {f : α → β} (hi : Injective f) :
    (range f).Infinite ↔ Infinite α := by
  rw [← image_univ, infinite_image_iff hi.injOn, infinite_univ_iff]

Range of Injective Function is Infinite iff Domain is Infinite

Informal description

For any injective function $f \colon \alpha \to \beta$, the range of $f$ is infinite if and only if the domain type $\alpha$ is infinite.

Set.infinite_of_injOn_mapsTo theorem

{s : Set α} {t : Set β} {f : α → β} (hi : InjOn f s) (hm : MapsTo f s t) (hs : s.Infinite) : t.Infinite

Full source

theorem infinite_of_injOn_mapsTo {s : Set α} {t : Set β} {f : α → β} (hi : InjOn f s)
    (hm : MapsTo f s t) (hs : s.Infinite) : t.Infinite :=
  ((infinite_image_iff hi).2 hs).mono (mapsTo'.mp hm)

Infinite Image Theorem for Injective Mappings

Informal description

Let $s \subseteq \alpha$ be an infinite set, $t \subseteq \beta$ be a set, and $f \colon \alpha \to \beta$ be a function that is injective on $s$ and maps $s$ into $t$. Then $t$ is infinite.

Set.Infinite.exists_ne_map_eq_of_mapsTo theorem

 {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

Full source

theorem Infinite.exists_ne_map_eq_of_mapsTo {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 := by
  contrapose! ht
  exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs

Infinite Domain and Finite Codomain Imply Non-Injective Mapping

Informal description

Let $s \subseteq \alpha$ be an infinite set, $t \subseteq \beta$ be a finite set, and $f \colon \alpha \to \beta$ be a function that maps $s$ into $t$. Then there exist distinct elements $x, y \in s$ such that $f(x) = f(y)$.

Set.infinite_range_of_injective theorem

[Infinite α] {f : α → β} (hi : Injective f) : (range f).Infinite

Full source

theorem infinite_range_of_injective [Infinite α] {f : α → β} (hi : Injective f) :
    (range f).Infinite := by
  rw [← image_univ, infinite_image_iff hi.injOn]
  exact infinite_univ

Range of an injective function on an infinite type is infinite

Informal description

If $\alpha$ is an infinite type and $f \colon \alpha \to \beta$ is an injective function, then the range of $f$ is infinite.

Set.infinite_of_injective_forall_mem theorem

[Infinite α] {s : Set β} {f : α → β} (hi : Injective f) (hf : ∀ x : α, f x ∈ s) : s.Infinite

Full source

theorem infinite_of_injective_forall_mem [Infinite α] {s : Set β} {f : α → β} (hi : Injective f)
    (hf : ∀ x : α, f x ∈ s) : s.Infinite := by
  rw [← range_subset_iff] at hf
  exact (infinite_range_of_injective hi).mono hf

Infinite Image of Injective Function on Infinite Domain

Informal description

Let $\alpha$ be an infinite type and $s$ a subset of $\beta$. If there exists an injective function $f \colon \alpha \to \beta$ such that $f(x) \in s$ for all $x \in \alpha$, then $s$ is infinite.

Set.not_injOn_infinite_finite_image theorem

{f : α → β} {s : Set α} (h_inf : s.Infinite) (h_fin : (f '' s).Finite) : ¬InjOn f s

Full source

theorem not_injOn_infinite_finite_image {f : α → β} {s : Set α} (h_inf : s.Infinite)
    (h_fin : (f '' s).Finite) : ¬InjOn f s := by
  have : Finite (f '' s) := finite_coe_iff.mpr h_fin
  have : Infinite s := infinite_coe_iff.mpr h_inf
  have h := not_injective_infinite_finite
            ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)
  contrapose! h
  rwa [injective_codRestrict, ← injOn_iff_injective]

Non-injectivity of functions with infinite domain and finite image

Informal description

For any function $f : \alpha \to \beta$ and any infinite subset $s \subseteq \alpha$, if the image $f(s)$ is finite, then $f$ is not injective on $s$.

Set.infinite_of_forall_exists_gt theorem

(h : ∀ a, ∃ b ∈ s, a < b) : s.Infinite

Full source

theorem infinite_of_forall_exists_gt (h : ∀ a, ∃ b ∈ s, a < b) : s.Infinite := by
  inhabit α
  set f : ℕ → α := fun n => Nat.recOn n (h default).choose fun _ a => (h a).choose
  have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
  exact infinite_of_injective_forall_mem
    (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf

Infinite Set Characterized by Existence of Larger Elements

Informal description

For any set $s$ in a type with an order, if for every element $a$ there exists an element $b \in s$ such that $a < b$, then $s$ is infinite.

Set.infinite_of_forall_exists_lt theorem

(h : ∀ a, ∃ b ∈ s, b < a) : s.Infinite

Full source

theorem infinite_of_forall_exists_lt (h : ∀ a, ∃ b ∈ s, b < a) : s.Infinite :=
  infinite_of_forall_exists_gt (α := αᵒᵈ) h

Infinite Set Characterized by Existence of Smaller Elements

Informal description

For any set $s$ in a type with an order, if for every element $a$ there exists an element $b \in s$ such that $b < a$, then $s$ is infinite.

Set.finite_isTop theorem

(α : Type*) [PartialOrder α] : {x : α | IsTop x}.Finite

Full source

theorem finite_isTop (α : Type*) [PartialOrder α] : { x : α | IsTop x }.Finite :=
  (subsingleton_isTop α).finite

Finiteness of Top Elements in a Partially Ordered Set

Informal description

For any type $\alpha$ equipped with a partial order, the set of top elements (i.e., elements that are greater than or equal to all other elements in $\alpha$) is finite.

Set.finite_isBot theorem

(α : Type*) [PartialOrder α] : {x : α | IsBot x}.Finite

Full source

theorem finite_isBot (α : Type*) [PartialOrder α] : { x : α | IsBot x }.Finite :=
  (subsingleton_isBot α).finite

Finiteness of Bottom Elements in a Partially Ordered Set

Informal description

For any type $\alpha$ equipped with a partial order, the set of bottom elements (i.e., elements that are less than or equal to all other elements in $\alpha$) is finite.

Set.Infinite.exists_lt_map_eq_of_mapsTo theorem

 [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

Full source

theorem Infinite.exists_lt_map_eq_of_mapsTo [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 :=
  let ⟨x, hx, y, hy, hxy, hf⟩ := hs.exists_ne_map_eq_of_mapsTo hf ht
  hxy.lt_or_lt.elim (fun hxy => ⟨x, hx, y, hy, hxy, hf⟩) fun hyx => ⟨y, hy, x, hx, hyx, hf.symm⟩

Infinite Domain and Finite Codomain Imply Non-Injective Mapping with Order Condition

Informal description

Let $\alpha$ be a linearly ordered type, $s \subseteq \alpha$ be an infinite set, $t \subseteq \beta$ be a finite set, and $f \colon \alpha \to \beta$ be a function that maps $s$ into $t$. Then there exist elements $x, y \in s$ with $x < y$ such that $f(x) = f(y)$.

Set.Finite.exists_lt_map_eq_of_forall_mem theorem

 [LinearOrder α] [Infinite α] {t : Set β} {f : α → β} (hf : ∀ a, f a ∈ t) (ht : t.Finite) : ∃ a b, a < b ∧ f a = f b

Full source

theorem Finite.exists_lt_map_eq_of_forall_mem [LinearOrder α] [Infinite α] {t : Set β} {f : α → β}
    (hf : ∀ a, f a ∈ t) (ht : t.Finite) : ∃ a b, a < b ∧ f a = f b := by
  rw [← mapsTo_univ_iff] at hf
  obtain ⟨a, -, b, -, h⟩ := infinite_univ.exists_lt_map_eq_of_mapsTo hf ht
  exact ⟨a, b, h⟩

Infinite domain and finite codomain imply non-injective mapping with order condition (universal version)

Informal description

Let $\alpha$ be an infinite linearly ordered type, $t$ a finite subset of $\beta$, and $f \colon \alpha \to \beta$ a function such that $f(a) \in t$ for all $a \in \alpha$. Then there exist elements $a, b \in \alpha$ with $a < b$ such that $f(a) = f(b)$.

Set.finite_range_findGreatest theorem

{P : α → ℕ → Prop} [∀ x, DecidablePred (P x)] {b : ℕ} : (range fun x => Nat.findGreatest (P x) b).Finite

Full source

theorem finite_range_findGreatest {P : α → ℕ → Prop} [∀ x, DecidablePred (P x)] {b : ℕ} :
    (range fun x => Nat.findGreatest (P x) b).Finite :=
  (finite_le_nat b).subset <| range_subset_iff.2 fun _ => Nat.findGreatest_le _

Finiteness of Range of `findGreatest` Function

Informal description

For any predicate $P : \alpha \to \mathbb{N} \to \text{Prop}$ with decidable values and any natural number $b$, the range of the function $x \mapsto \text{Nat.findGreatest } (P x) b$ is a finite set.

Set.Finite.exists_maximal_wrt theorem

 [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite) (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

Full source

theorem Finite.exists_maximal_wrt [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite)
    (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a' := by
  induction s, h using Set.Finite.induction_on with
  | empty => exact absurd hs not_nonempty_empty
  | @insert a s his _ ih =>
    rcases s.eq_empty_or_nonempty with h | h
    · use a
      simp [h]
    rcases ih h with ⟨b, hb, ih⟩
    by_cases h : f b ≤ f a
    · refine ⟨a, Set.mem_insert _ _, fun c hc hac => le_antisymm hac ?_⟩
      rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
      · rfl
      · rwa [← ih c hcs (le_trans h hac)]
    · refine ⟨b, Set.mem_insert_of_mem _ hb, fun c hc hbc => ?_⟩
      rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
      · exact (h hbc).elim
      · exact ih c hcs hbc

Existence of Maximal Elements under a Function on Finite Sets

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a partial order. Given a function $f : \alpha \to \beta$, a finite nonempty subset $s \subseteq \alpha$, there exists an element $a \in s$ such that for all $a' \in s$, if $f(a) \leq f(a')$ then $f(a) = f(a')$.

Set.Finite.exists_maximal_wrt' theorem

 [PartialOrder β] (f : α → β) (s : Set α) (h : (f '' s).Finite) (hs : s.Nonempty) :
  (∃ a ∈ s, ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a')

Full source

/-- A version of `Finite.exists_maximal_wrt` with the (weaker) hypothesis that the image of `s`
  is finite rather than `s` itself. -/
theorem Finite.exists_maximal_wrt' [PartialOrder β] (f : α → β) (s : Set α) (h : (f '' s).Finite)
    (hs : s.Nonempty) : (∃ a ∈ s, ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a') := by
  obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximal_wrt id (f '' s) h (hs.image f)
  exact ⟨a, ha, fun a' ha' hf ↦ hmax _ (mem_image_of_mem f ha') hf⟩

Existence of Maximal Elements under a Function with Finite Image

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a partial order. Given a function $f : \alpha \to \beta$ and a nonempty subset $s \subseteq \alpha$ such that the image $f(s)$ is finite, there exists an element $a \in s$ such that for all $a' \in s$, if $f(a) \leq f(a')$ then $f(a) = f(a')$.

Set.Finite.exists_minimal_wrt theorem

 [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite) (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, f a' ≤ f a → f a = f a'

Full source

theorem Finite.exists_minimal_wrt [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite)
    (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, f a' ≤ f a → f a = f a' :=
  Finite.exists_maximal_wrt (β := βᵒᵈ) f s h hs

Existence of Minimal Elements under a Function on Finite Sets

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a partial order. Given a function $f : \alpha \to \beta$ and a finite nonempty subset $s \subseteq \alpha$, there exists an element $a \in s$ such that for all $a' \in s$, if $f(a') \leq f(a)$ then $f(a') = f(a)$.

Set.Finite.exists_minimal_wrt' theorem

 [PartialOrder β] (f : α → β) (s : Set α) (h : (f '' s).Finite) (hs : s.Nonempty) :
  (∃ a ∈ s, ∀ (a' : α), a' ∈ s → f a' ≤ f a → f a = f a')

Full source

/-- A version of `Finite.exists_minimal_wrt` with the (weaker) hypothesis that the image of `s`
  is finite rather than `s` itself. -/
lemma Finite.exists_minimal_wrt' [PartialOrder β] (f : α → β) (s : Set α) (h : (f '' s).Finite)
    (hs : s.Nonempty) : (∃ a ∈ s, ∀ (a' : α), a' ∈ s → f a' ≤ f a → f a = f a') :=
  Set.Finite.exists_maximal_wrt' (β := βᵒᵈ) f s h hs

Existence of Minimal Elements under a Function with Finite Image

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a partial order. Given a function $f : \alpha \to \beta$ and a nonempty subset $s \subseteq \alpha$ such that the image $f(s)$ is finite, there exists an element $a \in s$ such that for all $a' \in s$, if $f(a') \leq f(a)$ then $f(a') = f(a)$.

Finset.exists_card_eq theorem

[Infinite α] : ∀ n : ℕ, ∃ s : Finset α, s.card = n

Full source

lemma exists_card_eq [Infinite α] : ∀ n : ℕ, ∃ s : Finset α, s.card = n
  | 0 => ⟨∅, card_empty⟩
  | n + 1 => by
    classical
    obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_not_mem
    exact ⟨insert a s, card_insert_of_not_mem ha⟩

Existence of Finite Subsets of Any Cardinality in Infinite Types

Informal description

For any infinite type $\alpha$ and any natural number $n$, there exists a finite subset $s$ of $\alpha$ (represented as a finset) with cardinality exactly $n$.

Finite.of_forall_not_lt_lt theorem

(h : ∀ ⦃x y z : α⦄, x < y → y < z → False) : Finite α

Full source

/-- If a linear order does not contain any triple of elements `x < y < z`, then this type
is finite. -/
lemma Finite.of_forall_not_lt_lt (h : ∀ ⦃x y z : α⦄, x < y → y < z → False) : Finite α := by
  nontriviality α
  rcases exists_pair_ne α with ⟨x, y, hne⟩
  refine @Finite.of_fintype α ⟨{x, y}, fun z => ?_⟩
  simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y

Finiteness from Absence of Three-Term Strictly Increasing Chains in Linear Orders

Informal description

If a linearly ordered type $\alpha$ satisfies the condition that for any three elements $x, y, z$ with $x < y < z$, the relation is false (i.e., there are no three strictly increasing elements), then $\alpha$ is finite.

Set.finite_of_forall_not_lt_lt theorem

(h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) : Set.Finite s

Full source

/-- If a set `s` does not contain any triple of elements `x < y < z`, then `s` is finite. -/
lemma Set.finite_of_forall_not_lt_lt (h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) :
    Set.Finite s :=
  @Set.toFinite _ s <| Finite.of_forall_not_lt_lt <| by simpa only [SetCoe.forall'] using h

Finiteness from Absence of Three-Term Strictly Increasing Chains in a Set

Informal description

For any set $s$ in a linearly ordered type $\alpha$, if there do not exist elements $x, y, z \in s$ such that $x < y < z$, then $s$ is finite.

Mathlib.Data.Set.Finite.Basic

Main definitions

Implementation

Tags