LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Data.Fintype.Card

`Fintype.card_eq_zero` theorem Fintype.card_eq_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : IsEmpty α], Fintype.card α = 0 The theorem `Fintype.card_eq_zero` states that for any finite type `α`, given that `α` is empty (i.e., there are no instances of `α`), then the cardinality of `α` (the number of elements in `α`) is `0`. This theorem is essentially saying that the size of an empty finite set is `0`. More concisely: The theorem asserts that the cardinality of a finite empty type is equal to zero.
`Fintype.card_le_one_iff` theorem Fintype.card_le_one_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α ≤ 1 ↔ ∀ (a b : α), a = b := by sorry The theorem `Fintype.card_le_one_iff` states that for any type `α` that is a finite type (fintype), the cardinality of `α`, i.e., the number of elements in `α`, is less than or equal to one if and only if all elements `a` and `b` in `α` are equal. In other words, a finite type has at most one distinct element if and only if any two elements in the type are the same. More concisely: A finite type `α` has at most one element if and only if all its elements are equal. (Equivalently, the cardinality of a finite type `α` is less than or equal to one if and only if `α` is a singleton.)
`Fintype.card_pos` theorem Fintype.card_pos : ∀ {α : Type u_1} [inst : Fintype α] [h : Nonempty α], 0 < Fintype.card α The theorem `Fintype.card_pos` states that for any type `α` which has a finite number of elements (i.e., is a `fintype`), if `α` is nonempty, then the cardinality of `α` (the number of elements in `α`, denoted as `Fintype.card α`) is strictly greater than zero. In other words, if a type has a finite number of elements and is not empty, then it must have at least one element. More concisely: If `α` is a nonempty finite type, then `Fintype.card α` is strictly positive.
`Function.Surjective.bijective_of_finite` theorem Function.Surjective.bijective_of_finite : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Surjective f → Function.Bijective f This theorem, referred to as an alias of the forward direction of `Finite.surjective_iff_bijective`, states that for any type `α` that is finite, a function `f` mapping from `α` to itself is bijective if it is surjective. That is, if `f` is a function such that every element of `α` can be mapped to by `f` (surjectivity), then `f` is also a function where each element of `α` is mapped to a unique element and each element is the image of a unique element (bijectivity). More concisely: If `α` is finite, then a function `f: α → α` is bijective if and only if it is surjective.
`Fintype.finite` theorem Fintype.finite : ∀ {α : Type u_4}, Fintype α → Finite α This theorem states that for any given type `α`, if `α` is a finite type (`Fintype α`), then `α` is also considered as a finite set (`Finite α`). This directly correlates the `Fintype` and `Finite` classes in Lean, asserting that if a type is finite, it also forms a finite set. More concisely: If `α` is a finite type, then `α` is a finite set (`Fintype α → Finite α`).
`Infinite.of_surjective` theorem Infinite.of_surjective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Infinite β] (f : α → β), Function.Surjective f → Infinite α The theorem `Infinite.of_surjective` states that for any two types `α` and `β`, if `β` is infinite and there exists a function `f` from `α` to `β` that is surjective (meaning that for every element `b` in `β`, there exists an element `a` in `α` such that `f(a) = b`), then `α` is also infinite. In other words, if we can map every element of an infinite type `β` to elements of another type `α` in a way that every element of `β` is the image of at least one element of `α`, then `α` must be infinite as well. More concisely: If `β` is an infinite type and there exists a surjective function `f` from `α` to `β`, then `α` is infinite.
`Finite.of_surjective` theorem Finite.of_surjective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Finite α] (f : α → β), Function.Surjective f → Finite β The theorem `Finite.of_surjective` states that for all types `α` and `β`, if `α` is finite and there exists a surjective function `f` from `α` to `β`, then `β` is also finite. In other words, if every element in `β` can be mapped from some element in `α` (which is a finite set), then `β` must also be a finite set. This theorem is a formal statement of the intuitive idea that the image of a finite set under a surjective function is also finite. More concisely: If `α` is a finite type and there exists a surjective function from `α` to `β`, then `β` is finite.
`Infinite.of_not_fintype` theorem Infinite.of_not_fintype : ∀ {α : Type u_1}, (Fintype α → False) → Infinite α This theorem states that for any type `α`, if the type `α` is not finite (meaning that it cannot be represented by a `Fintype` structure), then `α` is infinite. This is a fundamental result in set theory which essentially says that a type is infinite if and only if it is not finite. In mathematical notation, this could be written as: for every type `α`, if `α` is not a finite type, then `α` is an infinite type. More concisely: If a type `α` is not finite (has no `Fintype` structure), then `α` is infinite.
`Finite.injective_iff_bijective` theorem Finite.injective_iff_bijective : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Injective f ↔ Function.Bijective f The theorem `Finite.injective_iff_bijective` states that for any type `α`, given it is finite (as indicated by `Finite α`), for any function `f` from `α` to `α`, the function `f` is injective (meaning that if `f x = f y`, then `x = y`) if and only if `f` is bijective (meaning that `f` is both injective and surjective, where surjective means that for every element in the codomain there exists an element in the domain that is mapped to it). This theorem essentially says that in the realm of finite sets, injectivity of a function is equivalent to its bijectivity. More concisely: A function from a finite type to itself is injective if and only if it is bijective.
`Finset.card_eq_iff_eq_univ` theorem Finset.card_eq_iff_eq_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card = Fintype.card α ↔ s = Finset.univ The theorem `Finset.card_eq_iff_eq_univ` states that for any given type `α` with a finite number of elements (or `Fintype α`), and for any finite set `s` of type `α` (or `Finset α`), the cardinality of `s` (number of elements in `s`) is equal to the total number of elements of type `α` if and only if `s` is the universal finite set of type `α`. In other words, a finite set `s` contains all possible elements of its type `α` if and only if the number of elements in `s` equals the total count of elements of `α`. More concisely: For any finite type `α` and finite set `s` of type `Finset α`, the cardinalities of `s` and `α` are equal if and only if `s` is the universal set of type `α`.
`Fintype.card_ulift` theorem Fintype.card_ulift : ∀ (α : Type u_4) [inst : Fintype α], Fintype.card (ULift.{u_5, u_4} α) = Fintype.card α The theorem `Fintype.card_ulift` states that for any type `α` that is a finite set (or `Fintype`), the cardinality (or the number of elements) of the type `ULift.{u_5, u_4} α` is equal to the cardinality of the type `α`. Here, `ULift.{u_5, u_4} α` represents a type that is equivalent to `α` but lives in a different universe of types. Hence, this theorem highlights that lifting a type to a different universe does not change its cardinality. More concisely: The cardinality of a finite type `α` is equal to the cardinality of `ULift.{u_5, u_4} α`.
`Finite.exists_infinite_fiber` theorem Finite.exists_infinite_fiber : ∀ {α : Type u_1} {β : Type u_2} [inst : Infinite α] [inst : Finite β] (f : α → β), ∃ y, Infinite ↑(f ⁻¹' {y}) := by sorry The theorem `Finite.exists_infinite_fiber` states the strong pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. It says that if there is a function `f` that maps elements from an infinite type `α` to a finite type `β`, then there exists an element `y` in `β` such that the preimage of `y` under `f` (the set of all elements in `α` that `f` maps to `y`) is infinite. In other words, if there are infinitely many items (the 'pigeons') and they are distributed into a finite number of categories (the 'pigeonholes'), then at least one category must contain infinitely many items. More concisely: If `f` is a function from an infinite type `α` to a finite type `β`, then there exists `y` in `β` such that the fibre `f^{-1}(y)` is infinite.
`Function.Injective.surjective_of_fintype` theorem Function.Injective.surjective_of_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] {f : α → β}, α ≃ β → Function.Injective f → Function.Surjective f The theorem `Function.Injective.surjective_of_fintype` states that for any function `f` from type `α` to `β`, where `α` has a finite number of elements and `α` is equivalent to `β`, if `f` is injective (i.e., each input to `f` produces a distinct output), then `f` is also surjective (i.e., every element of `β` is the output of `f` for some input in `α`). In other words, for finite and equivalent types, an injective function from `α` to `β` is guaranteed to be surjective. More concisely: For any finite and equivalent types `α` and `β`, an injective function `f` from `α` to `β` is surjective.
`Fintype.card_ne_zero` theorem Fintype.card_ne_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α], Fintype.card α ≠ 0 The theorem `Fintype.card_ne_zero` states that for any type `α` that is a finite type (i.e., has a finite number of elements) and is nonempty (i.e., contains at least one element), the cardinality of `α` (the number of elements in `α`) is not equal to zero. This theorem is intuitively clear, as a set that contains at least one element cannot have zero elements, and serves as a formal encoding of this fact in Lean 4. More concisely: If `α` is a finite, nonempty type, then the cardinality of `α` is different from zero.
`Finite.of_injective` theorem Finite.of_injective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Finite β] (f : α → β), Function.Injective f → Finite α The theorem `Finite.of_injective` states that for any types `α` and `β`, if `β` is finite and there exists an injective function `f` from `α` to `β`, then `α` is also finite. In other words, if we have a function `f` such that for all elements `x` and `y` in `α`, if `f(x) = f(y)`, then `x = y`, and if the codomain `β` of this function is finite, then the domain `α` is also finite. This theorem connects the concept of injective functions with the finiteness property of sets in the context of mathematical logic and type theory. More concisely: If `β` is a finite type and there exists an injective function from `α` to `β`, then `α` is also finite.
`Infinite.of_injective` theorem Infinite.of_injective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Infinite β] (f : β → α), Function.Injective f → Infinite α The theorem `Infinite.of_injective` states that for any two types `α` and `β`, if `β` is infinite and there exists an injective function `f` from `β` to `α`, then `α` is also infinite. In other words, if we can map every element of `β` to a unique element of `α` (which is what it means for `f` to be injective) and `β` has infinitely many elements, then `α` must also have infinitely many elements. More concisely: If `β` is an infinite type and there exists an injective function from `β` to `α`, then `α` is infinite.
`Fintype.card_eq_one_iff` theorem Fintype.card_eq_one_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α = 1 ↔ ∃ x, ∀ (y : α), y = x := by sorry The theorem `Fintype.card_eq_one_iff` states that for every type `α` which is a finite type, the cardinality (number of elements) of `α` is equal to one if and only if there exists an element `x` in `α` such that every element `y` in `α` is equal to `x`. In other words, a finite type has exactly one element if and only if all elements in that type are the same. More concisely: A finite type `α` has exactly one element if and only if all elements in `α` are equal.
`Fintype.card_ofFinset` theorem Fintype.card_ofFinset : ∀ {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p), Fintype.card ↑p = s.card This theorem, `Fintype.card_ofFinset`, states that for any type `α`, any set `p` of type `α`, and any finite set `s` of type `α`, if each element `x` of type `α` belongs to `s` if and only if it belongs to `p`, then the cardinality (or the number of elements) of the type `p`, when `p` is considered as a `Fintype`, is equal to the cardinality of the finite set `s`. In other words, both `p` and `s` have the same number of elements under the condition that their membership relation is equivalent. More concisely: If `p` is a finite subset of type `α` such that `x ∈ p` if and only if `x ∈ s`, then `#p = #s`, where `#` denotes the cardinality.
`Finite.wellFounded_of_trans_of_irrefl` theorem Finite.wellFounded_of_trans_of_irrefl : ∀ {α : Type u_1} [inst : Finite α] (r : α → α → Prop) [inst : IsTrans α r] [inst : IsIrrefl α r], WellFounded r This theorem states that for any type `α` which is finite, and any binary relation `r` on `α`, if `r` is transitive and irreflexive, then `r` is well-founded. In mathematical terms, if we have a finite set and a relation on this set that is both transitive (i.e., if `a r b` and `b r c` then `a r c`) and irreflexive (i.e., `a r a` is always false), then we can say this relation is well-founded, meaning there are no infinite descending chains, which can be symbolized as: there does not exist a sequence `(a_i)` such that `a_{i+1} r a_i` for every `i`. More concisely: If `α` is a finite type and `r` is a transitive and irreflexive relation on `α`, then `r` is well-founded, i.e., there is no infinite descending chain `a_i r a_{i+1}` for any sequence `(a_i)` in `α`.
`Fintype.card_eq` theorem Fintype.card_eq : ∀ {α : Type u_4} {β : Type u_5} [_F : Fintype α] [_G : Fintype β], Fintype.card α = Fintype.card β ↔ Nonempty (α ≃ β) The theorem `Fintype.card_eq` states that for any two types `α` and `β`, assuming both are finite (`Fintype α` and `Fintype β` respectively), the cardinality of `α` (number of elements in `α`) is equal to the cardinality of `β` if and only if there exists a bijection between `α` and `β` (represented as `α ≃ β` in Lean). In other words, two finite types have the same number of elements if and only if there's a one-to-one correspondence between their elements. More concisely: For finite types `α` and `β`, their cardinalities are equal if and only if there exists a bijection between them.
`List.exists_pw_disjoint_with_card` theorem List.exists_pw_disjoint_with_card : ∀ {α : Type u_4} [inst : Fintype α] {c : List ℕ}, c.sum ≤ Fintype.card α → ∃ o, List.map List.length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ List.Pairwise List.Disjoint o The theorem `List.exists_pw_disjoint_with_card` states that for any list of natural numbers `c`, whose sum is less than or equal to the cardinality of a finite type `α`, there exists another list `o`, composed of lists of elements of type `α`. Each list in `o` has a unique set of elements (no duplicates) and their respective lengths match the elements in the original list `c`. Moreover, all lists in `o` are pairwise disjoint, meaning that there are no common elements between any two lists in `o`. More concisely: Given a list `c` of natural numbers with sum less than or equal to the cardinality of a finite type `α`, there exists a list `o` of pairwise disjoint, non-empty lists of elements from `α`, such that the length of each list in `o` equals the corresponding element in `c`.
`Finset.eq_univ_of_card` theorem Finset.eq_univ_of_card : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card = Fintype.card α → s = Finset.univ This theorem states that for any finite type `α` and any finite set `s` of type `α`, if the cardinality (or the number of elements) of `s` is equal to the cardinality of `α`, then `s` must be the universal set of `α`. In other words, if a set contains as many elements as the entire finite type it is drawn from, it must contain all elements of that type. More concisely: If a finite set has the same cardinality as a finite type, then the set is the type's universe.
`Fintype.card_le_of_surjective` theorem Fintype.card_le_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Function.Surjective f → Fintype.card β ≤ Fintype.card α The theorem `Fintype.card_le_of_surjective` states that for any two types `α` and `β`, both of which have a fintype instance, if there exists a surjective function `f` from `α` to `β`, then the cardinality (number of elements) in `β` is less than or equal to the cardinality of `α`. In other words, if every element of `β` can be mapped from some element in `α` using function `f`, then `β` cannot have more elements than `α`. More concisely: If `α` and `β` are finite types with a surjective function `f` from `α` to `β`, then the cardinality of `β` is less than or equal to the cardinality of `α`.
`Fintype.subtype_card` theorem Fintype.subtype_card : ∀ {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x), Fintype.card { x // p x } = s.card The theorem `Fintype.subtype_card` states that for any type `α` and any property `p` of elements of that type, if there is a `Finset` `s` of elements of `α` such that an element `x` of `α` is in `s` if and only if `x` satisfies `p`, then the cardinality of the subtype of `α` consisting of elements that satisfy `p` is equal to the cardinality of `s`. In other words, the number of elements in the subtype is the same as the number of elements in the finset. More concisely: If `α` is a type and `s : Finset α` is such that the subtype of `α` consisting of elements satisfying a property `p` is equal to the elements of `s`, then the cardinality of this subtype is equal to the cardinality of `s`.
`Fintype.card_congr'` theorem Fintype.card_congr' : ∀ {α β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β], α = β → Fintype.card α = Fintype.card β The theorem `Fintype.card_congr'` states that for any two types `α` and `β` that are both finite types (`Fintype`), if `α` is equal to `β`, then the cardinality (number of elements) of `α` is equal to the cardinality of `β`. In mathematical terms, it ensures the equality of the sizes of two sets if the two sets are the same. More concisely: If `α` and `β` are finite types (sets) in Lean, then `card α = card β` if and only if `α = β`.
`Function.Embedding.isEmpty_of_card_lt` theorem Function.Embedding.isEmpty_of_card_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β], Fintype.card β < Fintype.card α → IsEmpty (α ↪ β) This theorem states that, for any two finite types `α` and `β`, if the cardinality (or the number of elements) of `β` is less than the cardinality of `α`, then there are no functions that can embed `α` into `β`. This is a formulation of the pigeonhole principle, which roughly states that if there are more pigeons than pigeonholes, then there must be at least one pigeonhole with more than one pigeon. In this case, the elements of `α` represent pigeons and the elements of `β` represent pigeonholes. Note that this theorem cannot be an instance as it requires the proof of `Fintype.card β < Fintype.card α`. More concisely: For any finite types `α` and `β`, if the cardinality of `β` is less than that of `α`, then there is no injective function from `α` to `β`.
`Mathlib.Data.Fintype.Card._auxLemma.12` theorem Mathlib.Data.Fintype.Card._auxLemma.12 : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Injective f = Function.Surjective f This theorem states that for any type `α` that is finite (represented by the `Finite α` attribute), for any function `f` from `α` to `α`, the function `f` being injective is equivalent to the function `f` being surjective. Here, a function `f` is called injective if whenever `f(x)` equals `f(y)`, it must be the case that `x` equals `y`. On the other hand, the function `f` is called surjective if for every element `b` in `α`, there exists an element `a` in `α` such that `f(a)` equals `b`. More concisely: For any finite type `α` and function `f` from `α` to `α`, `f` is injective if and only if it is surjective.
`Fintype.card_subtype_le` theorem Fintype.card_subtype_le : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p], Fintype.card { x // p x } ≤ Fintype.card α The theorem `Fintype.card_subtype_le` states that, for any type `α` that is a `Fintype` (i.e., a finite type) and any predicate `p` on `α` that is decidable (i.e., for each element of `α`, it's known whether it satisfies `p` or not), the number of elements in the subtype of `α` for which `p` holds (denoted by `{ x // p x }` in Lean 4) is less than or equal to the total number of elements in `α`. In other words, the size of any subtype determined by a specific property is always less than or equal to the size of the original type. More concisely: For any finite type `α` and decidable predicate `p` on `α`, the number of elements in the subtype `{ x // p x }` is less than or equal to the cardinality of `α`.
`Fintype.card_ofSubsingleton` theorem Fintype.card_ofSubsingleton : ∀ {α : Type u_1} (a : α) [inst : Subsingleton α], Fintype.card α = 1 This theorem, `Fintype.card_ofSubsingleton`, states that for any type `α` and an element `a` of that type, if `α` is a subsingleton (i.e., it has at most one distinct element), then the cardinality of `α` is 1. In other words, the number of elements in a subsingleton type is always 1. Note that this theorem is particular to `Fintype.ofSubsingleton`, and for arbitrary `Fintype` instances, one should use `Fintype.card_le_one_iff_subsingleton` or `Fintype.card_unique` instead. More concisely: If `α` is a subsingleton type, then the cardinality of `α` is 1.
`Mathlib.Data.Fintype.Card._auxLemma.1` theorem Mathlib.Data.Fintype.Card._auxLemma.1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α], (Fintype.card α = 0) = False This theorem states that for any type `α` which is a finite type (denoted by `Fintype α`) and non-empty (denoted by `Nonempty α`), the cardinality of `α` (the number of elements in `α`) cannot be zero. In other words, it's impossible for a non-empty finite type to have zero elements. More concisely: A non-empty finite type has a positive number of elements.
`Infinite.exists_subset_card_eq` theorem Infinite.exists_subset_card_eq : ∀ (α : Type u_4) [inst : Infinite α] (n : ℕ), ∃ s, s.card = n This theorem, `Infinite.exists_subset_card_eq`, asserts that for any infinite type `α` and any natural number `n`, there exists a finite set `s` of type `α` such that the cardinality of `s` equals `n`. In other words, it is always possible to find a finite subset of an infinite set that has exactly `n` elements. The theorem refers to `Infinite.exists_superset_card_eq` for a similar assertion that instead provides a superset of a given set with a fixed cardinality. More concisely: For any infinite type `α` and natural number `n`, there exists a finite subset of `α` with cardinality equal to `n`.
`Function.Surjective.injective_of_fintype` theorem Function.Surjective.injective_of_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] {f : α → β}, α ≃ β → Function.Surjective f → Function.Injective f The theorem `Function.Surjective.injective_of_fintype` states that for all types `α` and `β`, if `α` is a finite type and there exists a function `f` from `α` to `β` and an equivalence between `α` and `β`, then if `f` is surjective (meaning for every `b` in `β`, there exists an `a` in `α` such that `f(a) = b`), `f` is also injective (meaning that if `f(x) = f(y)`, then `x = y`). In other words, in this specific case, surjectivity of a function implies its injectivity. More concisely: If `α` is a finite type and `f: α → β` is a surjective function with an equivalence between `α` and `β`, then `f` is injective.
`Finset.card_fin` theorem Finset.card_fin : ∀ (n : ℕ), Finset.univ.card = n This theorem states that for any natural number `n`, the cardinality (or size) of the universal finite set (`Finset.univ`) is equal to `n`. Here, `Finset.univ` is a set that consists of all elements of a given type `α`, under the assumption that `α` is a finite type (`Fintype α`). Essentially, this theorem is stating that the number of elements in this universal finite set is `n`, for any `n` in the natural numbers. More concisely: For any finite type `α`, the cardinality of `Finset.univ` (the universal finite set of `α`) equals the natural number representing its size.
`Fintype.card_fin` theorem Fintype.card_fin : ∀ (n : ℕ), Fintype.card (Fin n) = n The theorem `Fintype.card_fin` states that for any natural number `n`, the cardinality (or number of elements) of the finite type `Fin n` is exactly `n`. Here, `Fin n` represents a type with `n` elements indexed by natural numbers from `0` to `n-1`. Essentially, this theorem establishes that the cardinality function correctly computes the number of elements in a finite type. More concisely: The theorem `Fintype.card_fin` asserts that the cardinality of the finite type `Fin n` equals `n`.
`Fintype.card_of_finset'` theorem Fintype.card_of_finset' : ∀ {α : Type u_1} {p : Set α} (s : Finset α), (∀ (x : α), x ∈ s ↔ x ∈ p) → ∀ [inst : Fintype ↑p], Fintype.card ↑p = s.card The theorem `Fintype.card_of_finset'` in Lean 4 expresses a property of finite sets (fintypes) and their cardinalities. Specifically, it states that for any given type `α`, a predicate `p` defining a set of elements of type `α`, and a finite set `s` of elements of type `α`, if every element `x` of type `α` satisfies the condition that `x` is in `s` if and only if `x` is in `p` (i.e., `s` and `p` define the same set), then, assuming the set defined by `p` is a fintype (i.e., a finite set), the cardinality of the set defined by `p` (denoted `Fintype.card ↑p`) is equal to the cardinality of `s` (denoted `s.card`). More concisely: If `p` is a proposition defining a finite set and is equivalent to the membership in a finite set `s`, then the cardinalities of `s` and `{x : α \| p x}` are equal.
`Fintype.card_le_of_injective` theorem Fintype.card_le_of_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Function.Injective f → Fintype.card α ≤ Fintype.card β The theorem `Fintype.card_le_of_injective` states that for any two types `α` and `β`, both of which have a finite number of elements (i.e., they are `Fintype`s), if we have a function `f` from `α` to `β` that is injective (meaning no two different elements in `α` map to the same element in `β`), then the number of elements in `α` (denoted by `Fintype.card α`) is less than or equal to the number of elements in `β` (denoted by `Fintype.card β`). This aligns with the intuitive idea that an injective function cannot map more unique inputs to unique outputs than there are outputs available. More concisely: If `α` and `β` are finite types and `f: α → β` is an injective function, then `Fintype.card α ≤ Fintype.card β`.
`Fintype.card_le_one_iff_subsingleton` theorem Fintype.card_le_one_iff_subsingleton : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α ≤ 1 ↔ Subsingleton α The theorem `Fintype.card_le_one_iff_subsingleton` states that for any type `α` which is a `Fintype` (i.e., a finite type), the cardinality of `α` (i.e., the number of elements in `α`) is less than or equal to one if and only if `α` is a `Subsingleton`. In the language of set theory, a type is a `Subsingleton` if it has at most one element. By this theorem, we see the direct correlation between a type's cardinality and whether or not it is a `Subsingleton` in Lean 4. The "if and only if" indicates a bi-directional implication: not only does having at most one element imply that a type is a `Subsingleton`, but also being a `Subsingleton` implies that a type has at most one element. More concisely: For a type `α` in Lean 4, `α` is a `Fintype` with cardinality less than or equal to one if and only if `α` is a `Subsingleton`.
`Function.Injective.bijective_of_finite` theorem Function.Injective.bijective_of_finite : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Injective f → Function.Bijective f The theorem `Function.Injective.bijective_of_finite` states that for any type `α`, given it is finite (indicated by `[inst : Finite α]`) and a function `f` exists from `α` to `α`, if the function `f` is injective (meaning for every pair of input values in the domain `α`, the corresponding output values in the codomain `α` are identical if and only if the input values are identical), then the function `f` is also bijective. A bijective function is both injective and surjective, meaning that every element of the domain maps to a unique element of the codomain, and every element of the codomain is mapped to by an element of the domain. More concisely: If `α` is finite and `f : α → α` is an injective function, then `f` is bijective.
`Fintype.card_unit` theorem Fintype.card_unit : Fintype.card Unit = 1 The theorem `Fintype.card_unit` states that the cardinality (or the number of elements) of the `Unit` type is 1. Here, `Fintype.card Unit` refers to the size of the `Unit` type, which is a finite type (`Fintype`). The `Unit` type is a type with exactly one value in Lean 4, similar to the `void` type in some other programming languages. Therefore, this theorem is essentially saying that there is exactly one value in the `Unit` type. More concisely: The theorem `Fintype.card_unit` asserts that the cardinality of the Unit type in Lean 4 is equal to 1.
`Fintype.card_lt_of_injective_of_not_mem` theorem Fintype.card_lt_of_injective_of_not_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Function.Injective f → ∀ {b : β}, b ∉ Set.range f → Fintype.card α < Fintype.card β The theorem `Fintype.card_lt_of_injective_of_not_mem` states that for any two finite types `α` and `β` and a function `f` from `α` to `β`, if `f` is injective (meaning that equal outputs imply equal inputs) and there exists an element `b` in `β` that is not in the range of `f` (meaning that `b` is not the image of any element of `α` under `f`), then the cardinality (or size) of `α` is strictly less than the cardinality of `β`. In essence, this theorem is stating a property about the sizes of sets under certain conditions related to injective functions. More concisely: If `f` is an injective function from the finite type `α` to the finite type `β` with `β` containing an element not in the image of `f`, then `#α < #β`.
`Finset.card_univ` theorem Finset.card_univ : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ.card = Fintype.card α The theorem `Finset.card_univ` states that for any type `α` that is finite (i.e., it has a `Fintype α` instance), the cardinality (i.e., the number of elements) of the universal finite set `Finset.univ` of this type is equal to the cardinality of the type `α` itself. In other words, the total number of elements in the universal finite set of a certain type is equal to the total number of elements of that type. More concisely: For any finite type `α`, the cardinality of `Finset.univ (Fintype.of_size (card α))` equals the cardinality of `α`.
`Fintype.ofEquiv_card` theorem Fintype.ofEquiv_card : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α ≃ β), Fintype.card β = Fintype.card α The theorem `Fintype.ofEquiv_card` states that for any two finite types `α` and `β`, if there exists a bijective function (also known as an equivalence) `f` from `α` to `β`, then the cardinality (number of elements) of `α` is identical to the cardinality of `β`. This is a fundamental property in set theory and combinatorics, often referred to as cardinality preserving under bijections. More concisely: If `α` and `β` are finite types with a bijective function `f` between them, then `α` and `β` have the same cardinality.
`Set.toFinset_card` theorem Set.toFinset_card : ∀ {α : Type u_4} (s : Set α) [inst : Fintype ↑s], s.toFinset.card = Fintype.card ↑s := by sorry The theorem `Set.toFinset_card` states that for any type `α` and any set `s` of that type, given a `Fintype` instance for the set `s`, the cardinality of the finite set corresponding to `s` (obtained using `Set.toFinset`) is equal to the cardinality of the `Fintype` instance of `s`. In other words, converting a finite set to a finite type and calculating the number of elements will yield the same result as directly calculating the number of elements in the original finite set. More concisely: For any finite type `α` and finite set `s` of type `α`, the cardinality of `Set.toFinset s` equals the cardinality of the `Fintype` instance of `s`.
`Fintype.card_congr` theorem Fintype.card_congr : ∀ {α : Type u_4} {β : Type u_5} [inst : Fintype α] [inst_1 : Fintype β], α ≃ β → Fintype.card α = Fintype.card β The theorem `Fintype.card_congr` asserts that for any two types `α` and `β`, if they are both finite (`Fintype`) and there exists a bijective mapping (an equivalence, represented as `α ≃ β`) between them, then they have the same number of elements. In other words, the cardinality (`Fintype.card`) of `α` equals the cardinality of `β`. More concisely: If two types `α` and `β` are finite and there exists a bijective mapping between them, then they have the same number of elements.
`Finite.injective_iff_surjective` theorem Finite.injective_iff_surjective : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Injective f ↔ Function.Surjective f The theorem `Finite.injective_iff_surjective` states that for any type `α` that is Finite, and any function `f` from `α` to `α`, the function `f` is injective if and only if it is surjective. In mathematical terms, given a set `α` that is finite and a function `f : α → α`, the function `f` is said to be injective (meaning if `f(x) = f(y)`, then `x = y`) if and only if it is surjective (meaning for every element `b` in `α`, there exists an element `a` in `α` such that `f(a) = b`). More concisely: A function from a finite type to itself is injective if and only if it is surjective.
`Fintype.card_unique` theorem Fintype.card_unique : ∀ {α : Type u_1} [inst : Unique α] [h : Fintype α], Fintype.card α = 1 The theorem `Fintype.card_unique` states that for any type `α` which is both unique and a finite type (i.e., it has a finite number of elements), the cardinality of `α` (denoted by `Fintype.card α`) is equal to 1. In other words, any type that is unique and finite has exactly one element. More concisely: For any unique and finite type `α`, its cardinality equals 1, i.e., `Fintype.card α = 1`.
`Fintype.card_of_subtype` theorem Fintype.card_of_subtype : ∀ {α : Type u_1} {p : α → Prop} (s : Finset α), (∀ (x : α), x ∈ s ↔ p x) → ∀ [inst : Fintype { x // p x }], Fintype.card { x // p x } = s.card The theorem `Fintype.card_of_subtype` states that for any type `α` and any property `p` of `α`, given a finite set `s` of elements of `α`, if for every element `x` of `α`, `x` is in `s` if and only if `x` satisfies `p`, then, provided `{ x // p x }` is a finite type, the cardinality of `{ x // p x }` (i.e. the number of elements that satisfy `p`) is equal to the cardinality of the set `s`. In other words, this theorem relates the size of a subset defined by a property to the size of a finite set satisfying the same property. More concisely: If `s` is a finite set of elements in type `α` such that `x ∈ s` if and only if `p(x)` holds, then the number of elements in `{x : α \| p(x)}` equals the cardinality of `s`.
`Infinite.exists_not_mem_finset` theorem Infinite.exists_not_mem_finset : ∀ {α : Type u_1} [inst : Infinite α] (s : Finset α), ∃ x, x ∉ s This theorem states that for any type `α` that is infinite, for any finite set `s` of type `α`, there exists an element `x` of type `α` that is not in `s`. In other words, if you have an infinite set of elements, you can always find an element that is not in any given finite subset of that set. More concisely: For any infinite type `α`, there exists an element `x` in `α` not contained in any finite subset.
`card_finset_fin_le` theorem card_finset_fin_le : ∀ {n : ℕ} (s : Finset (Fin n)), s.card ≤ n This theorem states that for any natural number `n` and any finite set `s` of elements from the set of natural numbers less than `n` (`Fin n`), the cardinality or size of `s` (i.e., the number of elements in `s`) is always less than or equal to `n`. In terms of mathematical notation, for all natural numbers `n` and all finite sets `s` in `Fin n`, \|s\| ≤ n. More concisely: For all natural numbers `n` and finite sets `s` in `Fin n`, the cardinality of `s` is less than or equal to `n`. In mathematical notation, \|s\| ≤ n.
`Fintype.card_subtype_compl` theorem Fintype.card_subtype_compl : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : Fintype { x // p x }] [inst_2 : Fintype { x // ¬p x }], Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x } The theorem `Fintype.card_subtype_compl` states that for all types `α` that have finite number of elements (i.e., are 'fintypes'), and for any property `p` that elements of `α` might or might not satisfy, the number of elements in `α` that do not satisfy `p` (`Fintype.card { x // ¬p x }`) is equal to the total number of elements in `α` (`Fintype.card α`) minus the number of elements in `α` that do satisfy `p` (`Fintype.card { x // p x }`). In other words, it is a formal statement of the principle that the size of the complement of a subset of a finite set is the total size of the set minus the size of the subset. More concisely: For a fintype `α` and property `p` on `α`, the number of elements not satisfying `p` equals the total number of elements minus the number of elements satisfying `p`. In other words, `Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x }`.
`Fin.cast_eq_cast'` theorem Fin.cast_eq_cast' : ∀ {n m : ℕ} (h : Fin n = Fin m), cast h = Fin.cast ⋯ The theorem `Fin.cast_eq_cast'` states that for any two natural numbers `n` and `m`, if we have an equality between `Fin n` and `Fin m`, then the function `cast` applied to this equality (`h`) is the same as `Fin.cast` applied to some suppressed argument. In simpler terms, this theorem provides a reversed version of `Fin.cast_eq_cast`, making it easier to use in rewriting steps during proofs. More concisely: The theorem `Fin.cast_eq_cast'` asserts that for all natural numbers `n` and `m` and equality `h : Fin n = Fin m`, `cast h = Fin.cast n rwhere r is some suppressed argument.
`Fintype.one_lt_card_iff_nontrivial` theorem Fintype.one_lt_card_iff_nontrivial : ∀ {α : Type u_1} [inst : Fintype α], 1 < Fintype.card α ↔ Nontrivial α The theorem `Fintype.one_lt_card_iff_nontrivial` states that for any given finite type `α`, the number of elements (`Fintype.card α`) in `α` is greater than one if and only if `α` is nontrivial. In this context, a nontrivial type is one that has at least two distinct elements. Thus, this theorem is essentially relating the size of a finite type with its nontriviality. More concisely: A finite type `α` has more than one element if and only if `Fintype.card α` is greater than one.
`Fintype.induction_subsingleton_or_nontrivial` theorem Fintype.induction_subsingleton_or_nontrivial : ∀ {P : (α : Type u_4) → [inst : Fintype α] → Prop} (α : Type u_4) [inst : Fintype α], (∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α) → (∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], Fintype.card β < Fintype.card α → P β) → P α) → P α This theorem, `Fintype.induction_subsingleton_or_nontrivial`, is a custom induction principle for finite types. The base case of the induction is a subsingleton type, a type with at most one element. The induction step applies to non-trivial types, i.e., types with more than one element. In this case, the induction hypothesis can be assumed for all types smaller than the current one, where "smaller" is defined using the `Fintype.card` function, which returns the number of elements in the type. To apply this theorem using the `induction` tactic, you need to provide a specific instance of a finite type. The theorem helps to prove a proposition `P` for all finite types given that `P` holds for all subsingleton types and for all non-trivial types if `P` holds for all smaller finite types. More concisely: The theorem `Fintype.induction_subsingleton_or_nontrivial` states that given a proposition `P` holding for all subsingleton types and for all non-trivial finite types where `P` holds for smaller finite types, it holds for all finite types.
`Fintype.card_of_bijective` theorem Fintype.card_of_bijective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] {f : α → β}, Function.Bijective f → Fintype.card α = Fintype.card β The theorem `Fintype.card_of_bijective` states that for any two types `α` and `β`, both having finiteness property (instances of `Fintype`), if there exists a bijective function `f` from `α` to `β`, then the number of elements in `α` (represented by `Fintype.card α`) is equal to the number of elements in `β` (represented by `Fintype.card β`). Here, a function is bijective if it is both injective (no two different elements in `α` map to the same element in `β`) and surjective (for every element in `β`, there is an element in `α` that maps to it). More concisely: If `α` and `β` are finite types and there exists a bijective function from `α` to `β`, then `Fintype.card α = Fintype.card β`.
`Infinite.exists_superset_card_eq` theorem Infinite.exists_superset_card_eq : ∀ {α : Type u_1} [inst : Infinite α] (s : Finset α) (n : ℕ), s.card ≤ n → ∃ t, s ⊆ t ∧ t.card = n This theorem, `Infinite.exists_superset_card_eq`, states that for any type `α` that is infinite, any finite set `s` of type `α`, and any natural number `n`, if the cardinality of `s` is less than or equal to `n`, then there exists a superset `t` of `s` such that the cardinality of `t` is exactly `n`. In other words, it's always possible to find a larger set within the infinite set that has a specific desired cardinality, as long as that desired cardinality is greater than or equal to the size of the original set. More concisely: For any infinite type `α` and finite subset `s` of `α` with cardinality less than `n`, there exists a superset `t` of `s` with cardinality exactly `n`.
`Mathlib.Data.Fintype.Card._auxLemma.7` theorem Mathlib.Data.Fintype.Card._auxLemma.7 : ∀ {α : Type u_1} [inst : Fintype α] (x : α), (x ∈ Finset.univ) = True This theorem states that for any type `α` which is a finite type (denoted as `Fintype α`), any element `x` of type `α` is always contained in the universal finite set of type `α` (`Finset.univ`). In other words, for a given finite type, every element of that type is included in the universal set of that type. More concisely: For any finite type `α`, every element of `α` belongs to the universal finite set `Finset.univ` of type `Finset α`.
`Function.Embedding.nonempty_of_card_le` theorem Function.Embedding.nonempty_of_card_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β], Fintype.card α ≤ Fintype.card β → Nonempty (α ↪ β) This theorem states that for any two types `α` and `β`, both of which have a finite number of elements (fintype), if the number of elements in `α` is less than or equal to the number of elements in `β` (`Fintype.card α ≤ Fintype.card β`), then there exists a function that can embed `α` into `β` without any collisions (i.e., it is an injective function from `α` to `β`). In mathematical notation, this means that if \|α\| ≤ \|β\|, then there exists a function f: α ↪ β. More concisely: If `α` and `β` are types with finite numbers of elements such that the cardinality of `α` is less than or equal to that of `β`, then there exists an injective function from `α` to `β`.
`Infinite.of_surjective_from_set` theorem Infinite.of_surjective_from_set : ∀ {α : Type u_1} {s : Set α}, s ≠ Set.univ → ∀ {f : ↑s → α}, Function.Surjective f → Infinite α The theorem `Infinite.of_surjective_from_set` states that for any type `α` and any set `s` of type `α`, if `s` is not equal to the universal set of type `α` (i.e., `s` is a proper subset of `α`), and if there exists a surjective function `f` from the elements of `s` to `α` (means for every element in `α`, there is an element in `s` such that applying `f` to that element returns the given element of `α`), then the type `α` is infinite. In other words, if we have a proper subset of a type and a function from that subset onto the entire type, the type must have infinitely many elements. More concisely: If a subset of a type is non-empty, proper, and has a surjective function to the type, then the type is infinite.
`fin_injective` theorem fin_injective : Function.Injective Fin The theorem `fin_injective` states that the function `Fin` is injective when applied as a mapping from natural numbers (`ℕ`) to types (`Type`). In other words, if two natural numbers map to the same type when subjected to the `Fin` function, then those two natural numbers must have been the same. However, it's worth noting that since this theorem pertains to equality of types, it's recommended to avoid using it whenever possible. More concisely: The theorem `fin_injective` asserts that the `Fin` function maps distinct natural numbers to distinct types.
`Infinite.of_injective_to_set` theorem Infinite.of_injective_to_set : ∀ {α : Type u_1} {s : Set α}, s ≠ Set.univ → ∀ {f : α → ↑s}, Function.Injective f → Infinite α The theorem `Infinite.of_injective_to_set` states that for any type `α` and any set `s` of type `α`, if `s` is not the universal set (meaning `s` is a proper subset of `α`) and there is an injective function `f` from `α` to `s`, then `α` must be infinite. In other words, if there is a one-to-one function from a type to a proper subset of the type, then that type has an infinite number of elements. More concisely: If `α` is a type, `s` is a proper subset of `α`, and there exists an injective function from `α` to `s`, then `α` is infinite.
`Fintype.bijective_iff_surjective_and_card` theorem Fintype.bijective_iff_surjective_and_card : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Function.Bijective f ↔ Function.Surjective f ∧ Fintype.card α = Fintype.card β This theorem states that for all types `α` and `β` where both are finite types (indicated by `Fintype α` and `Fintype β`), a function `f` mapping from `α` to `β` is bijective if and only if two conditions are met: The function `f` is surjective (meaning that for every element `b` in `β`, there exists at least one `a` in `α` such that `f(a) = b`), and the cardinality of `α` (the number of elements in `α`) is equal to the cardinality of `β`. This theorem thus connects the concepts of bijectivity, surjectivity, and same cardinality in the context of finite types. More concisely: A function between two finite types is bijective if and only if it is surjective and the sizes of the types are equal.
`Fintype.card_compl_eq_card_compl` theorem Fintype.card_compl_eq_card_compl : ∀ {α : Type u_1} [inst : Finite α] (p q : α → Prop) [inst : Fintype { x // p x }] [inst_1 : Fintype { x // ¬p x }] [inst_2 : Fintype { x // q x }] [inst_3 : Fintype { x // ¬q x }], Fintype.card { x // p x } = Fintype.card { x // q x } → Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x } The theorem `Fintype.card_compl_eq_card_compl` states that for any finite type `α`, if the subtypes of `α` characterized by properties `p` and `q` have the same cardinality, then the complements of these subtypes within `α` also have the same cardinality. Here, a subtype characterized by a property `p` refers to the subset of `α` consisting of elements for which `p` holds, and the complement of such a subtype is the subset consisting of elements for which `p` does not hold. More concisely: For any finite type `α` and properties `p` and `q`, if the subsets of `α` defined by `p` and `q` have equal cardinalities, then so do their complements.
`Fintype.card_eq_zero_iff` theorem Fintype.card_eq_zero_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α = 0 ↔ IsEmpty α The theorem `Fintype.card_eq_zero_iff` states that for any type `α` which has a finite number of elements (i.e., is a `Fintype`), the number of elements (`Fintype.card α`) is equal to zero if and only if `α` is empty (i.e., `IsEmpty α`). In other words, a finite type has zero elements precisely when it is an empty type. More concisely: For any type `α` that is a `Fintype`, `Fintype.card α = 0` if and only if `α` is empty.
`Fintype.card_coe` theorem Fintype.card_coe : ∀ {α : Type u_1} (s : Finset α) [inst : Fintype { x // x ∈ s }], Fintype.card { x // x ∈ s } = s.card The theorem `Fintype.card_coe` states that for any type `α` and any finite set `s` of elements of type `α`, the cardinality (i.e., the number of elements) of the subtype consisting of elements in `s` is equal to the cardinality of `s` itself. In other words, if you restrict your attention to only those elements in `s`, the number of such elements doesn't change. More concisely: For any finite type `α` and subset `s` of `α`, the cardinality of the subtype of `α` equal to `s` is equal to the cardinality of `s`.
`finite_iff_nonempty_fintype` theorem finite_iff_nonempty_fintype : ∀ (α : Type u_4), Finite α ↔ Nonempty (Fintype α) This theorem states that, for any type `α`, `α` is finite if and only if there exists a finite type instance for `α`. In other words, a type is considered finite if it can be associated with a finite type, which is a type with a finite number of distinct values. Theorem `finite_iff_nonempty_fintype` provides a characterization of finite types in terms of the existence of a finite type instance. More concisely: A type `α` is finite if and only if there exists a finite type instance for it.
`Fintype.bijective_iff_injective_and_card` theorem Fintype.bijective_iff_injective_and_card : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Function.Bijective f ↔ Function.Injective f ∧ Fintype.card α = Fintype.card β This theorem states that for all types `α` and `β` which have a finite number of elements (also called as "finite types" or "fintypes"), a function `f` from `α` to `β` is bijective if and only if it is injective (meaning that different inputs yield different outputs) and the number of elements in `α` is the same as the number of elements in `β`. In mathematical terms, this can be written as: if `f: α → β` is a function between two finite sets `α` and `β`, then `f` is a bijection if and only if `f` is injective and the cardinality of `α` is equal to the cardinality of `β`. More concisely: A function between two finite sets is bijective if and only if it is injective and the cardinalities of the sets are equal.
`Finite.exists_ne_map_eq_of_infinite` theorem Finite.exists_ne_map_eq_of_infinite : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Infinite α] [inst : Finite β] (f : α → β), ∃ x y, x ≠ y ∧ f x = f y := by sorry This theorem is a statement of the pigeonhole principle for the case where there are infinitely many 'pigeons' and finitely many 'pigeonholes'. In this context, 'pigeons' and 'pigeonholes' are elements and sets of elements, respectively, from abstract types `α` and `β`. If `α` is infinite and `β` is finite, and there exists a function `f` that maps elements of `α` to elements of `β`, this theorem states that there must exist two distinct elements `x` and `y` in `α` such that they both map to the same element in `β` under the function `f`. This is essentially saying if you have more items (infinite) than containers (finite), at least two items must share a container. More concisely: If `α` is infinite and `β` is finite, and `f : α → β` is a function, then there exist distinct `x, y ∈ α` such that `f(x) = f(y)`.
`not_injective_infinite_finite` theorem not_injective_infinite_finite : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Infinite α] [inst : Finite β] (f : α → β), ¬Function.Injective f The theorem `not_injective_infinite_finite` states that for any two types `α` and `β`, if `α` is infinite and `β` is finite, then any function `f` from `α` to `β` cannot be injective. In other words, there does not exist a function that maps distinct elements of an infinite set to distinct elements of a finite set. More concisely: If `α` is infinite and `β` is finite, then no function from `α` to `β` can be injective.
`Finset.card_le_univ` theorem Finset.card_le_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card ≤ Fintype.card α The theorem `Finset.card_le_univ` states that for any given type `α` that is a finite type (i.e., has a `Fintype` instance), the number of elements (`card`) in any finite set (`Finset`) `s` of that type will always be less than or equal to the total number of elements in the type `α` itself. This is essentially a statement about the cardinality of subsets in a finite universal set, and corresponds to the intuitive idea that a subset can't be larger than the whole set. More concisely: For any finite type `α` and finite set `s` of type `α`, the cardinality of `s` is less than or equal to the cardinality of `α`.
`Finset.card_compl` theorem Finset.card_compl : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α), sᶜ.card = Fintype.card α - s.card := by sorry The theorem `Finset.card_compl` states that for any given type `α` that has decidable equality and is finite (i.e., it is a fintype), and for any finite set `s` of type `α`, the number of elements in the complement of `s` (`sᶜ.card`) is equal to the difference between the total number of elements of type `α` (`Fintype.card α`) and the number of elements in `s` (`s.card`). In other words, it captures the intuitive idea that the size of the complement of a set is the size of the whole space minus the size of the set itself. More concisely: For any finite type `α` with decidable equality and any finite set `s` of type `α`, the cardinality of the complement `sᶜ` is equal to the total cardinality of `α` minus the cardinality of `s`.
`Fintype.card_of_isEmpty` theorem Fintype.card_of_isEmpty : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : IsEmpty α], Fintype.card α = 0 := by sorry The theorem `Fintype.card_of_isEmpty` states that for any type `α` which is both a fintype (i.e., a finite type) and empty (i.e., it contains no elements), the cardinality (or number of elements) of `α` is zero. This is a direct consequence of the definition of an empty set, which has no elements and thus a cardinality of zero. More concisely: If a type is both empty and a fintype, then its cardinality is zero.
`Fintype.card_le_of_embedding` theorem Fintype.card_le_of_embedding : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β], (α ↪ β) → Fintype.card α ≤ Fintype.card β The theorem `Fintype.card_le_of_embedding` states that for any two types `α` and `β`, given that both `α` and `β` are fintypes (i.e., they have a finite number of elements), if there exists an injective function (also known as an embedding) from `α` to `β`, then the cardinality (or the number of elements) of `α` is less than or equal to the cardinality of `β`. In simpler terms, if we can map each element of `α` to a unique element in `β` without any overlaps, then `α` cannot have more elements than `β`. More concisely: If `α` and `β` are fintypes and there exists an injective function from `α` to `β`, then `#α ≤ #β`. (Here, `#α` and `#β` represent the cardinalities of `α` and `β`, respectively.)
`Fintype.card_pos_iff` theorem Fintype.card_pos_iff : ∀ {α : Type u_1} [inst : Fintype α], 0 < Fintype.card α ↔ Nonempty α The theorem `Fintype.card_pos_iff` states that for any type `α` that is finite (`Fintype α`), the number of elements in `α` (given by `Fintype.card α`) is greater than zero if and only if `α` is not empty. In other words, a finite type has more than zero elements exactly when there is at least one element in it. More concisely: A finite type `α` has more elements than zero if and only if `α` is non-empty. (Equivalently, `Fintype.card α > 0 iff ∃x, x ∈ α`)
`Fintype.exists_ne_map_eq_of_card_lt` theorem Fintype.exists_ne_map_eq_of_card_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Fintype.card β < Fintype.card α → ∃ x y, x ≠ y ∧ f x = f y This theorem is a formalization of the pigeonhole principle for finite types. The pigeonhole principle states that if you have more pigeons than pigeonholes, then there must be at least one pigeonhole with more than one pigeon. In this case, the theorem states that for any two finite types α and β, and any function `f` from α to β, if the cardinality (or size) of β is less than the cardinality of α, then there must be two different elements `x` and `y` in α such that `f(x)` is equal to `f(y)`. In other words, the function `f` cannot be injective. More concisely: If `α` and `β` are finite types with `\|β\| < \|α\|`, then there exist distinct `x, y ∈ α` such that `f(x) = f(y)` for any function `f : α → β`.
`nonempty_fintype` theorem nonempty_fintype : ∀ (α : Type u_4) [inst : Finite α], Nonempty (Fintype α) This theorem, `nonempty_fintype`, asserts that for any type `α` which is finite (as expressed by the typeclass `Finite α`), there exists a finite type instance `Fintype α`. In simpler terms, whenever we have a finite type, it is guaranteed that there is a corresponding finite type instance available. More concisely: For any finite type `α`, there exists a finite type instance `Fintype α`.
`Fintype.one_lt_card` theorem Fintype.one_lt_card : ∀ {α : Type u_1} [inst : Fintype α] [h : Nontrivial α], 1 < Fintype.card α The theorem `Fintype.one_lt_card` states that for any type `α` that belongs to the class `Fintype` (meaning that it has a finite number of elements) and is `Nontrivial` (meaning that it has at least two distinct elements), the cardinality of `α` (denoted by `Fintype.card α`) is strictly greater than 1. In other words, any nontrivial finite set has more than one element. More concisely: For any nontrivial finite type α, its cardinality is greater than 1.

LeanAide GPT-4 documentation

Module: Mathlib.Data.Fintype.Card

Fintype.card_eq_zero

theorem Fintype.card_eq_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : IsEmpty α], Fintype.card α = 0

Fintype.card_le_one_iff

theorem Fintype.card_le_one_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α ≤ 1 ↔ ∀ (a b : α), a = b := by sorry

Fintype.card_pos

theorem Fintype.card_pos : ∀ {α : Type u_1} [inst : Fintype α] [h : Nonempty α], 0 < Fintype.card α

Function.Surjective.bijective_of_finite

theorem Function.Surjective.bijective_of_finite : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Surjective f → Function.Bijective f

Fintype.finite

theorem Fintype.finite : ∀ {α : Type u_4}, Fintype α → Finite α

Infinite.of_surjective

theorem Infinite.of_surjective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Infinite β] (f : α → β), Function.Surjective f → Infinite α

Finite.of_surjective

theorem Finite.of_surjective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Finite α] (f : α → β), Function.Surjective f → Finite β

Infinite.of_not_fintype

theorem Infinite.of_not_fintype : ∀ {α : Type u_1}, (Fintype α → False) → Infinite α

Finite.injective_iff_bijective

theorem Finite.injective_iff_bijective : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Injective f ↔ Function.Bijective f

Finset.card_eq_iff_eq_univ

theorem Finset.card_eq_iff_eq_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card = Fintype.card α ↔ s = Finset.univ

Fintype.card_ulift

theorem Fintype.card_ulift : ∀ (α : Type u_4) [inst : Fintype α], Fintype.card (ULift.{u_5, u_4} α) = Fintype.card α

Finite.exists_infinite_fiber

theorem Finite.exists_infinite_fiber : ∀ {α : Type u_1} {β : Type u_2} [inst : Infinite α] [inst : Finite β] (f : α → β), ∃ y, Infinite ↑(f ⁻¹' {y}) := by sorry

Function.Injective.surjective_of_fintype

theorem Function.Injective.surjective_of_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] {f : α → β}, α ≃ β → Function.Injective f → Function.Surjective f

Fintype.card_ne_zero

theorem Fintype.card_ne_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α], Fintype.card α ≠ 0

Finite.of_injective

theorem Finite.of_injective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Finite β] (f : α → β), Function.Injective f → Finite α

Infinite.of_injective

theorem Infinite.of_injective : ∀ {α : Sort u_4} {β : Sort u_5} [inst : Infinite β] (f : β → α), Function.Injective f → Infinite α

Fintype.card_eq_one_iff

theorem Fintype.card_eq_one_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α = 1 ↔ ∃ x, ∀ (y : α), y = x := by sorry

Fintype.card_ofFinset

theorem Fintype.card_ofFinset : ∀ {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p), Fintype.card ↑p = s.card

Finite.wellFounded_of_trans_of_irrefl

theorem Finite.wellFounded_of_trans_of_irrefl : ∀ {α : Type u_1} [inst : Finite α] (r : α → α → Prop) [inst : IsTrans α r] [inst : IsIrrefl α r], WellFounded r

Fintype.card_eq

theorem Fintype.card_eq : ∀ {α : Type u_4} {β : Type u_5} [_F : Fintype α] [_G : Fintype β], Fintype.card α = Fintype.card β ↔ Nonempty (α ≃ β)

List.exists_pw_disjoint_with_card

theorem List.exists_pw_disjoint_with_card : ∀ {α : Type u_4} [inst : Fintype α] {c : List ℕ}, c.sum ≤ Fintype.card α → ∃ o, List.map List.length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ List.Pairwise List.Disjoint o

Finset.eq_univ_of_card

theorem Finset.eq_univ_of_card : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card = Fintype.card α → s = Finset.univ

Fintype.card_le_of_surjective

theorem Fintype.card_le_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Function.Surjective f → Fintype.card β ≤ Fintype.card α

Fintype.subtype_card

theorem Fintype.subtype_card : ∀ {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x), Fintype.card { x // p x } = s.card

Fintype.card_congr'

theorem Fintype.card_congr' : ∀ {α β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β], α = β → Fintype.card α = Fintype.card β

Function.Embedding.isEmpty_of_card_lt

theorem Function.Embedding.isEmpty_of_card_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β], Fintype.card β < Fintype.card α → IsEmpty (α ↪ β)

Mathlib.Data.Fintype.Card._auxLemma.12

theorem Mathlib.Data.Fintype.Card._auxLemma.12 : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Injective f = Function.Surjective f

Fintype.card_subtype_le

theorem Fintype.card_subtype_le : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p], Fintype.card { x // p x } ≤ Fintype.card α

Fintype.card_ofSubsingleton

theorem Fintype.card_ofSubsingleton : ∀ {α : Type u_1} (a : α) [inst : Subsingleton α], Fintype.card α = 1

Mathlib.Data.Fintype.Card._auxLemma.1

theorem Mathlib.Data.Fintype.Card._auxLemma.1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α], (Fintype.card α = 0) = False

Infinite.exists_subset_card_eq

theorem Infinite.exists_subset_card_eq : ∀ (α : Type u_4) [inst : Infinite α] (n : ℕ), ∃ s, s.card = n

Function.Surjective.injective_of_fintype

theorem Function.Surjective.injective_of_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] {f : α → β}, α ≃ β → Function.Surjective f → Function.Injective f

Finset.card_fin

theorem Finset.card_fin : ∀ (n : ℕ), Finset.univ.card = n

Fintype.card_fin

theorem Fintype.card_fin : ∀ (n : ℕ), Fintype.card (Fin n) = n

Fintype.card_of_finset'

theorem Fintype.card_of_finset' : ∀ {α : Type u_1} {p : Set α} (s : Finset α), (∀ (x : α), x ∈ s ↔ x ∈ p) → ∀ [inst : Fintype ↑p], Fintype.card ↑p = s.card

Fintype.card_le_of_injective

theorem Fintype.card_le_of_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β), Function.Injective f → Fintype.card α ≤ Fintype.card β

Fintype.card_le_one_iff_subsingleton

theorem Fintype.card_le_one_iff_subsingleton : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α ≤ 1 ↔ Subsingleton α

Function.Injective.bijective_of_finite

theorem Function.Injective.bijective_of_finite : ∀ {α : Type u_1} [inst : Finite α] {f : α → α}, Function.Injective f → Function.Bijective f

Fintype.card_unit

theorem Fintype.card_unit : Fintype.card Unit = 1

`Fintype.card_eq_zero`

`Fintype.card_le_one_iff`

`Fintype.card_pos`

`Function.Surjective.bijective_of_finite`

`Fintype.finite`

`Infinite.of_surjective`

`Finite.of_surjective`

`Infinite.of_not_fintype`

`Finite.injective_iff_bijective`

`Finset.card_eq_iff_eq_univ`

`Fintype.card_ulift`

`Finite.exists_infinite_fiber`

`Function.Injective.surjective_of_fintype`

`Fintype.card_ne_zero`

`Finite.of_injective`

`Infinite.of_injective`

`Fintype.card_eq_one_iff`

`Fintype.card_ofFinset`

`Finite.wellFounded_of_trans_of_irrefl`

`Fintype.card_eq`

`List.exists_pw_disjoint_with_card`

`Finset.eq_univ_of_card`

`Fintype.card_le_of_surjective`

`Fintype.subtype_card`

`Fintype.card_congr'`

`Function.Embedding.isEmpty_of_card_lt`

`Mathlib.Data.Fintype.Card._auxLemma.12`

`Fintype.card_subtype_le`

`Fintype.card_ofSubsingleton`

`Mathlib.Data.Fintype.Card._auxLemma.1`

`Infinite.exists_subset_card_eq`

`Function.Surjective.injective_of_fintype`

`Finset.card_fin`

`Fintype.card_fin`

`Fintype.card_of_finset'`

`Fintype.card_le_of_injective`

`Fintype.card_le_one_iff_subsingleton`

`Function.Injective.bijective_of_finite`

`Fintype.card_unit`

`Fintype.card_lt_of_injective_of_not_mem`

`Finset.card_univ`

`Fintype.ofEquiv_card`

`Set.toFinset_card`

`Fintype.card_congr`

`Finite.injective_iff_surjective`

`Fintype.card_unique`

`Fintype.card_of_subtype`

`Infinite.exists_not_mem_finset`

`card_finset_fin_le`

`Fintype.card_subtype_compl`

`Fin.cast_eq_cast'`

`Fintype.one_lt_card_iff_nontrivial`

`Fintype.induction_subsingleton_or_nontrivial`

`Fintype.card_of_bijective`

`Infinite.exists_superset_card_eq`

`Mathlib.Data.Fintype.Card._auxLemma.7`

`Function.Embedding.nonempty_of_card_le`

`Infinite.of_surjective_from_set`

`fin_injective`

`Infinite.of_injective_to_set`

`Fintype.bijective_iff_surjective_and_card`

`Fintype.card_compl_eq_card_compl`

`Fintype.card_eq_zero_iff`

`Fintype.card_coe`

`finite_iff_nonempty_fintype`

`Fintype.bijective_iff_injective_and_card`

`Finite.exists_ne_map_eq_of_infinite`

`not_injective_infinite_finite`

`Finset.card_le_univ`

`Finset.card_compl`

`Fintype.card_of_isEmpty`

`Fintype.card_le_of_embedding`

`Fintype.card_pos_iff`

`Fintype.exists_ne_map_eq_of_card_lt`