doc-next-gen

Mathlib.Data.Fintype.Card

Module docstring

{"# Cardinalities of finite types

This file defines the cardinality Fintype.card α as the number of elements in (univ : Finset α). We also include some elementary results on the values of Fintype.card on specific types.

Main declarations

  • Fintype.card α: Cardinality of a fintype. Equal to Finset.univ.card.
  • Finite.surjective_of_injective: an injective function from a finite type to itself is also surjective.

"}

Fintype.card definition
(α) [Fintype α] : ℕ
Full source 
/-- `card α` is the number of elements in `α`, defined when `α` is a fintype. -/
def card (α) [Fintype α] : ℕ :=
  (@univ α _).card
Cardinality of a finite type
Informal description
The function `Fintype.card α` returns the number of elements in a finite type `α`, defined as the cardinality of the universal finite set `univ : Finset α` containing all elements of `α`.
Fintype.subtype_card theorem
{p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) : @card { x // p x } (Fintype.subtype s H) = #s
Full source 
theorem subtype_card {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ sx ∈ s ↔ p x) :
    @card { x // p x } (Fintype.subtype s H) = #s :=
  Multiset.card_pmap _ _ _
Cardinality of Subtype Equals Cardinality of Defining Finset
Informal description
For any predicate $p : \alpha \to \mathrm{Prop}$ and finite set $s$ of elements of type $\alpha$ such that $x \in s$ if and only if $p(x)$ holds, the cardinality of the subtype $\{x \mid p(x)\}$ (equipped with the finite type structure derived from $s$) is equal to the cardinality of $s$. That is, $|\{x \mid p(x)\}| = |s|$.
Fintype.card_of_subtype theorem
{p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ s ↔ p x) [Fintype { x // p x }] : card { x // p x } = #s
Full source 
theorem card_of_subtype {p : α → Prop} (s : Finset α) (H : ∀ x : α, x ∈ sx ∈ s ↔ p x)
    [Fintype { x // p x }] : card { x // p x } = #s := by
  rw [← subtype_card s H]
  congr!
Cardinality of Subtype Equals Cardinality of Defining Finset
Informal description
For any predicate $p : \alpha \to \mathrm{Prop}$ and finite set $s$ of elements of type $\alpha$ such that $x \in s$ if and only if $p(x)$ holds, the cardinality of the subtype $\{x \mid p(x)\}$ (equipped with a finite type structure) is equal to the cardinality of $s$, i.e., $|\{x \mid p(x)\}| = |s|$.
Fintype.card_ofFinset theorem
{p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : @Fintype.card p (ofFinset s H) = #s
Full source 
@[simp]
theorem card_ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ sx ∈ s ↔ x ∈ p) :
    @Fintype.card p (ofFinset s H) = #s :=
  Fintype.subtype_card s H
Cardinality of Set Constructed from Finset Equals Finset Cardinality
Informal description
For any set $p$ over a type $\alpha$ and any finite set $s$ of elements of $\alpha$ such that $x \in s$ if and only if $x \in p$, the cardinality of $p$ (equipped with the finite type structure derived from $s$) is equal to the cardinality of $s$. That is, $|p| = |s|$.
Fintype.card_of_finset' theorem
{p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) [Fintype p] : Fintype.card p = #s
Full source 
theorem card_of_finset' {p : Set α} (s : Finset α) (H : ∀ x, x ∈ sx ∈ s ↔ x ∈ p) [Fintype p] :
    Fintype.card p = #s := by rw [← card_ofFinset s H]; congr!
Cardinality of Set Defined by Finset Equals Finset Cardinality
Informal description
For any set $p$ over a type $\alpha$ and any finite set $s$ of elements of $\alpha$ such that $x \in s$ if and only if $x \in p$, the cardinality of $p$ (when equipped with a finite type structure) is equal to the cardinality of $s$, i.e., $|p| = |s|$.
Fintype.ofEquiv_card theorem
[Fintype α] (f : α ≃ β) : @card β (ofEquiv α f) = card α
Full source 
theorem ofEquiv_card [Fintype α] (f : α ≃ β) : @card β (ofEquiv α f) = card α :=
  Multiset.card_map _ _
Cardinality Preservation under Type Equivalence
Informal description
For any finite type $\alpha$ and any equivalence (bijection) $f : \alpha \simeq \beta$, the cardinality of $\beta$ (equipped with the finite type structure derived via $f$) is equal to the cardinality of $\alpha$, i.e., $|\beta| = |\alpha|$.
Fintype.card_congr theorem
{α β} [Fintype α] [Fintype β] (f : α ≃ β) : card α = card β
Full source 
theorem card_congr {α β} [Fintype α] [Fintype β] (f : α ≃ β) : card α = card β := by
  rw [← ofEquiv_card f]; congr!
Cardinality Equality under Type Equivalence for Finite Types
Informal description
For any finite types $\alpha$ and $\beta$, if there exists an equivalence (bijection) $f : \alpha \simeq \beta$, then the cardinalities of $\alpha$ and $\beta$ are equal, i.e., $|\alpha| = |\beta|$.
Fintype.card_congr' theorem
{α β} [Fintype α] [Fintype β] (h : α = β) : card α = card β
Full source 
@[congr]
theorem card_congr' {α β} [Fintype α] [Fintype β] (h : α = β) : card α = card β :=
  card_congr (by rw [h])
Cardinality Equality for Equal Finite Types
Informal description
For any finite types $\alpha$ and $\beta$, if $\alpha$ is equal to $\beta$ (i.e., $\alpha = \beta$), then their cardinalities are equal, i.e., $|\alpha| = |\beta|$.
Fintype.card_ofSubsingleton theorem
(a : α) [Subsingleton α] : @Fintype.card _ (ofSubsingleton a) = 1
Full source 
/-- Note: this lemma is specifically about `Fintype.ofSubsingleton`. For a statement about
arbitrary `Fintype` instances, use either `Fintype.card_le_one_iff_subsingleton` or
`Fintype.card_unique`. -/
theorem card_ofSubsingleton (a : α) [Subsingleton α] : @Fintype.card _ (ofSubsingleton a) = 1 :=
  rfl
Cardinality of a Subsingleton Type is One
Informal description
For any subsingleton type $\alpha$ (i.e., a type with at most one element) and any element $a \in \alpha$, the cardinality of $\alpha$ when equipped with the finite type structure `Fintype.ofSubsingleton a` is equal to $1$.
Fintype.card_ofIsEmpty theorem
[IsEmpty α] : @Fintype.card α Fintype.ofIsEmpty = 0
Full source 
/-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
arbitrary `Fintype` instances, use `Fintype.card_eq_zero`. -/
theorem card_ofIsEmpty [IsEmpty α] : @Fintype.card α Fintype.ofIsEmpty = 0 :=
  rfl
Cardinality of an Empty Type is Zero
Informal description
For any empty type $\alpha$ (i.e., a type with no elements), the cardinality of $\alpha$ under the finite type structure `Fintype.ofIsEmpty` is $0$.
Set.toFinset_card theorem
{α : Type*} (s : Set α) [Fintype s] : s.toFinset.card = Fintype.card s
Full source 
@[simp]
theorem toFinset_card {α : Type*} (s : Set α) [Fintype s] : s.toFinset.card = Fintype.card s :=
  Multiset.card_map Subtype.val Finset.univ.val
Cardinality Preservation in Set-to-Finset Conversion
Informal description
For any set $s$ in a finite type $\alpha$, the cardinality of the finite set obtained by converting $s$ to a `Finset` is equal to the cardinality of $s$ as a finite type, i.e., $|s.\text{toFinset}| = \text{card}(s)$.
Finset.card_univ theorem
[Fintype α] : #(univ : Finset α) = Fintype.card α
Full source 
@[simp]
theorem Finset.card_univ [Fintype α] : #(univ : Finset α) = Fintype.card α := rfl
Cardinality of Universal Finite Set Equals Cardinality of Finite Type
Informal description
For any finite type $\alpha$, the cardinality of the universal finite set `univ : Finset α` is equal to the cardinality of the type $\alpha$ itself, i.e., $|\text{univ}| = \text{card}(\alpha)$.
Finset.card_eq_iff_eq_univ theorem
[Fintype α] (s : Finset α) : #s = Fintype.card α ↔ s = univ
Full source 
theorem Finset.card_eq_iff_eq_univ [Fintype α] (s : Finset α) : #s#s = Fintype.card α ↔ s = univ :=
  ⟨s.eq_univ_of_card, by
    rintro rfl
    exact Finset.card_univ⟩
Finite Set Equals Universal Set iff Cardinalities Match
Informal description
For a finite type $\alpha$ and a finite set $s$ of elements of $\alpha$, the cardinality of $s$ equals the cardinality of $\alpha$ if and only if $s$ is the universal set containing all elements of $\alpha$. In other words, $|s| = |\alpha| \leftrightarrow s = \text{univ}$.
Finset.card_le_univ theorem
[Fintype α] (s : Finset α) : #s ≤ Fintype.card α
Full source 
theorem Finset.card_le_univ [Fintype α] (s : Finset α) : #s ≤ Fintype.card α :=
  card_le_card (subset_univ s)
Cardinality of Subset Bounded by Universal Set in Finite Types
Informal description
For any finite subset $s$ of a finite type $\alpha$, the cardinality of $s$ is less than or equal to the cardinality of $\alpha$, i.e., $|s| \leq |\alpha|$.
Finset.card_lt_univ_of_not_mem theorem
[Fintype α] {s : Finset α} {x : α} (hx : x ∉ s) : #s < Fintype.card α
Full source 
theorem Finset.card_lt_univ_of_not_mem [Fintype α] {s : Finset α} {x : α} (hx : x ∉ s) :
    #s < Fintype.card α :=
  card_lt_card ⟨subset_univ s, not_forall.2 ⟨x, fun hx' => hx (hx' <| mem_univ x)⟩⟩
Cardinality Inequality for Proper Subset of Finite Type
Informal description
For any finite type $\alpha$, finite subset $s \subseteq \alpha$, and element $x \in \alpha$ such that $x \notin s$, the cardinality of $s$ is strictly less than the cardinality of $\alpha$ (i.e., $|s| < |\alpha|$).
Finset.card_lt_iff_ne_univ theorem
[Fintype α] (s : Finset α) : #s < Fintype.card α ↔ s ≠ Finset.univ
Full source 
theorem Finset.card_lt_iff_ne_univ [Fintype α] (s : Finset α) :
    #s#s < Fintype.card α ↔ s ≠ Finset.univ :=
  s.card_le_univ.lt_iff_ne.trans (not_congr s.card_eq_iff_eq_univ)
Cardinality Strictly Less Than Universal Set iff Proper Subset
Informal description
For a finite type $\alpha$ and a finite subset $s \subseteq \alpha$, the cardinality of $s$ is strictly less than the cardinality of $\alpha$ if and only if $s$ is not the universal set of $\alpha$. In other words, $|s| < |\alpha| \leftrightarrow s \neq \text{univ}$.
Finset.card_compl_lt_iff_nonempty theorem
[Fintype α] [DecidableEq α] (s : Finset α) : #sᶜ < Fintype.card α ↔ s.Nonempty
Full source 
theorem Finset.card_compl_lt_iff_nonempty [Fintype α] [DecidableEq α] (s : Finset α) :
    #sᶜ#sᶜ < Fintype.card α ↔ s.Nonempty :=
  sᶜ.card_lt_iff_ne_univ.trans s.compl_ne_univ_iff_nonempty
Cardinality of Complement is Less Than Universal Set iff Subset is Nonempty
Informal description
For a finite type $\alpha$ with decidable equality and a finite subset $s \subseteq \alpha$, the cardinality of the complement $s^c$ is strictly less than the cardinality of $\alpha$ if and only if $s$ is nonempty. In other words, $|s^c| < |\alpha| \leftrightarrow s \neq \emptyset$.
Finset.card_univ_diff theorem
[DecidableEq α] [Fintype α] (s : Finset α) : #(univ \ s) = Fintype.card α - #s
Full source 
theorem Finset.card_univ_diff [DecidableEq α] [Fintype α] (s : Finset α) :
    #(univ \ s) = Fintype.card α - #s :=
  Finset.card_sdiff (subset_univ s)
Cardinality of Set Difference from Universal Finite Set: $|\text{univ} \setminus s| = |\alpha| - |s|$
Informal description
For any finite type $\alpha$ with decidable equality and any finite subset $s$ of $\alpha$, the cardinality of the set difference between the universal finite set $\text{univ}$ and $s$ is equal to the difference between the cardinality of $\alpha$ and the cardinality of $s$, i.e., $|\text{univ} \setminus s| = |\alpha| - |s|$.
Finset.card_compl theorem
[DecidableEq α] [Fintype α] (s : Finset α) : #sᶜ = Fintype.card α - #s
Full source 
theorem Finset.card_compl [DecidableEq α] [Fintype α] (s : Finset α) : #sᶜ = Fintype.card α - #s :=
  Finset.card_univ_diff s
Cardinality of Complement: $|s^c| = |\alpha| - |s|$
Informal description
For any finite type $\alpha$ with decidable equality and any finite subset $s$ of $\alpha$, the cardinality of the complement of $s$ is equal to the difference between the cardinality of $\alpha$ and the cardinality of $s$, i.e., $|s^c| = |\alpha| - |s|$.
Finset.card_add_card_compl theorem
[DecidableEq α] [Fintype α] (s : Finset α) : #s + #sᶜ = Fintype.card α
Full source 
@[simp]
theorem Finset.card_add_card_compl [DecidableEq α] [Fintype α] (s : Finset α) :
    #s + #sᶜ = Fintype.card α := by
  rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]
Cardinality Sum of Set and Complement Equals Type Size
Informal description
For any finite type $\alpha$ with decidable equality and any finite subset $s$ of $\alpha$, the sum of the cardinalities of $s$ and its complement $s^c$ equals the cardinality of $\alpha$, i.e., $|s| + |s^c| = |\alpha|$.
Finset.card_compl_add_card theorem
[DecidableEq α] [Fintype α] (s : Finset α) : #sᶜ + #s = Fintype.card α
Full source 
@[simp]
theorem Finset.card_compl_add_card [DecidableEq α] [Fintype α] (s : Finset α) :
    #sᶜ + #s = Fintype.card α := by
  rw [Nat.add_comm, card_add_card_compl]
Complement and Set Cardinality Sum to Type Size
Informal description
For any finite type $\alpha$ with decidable equality and any finite subset $s$ of $\alpha$, the sum of the cardinalities of the complement of $s$ and $s$ itself equals the cardinality of $\alpha$, i.e., $|s^c| + |s| = |\alpha|$.
Fintype.card_compl_set theorem
[Fintype α] (s : Set α) [Fintype s] [Fintype (↥sᶜ : Sort _)] : Fintype.card (↥sᶜ : Sort _) = Fintype.card α - Fintype.card s
Full source 
theorem Fintype.card_compl_set [Fintype α] (s : Set α) [Fintype s] [Fintype (↥sᶜ : Sort _)] :
    Fintype.card (↥sᶜ : Sort _) = Fintype.card α - Fintype.card s := by
  classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
Cardinality of Complement Set: $|s^c| = |\alpha| - |s|$
Informal description
For a finite type $\alpha$ and a subset $s \subseteq \alpha$ that is finite (with its complement $s^c$ also finite), the cardinality of the complement set $s^c$ is equal to the difference between the cardinality of $\alpha$ and the cardinality of $s$, i.e., $|s^c| = |\alpha| - |s|$.
Fintype.card_empty theorem
: Fintype.card Empty = 0
Full source 
theorem Fintype.card_empty : Fintype.card Empty = 0 :=
  rfl
Cardinality of the Empty Type is Zero
Informal description
The cardinality of the empty type $\text{Empty}$ is $0$, i.e., $\text{card}(\text{Empty}) = 0$.
Fintype.card_pempty theorem
: Fintype.card PEmpty = 0
Full source 
theorem Fintype.card_pempty : Fintype.card PEmpty = 0 :=
  rfl
Cardinality of Empty Type is Zero
Informal description
The cardinality of the empty type `PEmpty` is $0$, i.e., $\text{card}(\text{PEmpty}) = 0$.
Fintype.card_unit theorem
: Fintype.card Unit = 1
Full source 
theorem Fintype.card_unit : Fintype.card Unit = 1 :=
  rfl
Cardinality of the Unit Type is One
Informal description
The cardinality of the unit type `Unit` is $1$, i.e., $\text{card}(\text{Unit}) = 1$.
Fintype.card_punit theorem
: Fintype.card PUnit = 1
Full source 
@[simp]
theorem Fintype.card_punit : Fintype.card PUnit = 1 :=
  rfl
Cardinality of Pointed Unit Type is One
Informal description
The cardinality of the pointed unit type `PUnit` is $1$, i.e., $\text{card}(\text{PUnit}) = 1$.
Fintype.card_bool theorem
: Fintype.card Bool = 2
Full source 
@[simp]
theorem Fintype.card_bool : Fintype.card Bool = 2 :=
  rfl
Cardinality of Boolean Type is Two
Informal description
The cardinality of the Boolean type is $2$, i.e., $\text{card}(\text{Bool}) = 2$.
Fintype.card_ulift theorem
(α : Type*) [Fintype α] : Fintype.card (ULift α) = Fintype.card α
Full source 
@[simp]
theorem Fintype.card_ulift (α : Type*) [Fintype α] : Fintype.card (ULift α) = Fintype.card α :=
  Fintype.ofEquiv_card _
Cardinality Preservation under Universe Lifting
Informal description
For any finite type $\alpha$, the cardinality of the lifted type $\text{ULift}\,\alpha$ is equal to the cardinality of $\alpha$, i.e., $|\text{ULift}\,\alpha| = |\alpha|$.
Fintype.card_plift theorem
(α : Type*) [Fintype α] : Fintype.card (PLift α) = Fintype.card α
Full source 
@[simp]
theorem Fintype.card_plift (α : Type*) [Fintype α] : Fintype.card (PLift α) = Fintype.card α :=
  Fintype.ofEquiv_card _
Cardinality Preservation under PLift
Informal description
For any finite type $\alpha$, the cardinality of the lifted type $\mathrm{PLift}\,\alpha$ is equal to the cardinality of $\alpha$, i.e., $|\mathrm{PLift}\,\alpha| = |\alpha|$.
Fintype.card_orderDual theorem
(α : Type*) [Fintype α] : Fintype.card αᵒᵈ = Fintype.card α
Full source 
@[simp]
theorem Fintype.card_orderDual (α : Type*) [Fintype α] : Fintype.card αᵒᵈ = Fintype.card α :=
  rfl
Cardinality Preservation under Order Dual
Informal description
For any finite type $\alpha$, the cardinality of its order dual $\alpha^{\mathrm{op}}$ is equal to the cardinality of $\alpha$, i.e., $|\alpha^{\mathrm{op}}| = |\alpha|$.
Fintype.card_lex theorem
(α : Type*) [Fintype α] : Fintype.card (Lex α) = Fintype.card α
Full source 
@[simp]
theorem Fintype.card_lex (α : Type*) [Fintype α] : Fintype.card (Lex α) = Fintype.card α :=
  rfl
Cardinality Preservation under Lexicographic Order
Informal description
For any finite type $\alpha$, the cardinality of $\alpha$ equipped with the lexicographic order is equal to the cardinality of $\alpha$, i.e., $|\text{Lex}(\alpha)| = |\alpha|$.
Fintype.card_setUniv theorem
[Fintype α] {h : Fintype (Set.univ : Set α)} : Fintype.card (Set.univ : Set α) = Fintype.card α
Full source 
@[simp]
theorem Fintype.card_setUniv [Fintype α] {h : Fintype (Set.univ : Set α)} :
    Fintype.card (Set.univ : Set α) = Fintype.card α := by
  apply Fintype.card_of_finset'
  simp
Cardinality of Universal Set Equals Cardinality of Finite Type
Informal description
For any finite type $\alpha$, the cardinality of the universal set $\mathrm{Set.univ} : \mathrm{Set}\,\alpha$ (when equipped with a finite type structure) is equal to the cardinality of $\alpha$, i.e., $|\mathrm{Set.univ}| = |\alpha|$.
Fintype.card_subtype_true theorem
[Fintype α] {h : Fintype { _a : α // True }} : @Fintype.card { _a // True } h = Fintype.card α
Full source 
@[simp]
theorem Fintype.card_subtype_true [Fintype α] {h : Fintype {_a : α // True}} :
    @Fintype.card {_a // True} h = Fintype.card α := by
  apply Fintype.card_of_subtype
  simp
Cardinality of Trivial Subtype Equals Cardinality of Original Type
Informal description
For any finite type $\alpha$, the cardinality of the subtype $\{a : \alpha \mid \text{True}\}$ (equipped with a finite type structure) is equal to the cardinality of $\alpha$, i.e., $|\{a : \alpha \mid \text{True}\}| = |\alpha|$.
Fintype.sumLeft definition
{α β} [Fintype (α ⊕ β)] : Fintype α
Full source 
/-- Given that `α ⊕ β` is a fintype, `α` is also a fintype. This is non-computable as it uses
that `Sum.inl` is an injection, but there's no clear inverse if `α` is empty. -/
noncomputable def Fintype.sumLeft {α β} [Fintype (α ⊕ β)] : Fintype α :=
  Fintype.ofInjective (Sum.inl : α → α ⊕ β) Sum.inl_injective
Finite type from left summand of finite sum type
Informal description
Given that the sum type $\alpha \oplus \beta$ is finite, the type $\alpha$ is also finite. This is constructed using the injective function $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$.
Fintype.sumRight definition
{α β} [Fintype (α ⊕ β)] : Fintype β
Full source 
/-- Given that `α ⊕ β` is a fintype, `β` is also a fintype. This is non-computable as it uses
that `Sum.inr` is an injection, but there's no clear inverse if `β` is empty. -/
noncomputable def Fintype.sumRight {α β} [Fintype (α ⊕ β)] : Fintype β :=
  Fintype.ofInjective (Sum.inr : β → α ⊕ β) Sum.inr_injective
Finiteness of the right summand
Informal description
Given that the sum type $\alpha \oplus \beta$ is finite, the type $\beta$ is also finite. This is proved by constructing an injective function from $\beta$ to $\alpha \oplus \beta$ (using the right injection $\text{Sum.inr}$) and applying the fact that the domain of an injective function into a finite type is finite.
Finite.exists_univ_list theorem
(α) [Finite α] : ∃ l : List α, l.Nodup ∧ ∀ x : α, x ∈ l
Full source 
theorem Finite.exists_univ_list (α) [Finite α] : ∃ l : List α, l.Nodup ∧ ∀ x : α, x ∈ l := by
  cases nonempty_fintype α
  obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1
  have := And.intro (@univ α _).2 (@mem_univ_val α _)
  exact ⟨_, by rwa [← e] at this⟩
Existence of Duplicate-Free Enumeration for Finite Types
Informal description
For any finite type $\alpha$, there exists a list $l$ of elements of $\alpha$ such that $l$ has no duplicate elements and every element of $\alpha$ appears in $l$.
List.Nodup.length_le_card theorem
{α : Type*} [Fintype α] {l : List α} (h : l.Nodup) : l.length ≤ Fintype.card α
Full source 
theorem List.Nodup.length_le_card {α : Type*} [Fintype α] {l : List α} (h : l.Nodup) :
    l.length ≤ Fintype.card α := by
  classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ
Length of Duplicate-Free List Bounded by Cardinality of Finite Type
Informal description
For any finite type $\alpha$ and any duplicate-free list $l$ of elements of $\alpha$, the length of $l$ is less than or equal to the cardinality of $\alpha$, i.e., $|l| \leq |\alpha|$.
Fintype.card_le_of_injective theorem
(f : α → β) (hf : Function.Injective f) : card α ≤ card β
Full source 
theorem card_le_of_injective (f : α → β) (hf : Function.Injective f) : card α ≤ card β :=
  Finset.card_le_card_of_injOn f (fun _ _ => Finset.mem_univ _) fun _ _ _ _ h => hf h
Cardinality Inequality for Injective Functions between Finite Types
Informal description
For any injective function $f : \alpha \to \beta$ between finite types $\alpha$ and $\beta$, the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$.
Fintype.card_le_of_embedding theorem
(f : α ↪ β) : card α ≤ card β
Full source 
theorem card_le_of_embedding (f : α ↪ β) : card α ≤ card β :=
  card_le_of_injective f f.2
Cardinality Inequality for Injective Embeddings between Finite Types
Informal description
For any injective function $f : \alpha \hookrightarrow \beta$ between finite types $\alpha$ and $\beta$, the cardinality of $\alpha$ is less than or equal to the cardinality of $\beta$, i.e., $|\alpha| \leq |\beta|$.
Fintype.card_lt_of_injective_of_not_mem theorem
(f : α → β) (h : Function.Injective f) {b : β} (w : b ∉ Set.range f) : card α < card β
Full source 
theorem card_lt_of_injective_of_not_mem (f : α → β) (h : Function.Injective f) {b : β}
    (w : b ∉ Set.range f) : card α < card β :=
  calc
    card α = (univ.map ⟨f, h⟩).card := (card_map _).symm
    _ < card β :=
      Finset.card_lt_univ_of_not_mem (x := b) <| by
        rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
Cardinality Strict Inequality for Injective Functions with Non-Member Codomain Element
Informal description
Let $\alpha$ and $\beta$ be finite types. Given an injective function $f : \alpha \to \beta$ and an element $b \in \beta$ such that $b \notin \text{range}(f)$, the cardinality of $\alpha$ is strictly less than the cardinality of $\beta$, i.e., $|\alpha| < |\beta|$.
Fintype.card_lt_of_injective_not_surjective theorem
(f : α → β) (h : Function.Injective f) (h' : ¬Function.Surjective f) : card α < card β
Full source 
theorem card_lt_of_injective_not_surjective (f : α → β) (h : Function.Injective f)
    (h' : ¬Function.Surjective f) : card α < card β :=
  let ⟨_y, hy⟩ := not_forall.1 h'
  card_lt_of_injective_of_not_mem f h hy
Cardinality Strict Inequality for Injective Non-Surjective Functions between Finite Types
Informal description
Let $\alpha$ and $\beta$ be finite types. Given an injective function $f : \alpha \to \beta$ that is not surjective, the cardinality of $\alpha$ is strictly less than the cardinality of $\beta$, i.e., $|\alpha| < |\beta|$.
Fintype.card_le_of_surjective theorem
(f : α → β) (h : Function.Surjective f) : card β ≤ card α
Full source 
theorem card_le_of_surjective (f : α → β) (h : Function.Surjective f) : card β ≤ card α :=
  card_le_of_injective _ (Function.injective_surjInv h)
Cardinality Inequality for Surjective Functions between Finite Types
Informal description
For any surjective function $f : \alpha \to \beta$ between finite types $\alpha$ and $\beta$, the cardinality of $\beta$ is less than or equal to the cardinality of $\alpha$.
Fintype.card_range_le theorem
{α β : Type*} (f : α → β) [Fintype α] [Fintype (Set.range f)] : Fintype.card (Set.range f) ≤ Fintype.card α
Full source 
theorem card_range_le {α β : Type*} (f : α → β) [Fintype α] [Fintype (Set.range f)] :
    Fintype.card (Set.range f) ≤ Fintype.card α :=
  Fintype.card_le_of_surjective (fun a => ⟨f a, by simp⟩) fun ⟨_, a, ha⟩ => ⟨a, by simpa using ha⟩
Cardinality of Range is Bounded by Domain Size in Finite Types
Informal description
For any function $f : \alpha \to \beta$ between finite types $\alpha$ and $\beta$, the cardinality of the range of $f$ is less than or equal to the cardinality of $\alpha$. In other words, $|\mathrm{range}\, f| \leq |\alpha|$.
Fintype.card_range theorem
{α β F : Type*} [FunLike F α β] [EmbeddingLike F α β] (f : F) [Fintype α] [Fintype (Set.range f)] : Fintype.card (Set.range f) = Fintype.card α
Full source 
theorem card_range {α β F : Type*} [FunLike F α β] [EmbeddingLike F α β] (f : F) [Fintype α]
    [Fintype (Set.range f)] : Fintype.card (Set.range f) = Fintype.card α :=
  Eq.symm <| Fintype.card_congr <| Equiv.ofInjective _ <| EmbeddingLike.injective f
Cardinality of Range Equals Domain for Injective Functions on Finite Types
Informal description
Let $\alpha$ and $\beta$ be finite types, and let $F$ be a type with function-like and embedding-like structures from $\alpha$ to $\beta$. For any $f : F$, if both $\alpha$ and the range of $f$ are finite, then the cardinality of the range of $f$ is equal to the cardinality of $\alpha$, i.e., $|\mathrm{range}\, f| = |\alpha|$.
Fintype.card_eq_zero theorem
[IsEmpty α] : card α = 0
Full source 
@[simp] theorem card_eq_zero [IsEmpty α] : card α = 0 :=
  card_eq_zero_iff.2 ‹_›
Cardinality of Empty Finite Type is Zero
Informal description
For any finite type $\alpha$, if $\alpha$ is empty (i.e., `IsEmpty α` holds), then the cardinality of $\alpha$ is zero, i.e., $\text{card}(\alpha) = 0$.
Fintype.cardEqZeroEquivEquivEmpty definition
: card α = 0 ≃ (α ≃ Empty)
Full source 
/-- A `Fintype` with cardinality zero is equivalent to `Empty`. -/
def cardEqZeroEquivEquivEmpty : cardcard α = 0 ≃ (α ≃ Empty) :=
  (Equiv.ofIff card_eq_zero_iff).trans (Equiv.equivEmptyEquiv α).symm
Equivalence between zero cardinality and bijection with the empty type
Informal description
The equivalence between the statement that the cardinality of a finite type $\alpha$ is zero and the existence of a bijection from $\alpha$ to the empty type. This is constructed by combining the equivalence between $\text{card}(\alpha) = 0$ and $\alpha$ being empty with the equivalence between $\alpha$ being empty and $\alpha$ being in bijection with the empty type.
Fintype.card_pos theorem
[h : Nonempty α] : 0 < card α
Full source 
theorem card_pos [h : Nonempty α] : 0 < card α :=
  card_pos_iff.mpr h
Positive Cardinality of Nonempty Finite Types
Informal description
For any nonempty finite type $\alpha$, the cardinality of $\alpha$ is strictly positive, i.e., $0 < \text{card}(\alpha)$.
Fintype.card_ne_zero theorem
[Nonempty α] : card α ≠ 0
Full source 
@[simp]
theorem card_ne_zero [Nonempty α] : cardcard α ≠ 0 :=
  _root_.ne_of_gt card_pos
Nonzero Cardinality of Nonempty Finite Types
Informal description
For any nonempty finite type $\alpha$, the cardinality of $\alpha$ is not zero, i.e., $\text{card}(\alpha) \neq 0$.
Fintype.instNeZeroNatCardOfNonempty instance
[Nonempty α] : NeZero (card α)
Full source 
instance [Nonempty α] : NeZero (card α) := ⟨card_ne_zero⟩
Nonzero Cardinality of Nonempty Finite Types
Informal description
For any nonempty finite type $\alpha$, the cardinality of $\alpha$ is a nonzero natural number.
Fintype.existsUnique_iff_card_one theorem
{α} [Fintype α] (p : α → Prop) [DecidablePred p] : (∃! a : α, p a) ↔ #{x | p x} = 1
Full source 
theorem existsUnique_iff_card_one {α} [Fintype α] (p : α → Prop) [DecidablePred p] :
    (∃! a : α, p a) ↔ #{x | p x} = 1 := by
  rw [Finset.card_eq_one]
  refine exists_congr fun x => ?_
  simp only [forall_true_left, Subset.antisymm_iff, subset_singleton_iff', singleton_subset_iff,
      true_and, and_comm, mem_univ, mem_filter]
Unique Existence in Finite Types is Equivalent to Cardinality One
Informal description
For a finite type $\alpha$ and a decidable predicate $p : \alpha \to \text{Prop}$, there exists a unique element $a \in \alpha$ satisfying $p(a)$ if and only if the cardinality of the subset $\{x \in \alpha \mid p(x)\}$ is equal to 1.
Fintype.two_lt_card_iff theorem
: 2 < card α ↔ ∃ a b c : α, a ≠ b ∧ a ≠ c ∧ b ≠ c
Full source 
nonrec theorem two_lt_card_iff : 2 < card α ↔ ∃ a b c : α, a ≠ b ∧ a ≠ c ∧ b ≠ c := by
  simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and]
Cardinality Greater Than Two Characterization for Finite Types
Informal description
For a finite type $\alpha$, the cardinality of $\alpha$ is greater than 2 if and only if there exist three distinct elements $a, b, c \in \alpha$ such that $a \neq b$, $a \neq c$, and $b \neq c$.
Fintype.card_of_bijective theorem
{f : α → β} (hf : Bijective f) : card α = card β
Full source 
theorem card_of_bijective {f : α → β} (hf : Bijective f) : card α = card β :=
  card_congr (Equiv.ofBijective f hf)
Cardinality Equality under Bijection for Finite Types
Informal description
For any finite types $\alpha$ and $\beta$, if there exists a bijective function $f \colon \alpha \to \beta$, then the cardinalities of $\alpha$ and $\beta$ are equal, i.e., $|\alpha| = |\beta|$.
Finite.surjective_of_injective theorem
{f : α → α} (hinj : Injective f) : Surjective f
Full source 
theorem surjective_of_injective {f : α → α} (hinj : Injective f) : Surjective f := by
  intro x
  have := Classical.propDecidable
  cases nonempty_fintype α
  have h₁ : image f univ = univ :=
    eq_of_subset_of_card_le (subset_univ _)
      ((card_image_of_injective univ hinj).symm ▸ le_rfl)
  have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
  obtain ⟨y, h⟩ := mem_image.1 h₂
  exact ⟨y, h.2⟩
Injective implies surjective for endomorphisms of finite types
Informal description
For any injective function $f \colon \alpha \to \alpha$ on a finite type $\alpha$, $f$ is also surjective.
Finite.injective_iff_surjective theorem
{f : α → α} : Injective f ↔ Surjective f
Full source 
theorem injective_iff_surjective {f : α → α} : InjectiveInjective f ↔ Surjective f :=
  ⟨surjective_of_injective, fun hsurj =>
    HasLeftInverse.injective ⟨surjInv hsurj, leftInverse_of_surjective_of_rightInverse
      (surjective_of_injective (injective_surjInv _))
      (rightInverse_surjInv _)⟩⟩
Equivalence of Injectivity and Surjectivity for Endomorphisms of Finite Types
Informal description
For any function $f \colon \alpha \to \alpha$ on a finite type $\alpha$, the following are equivalent: 1. $f$ is injective, 2. $f$ is surjective.
Finite.injective_iff_surjective_of_equiv theorem
{f : α → β} (e : α ≃ β) : Injective f ↔ Surjective f
Full source 
theorem injective_iff_surjective_of_equiv {f : α → β} (e : α ≃ β) : InjectiveInjective f ↔ Surjective f :=
  have : InjectiveInjective (e.symm ∘ f) ↔ Surjective (e.symm ∘ f) := injective_iff_surjective
  ⟨fun hinj => by
    simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj)),
    fun hsurj => by
    simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))⟩
Equivalence of Injectivity and Surjectivity for Functions Between Equivalent Finite Types
Informal description
Let $\alpha$ and $\beta$ be finite types with a bijection $e : \alpha \simeq \beta$ between them. For any function $f : \alpha \to \beta$, the following are equivalent: 1. $f$ is injective, 2. $f$ is surjective.
Fintype.card_coe theorem
(s : Finset α) [Fintype s] : Fintype.card s = #s
Full source 
@[simp]
theorem Fintype.card_coe (s : Finset α) [Fintype s] : Fintype.card s = #s :=
  @Fintype.card_of_finset' _ _ _ (fun _ => Iff.rfl) (id _)
Cardinality of Finite Subset as Type Equals its Finset Cardinality
Informal description
For any finite subset $s$ of a type $\alpha$, the cardinality of $s$ as a finite type is equal to the cardinality of $s$ as a finite set, i.e., $|s| = \#s$.
Finset.exists_superset_card_eq theorem
[Fintype α] {n : ℕ} {s : Finset α} (hsn : #s ≤ n) (hnα : n ≤ Fintype.card α) : ∃ t, s ⊆ t ∧ #t = n
Full source 
/-- We can inflate a set `s` to any bigger size. -/
lemma Finset.exists_superset_card_eq [Fintype α] {n : ℕ} {s : Finset α} (hsn : #s ≤ n)
    (hnα : n ≤ Fintype.card α) :
    ∃ t, s ⊆ t ∧ #t = n := by simpa using exists_subsuperset_card_eq s.subset_univ hsn hnα
Existence of Superset with Prescribed Cardinality in Finite Types
Informal description
Let $\alpha$ be a finite type, $s$ be a finite subset of $\alpha$, and $n$ be a natural number such that the cardinality of $s$ is at most $n$ and $n$ is at most the cardinality of $\alpha$. Then there exists a finite subset $t$ of $\alpha$ such that $s \subseteq t$ and the cardinality of $t$ is exactly $n$.
Fintype.card_prop theorem
: Fintype.card Prop = 2
Full source 
@[simp]
theorem Fintype.card_prop : Fintype.card Prop = 2 :=
  rfl
Cardinality of Proposition Type is 2
Informal description
The cardinality of the type of propositions `Prop` is equal to 2, i.e., $|\text{Prop}| = 2$.
set_fintype_card_le_univ theorem
[Fintype α] (s : Set α) [Fintype s] : Fintype.card s ≤ Fintype.card α
Full source 
theorem set_fintype_card_le_univ [Fintype α] (s : Set α) [Fintype s] :
    Fintype.card s ≤ Fintype.card α :=
  Fintype.card_le_of_embedding (Function.Embedding.subtype s)
Cardinality Inequality for Subsets of Finite Types
Informal description
For any finite type $\alpha$ and any subset $s \subseteq \alpha$ that is also finite, the cardinality of $s$ is less than or equal to the cardinality of $\alpha$, i.e., $|s| \leq |\alpha|$.
set_fintype_card_eq_univ_iff theorem
[Fintype α] (s : Set α) [Fintype s] : Fintype.card s = Fintype.card α ↔ s = Set.univ
Full source 
theorem set_fintype_card_eq_univ_iff [Fintype α] (s : Set α) [Fintype s] :
    Fintype.cardFintype.card s = Fintype.card α ↔ s = Set.univ := by
  rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]
Subset Equals Universal Set iff Cardinalities Match in Finite Types
Informal description
For a finite type $\alpha$ and a subset $s \subseteq \alpha$ that is also finite, the cardinality of $s$ equals the cardinality of $\alpha$ if and only if $s$ is the universal set of $\alpha$, i.e., $|s| = |\alpha| \leftrightarrow s = \text{univ}$.
Fintype.card_subtype_le theorem
[Fintype α] (p : α → Prop) [Fintype { a // p a }] : Fintype.card { x // p x } ≤ Fintype.card α
Full source 
theorem Fintype.card_subtype_le [Fintype α] (p : α → Prop) [Fintype {a // p a}] :
    Fintype.card { x // p x } ≤ Fintype.card α :=
  Fintype.card_le_of_embedding (Function.Embedding.subtype _)
Cardinality Bound for Subtypes of Finite Types
Informal description
For any finite type $\alpha$ and predicate $p$ on $\alpha$, the cardinality of the subtype $\{x \in \alpha \mid p(x)\}$ is less than or equal to the cardinality of $\alpha$.
Fintype.card_subtype_lt theorem
[Fintype α] {p : α → Prop} [Fintype { a // p a }] {x : α} (hx : ¬p x) : Fintype.card { x // p x } < Fintype.card α
Full source 
lemma Fintype.card_subtype_lt [Fintype α] {p : α → Prop} [Fintype {a // p a}] {x : α} (hx : ¬p x) :
    Fintype.card { x // p x } < Fintype.card α :=
  Fintype.card_lt_of_injective_of_not_mem (b := x) (↑) Subtype.coe_injective <| by
    rwa [Subtype.range_coe_subtype]
Strict Cardinality Inequality for Proper Subtypes of Finite Types
Informal description
Let $\alpha$ be a finite type and $p : \alpha \to \mathrm{Prop}$ a predicate on $\alpha$. If there exists an element $x \in \alpha$ such that $\neg p(x)$, then the cardinality of the subtype $\{x \mid p(x)\}$ is strictly less than the cardinality of $\alpha$, i.e., $|\{x \mid p(x)\}| < |\alpha|$.
Fintype.card_subtype theorem
[Fintype α] (p : α → Prop) [Fintype { a // p a }] [DecidablePred p] : Fintype.card { x // p x } = #{x | p x}
Full source 
theorem Fintype.card_subtype [Fintype α] (p : α → Prop) [Fintype {a // p a}] [DecidablePred p] :
    Fintype.card { x // p x } = #{x | p x} := by
  refine Fintype.card_of_subtype _ ?_
  simp
Cardinality of Subtype Equals Cardinality of Predicate-Satisfying Elements
Informal description
For a finite type $\alpha$ and a decidable predicate $p : \alpha \to \mathrm{Prop}$, the cardinality of the subtype $\{x \mid p(x)\}$ is equal to the number of elements in $\alpha$ that satisfy $p$, i.e., $|\{x \mid p(x)\}| = |\{x \in \alpha \mid p(x)\}|$.
Fintype.card_subtype_compl theorem
[Fintype α] (p : α → Prop) [Fintype { x // p x }] [Fintype { x // ¬p x }] : Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x }
Full source 
@[simp]
theorem Fintype.card_subtype_compl [Fintype α] (p : α → Prop) [Fintype { x // p x }]
    [Fintype { x // ¬p x }] :
    Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x } := by
  classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }{ x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
Cardinality of Complement Subtype: $|\{x \mid \neg p(x)\}| = |\alpha| - |\{x \mid p(x)\}|$
Informal description
For a finite type $\alpha$ and a predicate $p : \alpha \to \mathrm{Prop}$ such that both the subtype $\{x \mid p(x)\}$ and its complement $\{x \mid \neg p(x)\}$ are finite, the cardinality of the complement subtype equals the difference between the cardinality of $\alpha$ and the cardinality of the original subtype, i.e., $$|\{x \mid \neg p(x)\}| = |\alpha| - |\{x \mid p(x)\}|.$$
Fintype.card_subtype_mono theorem
(p q : α → Prop) (h : p ≤ q) [Fintype { x // p x }] [Fintype { x // q x }] : Fintype.card { x // p x } ≤ Fintype.card { x // q x }
Full source 
theorem Fintype.card_subtype_mono (p q : α → Prop) (h : p ≤ q) [Fintype { x // p x }]
    [Fintype { x // q x }] : Fintype.card { x // p x } ≤ Fintype.card { x // q x } :=
  Fintype.card_le_of_embedding (Subtype.impEmbedding _ _ h)
Monotonicity of Subtype Cardinality under Implication of Predicates
Informal description
For any finite type $\alpha$ and predicates $p, q : \alpha \to \mathrm{Prop}$ such that $p(x)$ implies $q(x)$ for all $x \in \alpha$, the cardinality of the subtype $\{x \mid p(x)\}$ is less than or equal to the cardinality of the subtype $\{x \mid q(x)\}$.
Fintype.card_compl_eq_card_compl theorem
[Finite α] (p q : α → Prop) [Fintype { x // p x }] [Fintype { x // ¬p x }] [Fintype { x // q x }] [Fintype { x // ¬q x }] (h : Fintype.card { x // p x } = Fintype.card { x // q x }) : Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x }
Full source 
/-- If two subtypes of a fintype have equal cardinality, so do their complements. -/
theorem Fintype.card_compl_eq_card_compl [Finite α] (p q : α → Prop) [Fintype { x // p x }]
    [Fintype { x // ¬p x }] [Fintype { x // q x }] [Fintype { x // ¬q x }]
    (h : Fintype.card { x // p x } = Fintype.card { x // q x }) :
    Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x } := by
  cases nonempty_fintype α
  simp only [Fintype.card_subtype_compl, h]
Equal Cardinality of Complements for Subtypes with Equal Cardinality
Informal description
Let $\alpha$ be a finite type, and let $p, q : \alpha \to \mathrm{Prop}$ be predicates such that the subtypes $\{x \mid p(x)\}$, $\{x \mid \neg p(x)\}$, $\{x \mid q(x)\}$, and $\{x \mid \neg q(x)\}$ are all finite. If the cardinalities of $\{x \mid p(x)\}$ and $\{x \mid q(x)\}$ are equal, then the cardinalities of their complements $\{x \mid \neg p(x)\}$ and $\{x \mid \neg q(x)\}$ are also equal. In other words, if $|\{x \mid p(x)\}| = |\{x \mid q(x)\}|$, then $|\{x \mid \neg p(x)\}| = |\{x \mid \neg q(x)\}|$.
Fintype.card_quotient_le theorem
[Fintype α] (s : Setoid α) [DecidableRel ((· ≈ ·) : α → α → Prop)] : Fintype.card (Quotient s) ≤ Fintype.card α
Full source 
theorem Fintype.card_quotient_le [Fintype α] (s : Setoid α)
    [DecidableRel ((· ≈ ·) : α → α → Prop)] : Fintype.card (Quotient s) ≤ Fintype.card α :=
  Fintype.card_le_of_surjective _ Quotient.mk'_surjective
Cardinality Inequality for Quotient of Finite Type
Informal description
For any finite type $\alpha$ with a setoid $s$ and a decidable equivalence relation $\approx$ on $\alpha$, the cardinality of the quotient type $\text{Quotient } s$ is less than or equal to the cardinality of $\alpha$.
univ_eq_singleton_of_card_one theorem
{α} [Fintype α] (x : α) (h : Fintype.card α = 1) : (univ : Finset α) = { x }
Full source 
theorem univ_eq_singleton_of_card_one {α} [Fintype α] (x : α) (h : Fintype.card α = 1) :
    (univ : Finset α) = {x} := by
  symm
  apply eq_of_subset_of_card_le (subset_univ {x})
  apply le_of_eq
  simp [h, Finset.card_univ]
Universal Finite Set is Singleton for Cardinality One
Informal description
For a finite type $\alpha$ with cardinality $1$ and an element $x \in \alpha$, the universal finite set $\text{univ}$ of $\alpha$ is equal to the singleton set $\{x\}$.
Finite.wellFounded_of_trans_of_irrefl theorem
(r : α → α → Prop) [IsTrans α r] [IsIrrefl α r] : WellFounded r
Full source 
theorem wellFounded_of_trans_of_irrefl (r : α → α → Prop) [IsTrans α r] [IsIrrefl α r] :
    WellFounded r := by
  classical
  cases nonempty_fintype α
  have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset,
          Finset.subset_iff, mem_filter, true_and, mem_univ, hxy]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  exact Subrelation.wf (this _ _) (measure _).wf
Well-foundedness of Transitive and Irreflexive Relations on Finite Types
Informal description
For any finite type $\alpha$ and any binary relation $r$ on $\alpha$ that is both transitive and irreflexive, the relation $r$ is well-founded. That is, every non-empty subset of $\alpha$ has a minimal element with respect to $r$.
Finite.to_wellFoundedGT instance
[Preorder α] : WellFoundedGT α
Full source 
instance (priority := 100) to_wellFoundedGT [Preorder α] : WellFoundedGT α :=
  ⟨wellFounded_of_trans_of_irrefl _⟩
Well-foundedness of $>$ on finite preorders
Informal description
For any finite type $\alpha$ with a preorder, the strict greater-than relation $>$ is well-founded. That is, every non-empty subset of $\alpha$ has a minimal element with respect to $>$.
Bool.instWellFoundedLT instance
: WellFoundedLT Bool
Full source 
instance Bool.instWellFoundedLT : WellFoundedLT Bool := inferInstance
Well-foundedness of the Boolean Order
Informal description
The boolean type `Bool` with its strict less-than relation $<$ is well-founded.
Bool.instWellFoundedGT instance
: WellFoundedGT Bool
Full source 
instance Bool.instWellFoundedGT : WellFoundedGT Bool := inferInstance
Well-foundedness of $>$ on Booleans
Informal description
The boolean type `Bool` with its strict greater-than relation $>$ is well-founded. That is, every non-empty subset of `Bool` has a minimal element with respect to $>$.
Prop.instWellFoundedLT instance
: WellFoundedLT Prop
Full source 
instance Prop.instWellFoundedLT : WellFoundedLT Prop := inferInstance
Well-foundedness of Strict Implication on Propositions
Informal description
The strict implication order $<$ on propositions is well-founded. That is, every non-empty collection of propositions has a minimal element with respect to the strict implication relation.
Prop.instWellFoundedGT instance
: WellFoundedGT Prop
Full source 
instance Prop.instWellFoundedGT : WellFoundedGT Prop := inferInstance
Well-foundedness of the Implication Order on Propositions
Informal description
The type of propositions `Prop` has a well-founded strict greater-than relation $>$, meaning every non-empty subset of propositions has a minimal element with respect to the implication order.
truncOfCardPos definition
{α} [Fintype α] (h : 0 < Fintype.card α) : Trunc α
Full source 
/-- A `Fintype` with positive cardinality constructively contains an element.
-/
def truncOfCardPos {α} [Fintype α] (h : 0 < Fintype.card α) : Trunc α :=
  letI := Fintype.card_pos_iff.mp h
  truncOfNonemptyFintype α
Truncation of an element in a nonempty finite type
Informal description
Given a finite type $\alpha$ with positive cardinality (i.e., $|\alpha| > 0$), the function constructs a term of type `Trunc α`, representing the truncation of some element in $\alpha$.
Fintype.induction_subsingleton_or_nontrivial theorem
{P : ∀ (α) [Fintype α], Prop} (α : Type*) [Fintype α] (hbase : ∀ (α) [Fintype α] [Subsingleton α], P α) (hstep : ∀ (α) [Fintype α] [Nontrivial α], (∀ (β) [Fintype β], Fintype.card β < Fintype.card α → P β) → P α) : P α
Full source 
/-- A custom induction principle for fintypes. The base case is a subsingleton type,
and the induction step is for non-trivial types, and one can assume the hypothesis for
smaller types (via `Fintype.card`).

The major premise is `Fintype α`, so to use this with the `induction` tactic you have to give a name
to that instance and use that name.
-/
@[elab_as_elim]
theorem Fintype.induction_subsingleton_or_nontrivial {P : ∀ (α) [Fintype α], Prop} (α : Type*)
    [Fintype α] (hbase : ∀ (α) [Fintype α] [Subsingleton α], P α)
    (hstep : ∀ (α) [Fintype α] [Nontrivial α],
      (∀ (β) [Fintype β], Fintype.card β < Fintype.card α → P β) → P α) :
    P α := by
  obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.card α, rfl⟩
  induction' n using Nat.strong_induction_on with n ih generalizing α
  rcases subsingleton_or_nontrivial α with hsing | hnontriv
  · apply hbase
  · apply hstep
    intro β _ hlt
    rw [hn] at hlt
    exact ih (Fintype.card β) hlt _ rfl
Induction Principle for Finite Types via Subsingleton-Nontrivial Dichotomy
Informal description
Let $P$ be a property depending on a finite type $\alpha$. To prove $P(\alpha)$ for all finite types $\alpha$, it suffices to: 1. Prove $P(\alpha)$ for all subsingleton types $\alpha$ (base case), and 2. For any nontrivial finite type $\alpha$, assuming $P(\beta)$ holds for all finite types $\beta$ with $|\beta| < |\alpha|$, prove $P(\alpha)$ (inductive step). Here $|\alpha|$ denotes the cardinality of $\alpha$.
Fintype.card_fin theorem
(n : ℕ) : Fintype.card (Fin n) = n
Full source 
@[simp]
theorem Fintype.card_fin (n : ℕ) : Fintype.card (Fin n) = n :=
  List.length_finRange
Cardinality of Finite Ordinals: $|\mathrm{Fin}(n)| = n$
Informal description
For any natural number $n$, the cardinality of the finite type $\mathrm{Fin}(n)$ is equal to $n$.
Fintype.card_fin_lt_of_le theorem
{m n : ℕ} (h : m ≤ n) : Fintype.card { i : Fin n // i < m } = m
Full source 
theorem Fintype.card_fin_lt_of_le {m n : ℕ} (h : m ≤ n) :
    Fintype.card {i : Fin n // i < m} = m := by
  conv_rhs => rw [← Fintype.card_fin m]
  apply Fintype.card_congr
  exact { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
          invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩
          left_inv := fun i ↦ rfl
          right_inv := fun i ↦ rfl }
Cardinality of Initial Segment of Finite Ordinals: $|\{i \in \mathrm{Fin}(n) \mid i < m\}| = m$ when $m \leq n$
Informal description
For any natural numbers $m$ and $n$ such that $m \leq n$, the cardinality of the subtype $\{i \in \mathrm{Fin}(n) \mid i < m\}$ is equal to $m$.
Finset.card_fin theorem
(n : ℕ) : #(univ : Finset (Fin n)) = n
Full source 
theorem Finset.card_fin (n : ℕ) : #(univ : Finset (Fin n)) = n := by simp
Cardinality of Finite Ordinals: $|\mathrm{Fin}(n)| = n$
Informal description
For any natural number $n$, the cardinality of the universal finite set of $\mathrm{Fin}(n)$ is equal to $n$, i.e., $|\mathrm{Fin}(n)| = n$.
fin_injective theorem
: Function.Injective Fin
Full source 
/-- `Fin` as a map from `ℕ` to `Type` is injective. Note that since this is a statement about
equality of types, using it should be avoided if possible. -/
theorem fin_injective : Function.Injective Fin := fun m n h =>
  (Fintype.card_fin m).symm.trans <| (Fintype.card_congr <| Equiv.cast h).trans (Fintype.card_fin n)
Injectivity of the Finite Ordinal Type Constructor: $\mathrm{Fin}(m) = \mathrm{Fin}(n) \Rightarrow m = n$
Informal description
The function $\mathrm{Fin} : \mathbb{N} \to \mathrm{Type}$ that maps a natural number $n$ to the type $\mathrm{Fin}(n)$ of finite ordinals less than $n$ is injective. That is, for any natural numbers $m$ and $n$, if $\mathrm{Fin}(m) = \mathrm{Fin}(n)$, then $m = n$.
Fin.val_eq_val_of_heq theorem
{k l : ℕ} {i : Fin k} {j : Fin l} (h : HEq i j) : (i : ℕ) = (j : ℕ)
Full source 
theorem Fin.val_eq_val_of_heq {k l : ℕ} {i : Fin k} {j : Fin l} (h : HEq i j) :
    (i : ℕ) = (j : ℕ) :=
  (Fin.heq_ext_iff (fin_injective (type_eq_of_heq h))).1 h
Natural Number Values Agree Under Heterogeneous Equality in Finite Types
Informal description
For any natural numbers $k$ and $l$, and any elements $i \in \mathrm{Fin}(k)$ and $j \in \mathrm{Fin}(l)$, if $i$ and $j$ are heterogeneously equal (denoted as $i \approx j$), then their underlying natural number values are equal, i.e., $(i : \mathbb{N}) = (j : \mathbb{N})$.
Fin.cast_eq_cast' theorem
{n m : ℕ} (h : Fin n = Fin m) : _root_.cast h = Fin.cast (fin_injective h)
Full source 
/-- A reversed version of `Fin.cast_eq_cast` that is easier to rewrite with. -/
theorem Fin.cast_eq_cast' {n m : ℕ} (h : Fin n = Fin m) :
    _root_.cast h = Fin.cast (fin_injective h) := by
  cases fin_injective h
  rfl
Equality of Cast Functions for Finite Ordinals: $\mathrm{cast} = \mathrm{Fin.cast}$ under $\mathrm{Fin}(n) = \mathrm{Fin}(m)$
Informal description
For any natural numbers $n$ and $m$, if the finite ordinal types $\mathrm{Fin}(n)$ and $\mathrm{Fin}(m)$ are equal (i.e., $\mathrm{Fin}(n) = \mathrm{Fin}(m)$), then the canonical cast function `_root_.cast h` is equal to the finite ordinal cast function `Fin.cast` applied to the proof that $n = m$ obtained from the injectivity of $\mathrm{Fin}$.
card_finset_fin_le theorem
{n : ℕ} (s : Finset (Fin n)) : #s ≤ n
Full source 
theorem card_finset_fin_le {n : ℕ} (s : Finset (Fin n)) : #s ≤ n := by
  simpa only [Fintype.card_fin] using s.card_le_univ
Cardinality Bound for Subsets of Finite Ordinals: $|s| \leq n$
Informal description
For any natural number $n$ and any finite subset $s$ of the finite ordinal type $\mathrm{Fin}(n)$, the cardinality of $s$ is less than or equal to $n$, i.e., $|s| \leq n$.