Finite.card_eq_zero_of_surjective
theorem Finite.card_eq_zero_of_surjective :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Nat.card β = 0 → Nat.card α = 0
The theorem `Finite.card_eq_zero_of_surjective` states that for all types `α` and `β` and for any function `f` from `α` to `β`, if `f` is a surjective function and the cardinality of `β` (expressed as a natural number `Nat.card β`) is zero, then the cardinality of `α` (expressed as `Nat.card α`) is also zero. In mathematical terms, this theorem says that if every element of `β` is the image of some element of `α` under `f` (i.e., `f` is surjective), and if `β` is infinite (since its cardinality is defined to be zero for infinite sets), then `α` must also be infinite.
More concisely: If a surjective function maps between non-empty sets, then they have the same infinite cardinality. (Assuming the cardinality of an empty set is considered to be zero in the given context.)
|
Finite.card_le_of_injective'
theorem Finite.card_le_of_injective' :
∀ {α : Type u_1} {β : Type u_2} {f : α → β},
Function.Injective f → (Nat.card β = 0 → Nat.card α = 0) → Nat.card α ≤ Nat.card β
The theorem `Finite.card_le_of_injective'` states that for any two types `α` and `β`, and a function `f` from `α` to `β`, if `f` is injective, then the cardinality of `α` (as a natural number) is less than or equal to the cardinality of `β`. However, the theorem also requires an additional assumption that if the cardinality of `β` is zero (which Lean 4 interprets as `β` being infinite), then the cardinality of `α` must also be zero. In other words, if `β` is infinite and `α` is not, then `f` cannot be injective.
More concisely: If `α` and `β` are types, `f` is a function from `α` to `β`, and `f` is injective, then `|α| ≤ |β|` provided `β` is not empty.
|
Finite.card_le_of_injective
theorem Finite.card_le_of_injective :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite β] (f : α → β), Function.Injective f → Nat.card α ≤ Nat.card β := by
sorry
The theorem `Finite.card_le_of_injective` states that for any two types `α` and `β`, where `β` is finite, and a function `f` from `α` to `β`, if the function `f` is injective, then the cardinality of `α` as a natural number, represented by `Nat.card α`, is less than or equal to the cardinality of `β`, represented by `Nat.card β`. In other words, the size of the domain of an injective function cannot exceed the size of the codomain, when the codomain is finite.
More concisely: If `α` is a type, `β` is finite, and `f : α → β` is injective, then `Nat.card α ≤ Nat.card β`.
|
Mathlib.Data.Finite.Card._auxLemma.4
theorem Mathlib.Data.Finite.Card._auxLemma.4 : ∀ {α : Type u} [inst : LE α] {x y : α}, (x ≥ y) = (y ≤ x)
This theorem, named `Mathlib.Data.Finite.Card._auxLemma.4`, states that for any type `α` with a less than or equal to (`≤`) operation, and for any two elements `x` and `y` of type `α`, the statement that `x` is greater than or equal to (`≥`) `y` is equivalent to the statement that `y` is less than or equal to (`≤`) `x`.
More concisely: For any type `α` with a total order and any `x, y` in `α`, `x ≥ y` is equivalent to `y ≤ x`.
|
Finite.card_le_of_surjective
theorem Finite.card_le_of_surjective :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] (f : α → β), Function.Surjective f → Nat.card β ≤ Nat.card α := by
sorry
This theorem states that for any two types `α` and `β`, if `α` is finite and there exists a surjective function `f` from `α` to `β` (meaning each element of `β` can be obtained from applying `f` to some element of `α`), then the cardinality of `β` (expressed as a natural number by `Nat.card β`) is less than or equal to the cardinality of `α` (expressed as `Nat.card α`). In mathematical terms, if `f: α -> β` is surjective and the set `α` is finite, then the cardinality of `β` is less than or equal to the cardinality of `α`.
More concisely: If `α` is a finite type and there exists a surjective function `f: α -> β`, then `Nat.card β <= Nat.card α`.
|
Finite.card_eq_zero_of_injective
theorem Finite.card_eq_zero_of_injective :
∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] {f : α → β},
Function.Injective f → Nat.card α = 0 → Nat.card β = 0
The theorem `Finite.card_eq_zero_of_injective` states that for any two types `α` and `β`, where `α` is nonempty, and any injective function `f` from `α` to `β`, if the cardinality of `α` as a natural number is zero (which is defined to mean that `α` is an infinite type), then the cardinality of `β` as a natural number is also zero, implying that `β` is also an infinite type. This theorem essentially says that an injective function cannot map an infinite set to a finite set.
More concisely: If `α` is a nonempty type with cardinality zero and `f` is an injective function from `α` to `β`, then `β` also has cardinality zero.
|
Finite.card_le_of_surjective'
theorem Finite.card_le_of_surjective' :
∀ {α : Type u_1} {β : Type u_2} {f : α → β},
Function.Surjective f → (Nat.card α = 0 → Nat.card β = 0) → Nat.card β ≤ Nat.card α
This theorem states that for any two types `α` and `β` and a function `f` from `α` to `β`, if `f` is surjective (i.e., every element of `β` is the image of some element of `α` under `f`), then the cardinality of `β` as a natural number (`Nat.card β`) is less than or equal to the cardinality of `α` as a natural number (`Nat.card α`). However, we must also assume that if `α` is infinite (which is represented as `Nat.card α = 0`), then `β` must also be infinite (which is represented as `Nat.card β = 0`), since the `Nat.card` function is defined to be `0` for infinite types.
More concisely: If `α` and `β` are types and `f : α → β` is a surjective function, then `Nat.card α ≥ Nat.card β` under the assumption that `Nat.card α = 0` if and only if `Nat.card β = 0`.
|
Finite.card_pos
theorem Finite.card_pos : ∀ {α : Type u_1} [inst : Finite α] [h : Nonempty α], 0 < Nat.card α
The theorem `Finite.card_pos` states that for any finite type `α` (denoted as `{α : Type u_1}`) which is nonempty (denoted as `[h : Nonempty α]`), the cardinality of `α` is strictly greater than 0. Here, cardinality is represented as a natural number by the function `Nat.card`. In simple words, a nonempty finite set always has a positive number of elements.
More concisely: For any nonempty finite type `α`, the cardinality of `α` is a positive natural number.
|
Finite.card_le_of_embedding'
theorem Finite.card_le_of_embedding' :
∀ {α : Type u_1} {β : Type u_2}, (α ↪ β) → (Nat.card β = 0 → Nat.card α = 0) → Nat.card α ≤ Nat.card β
This theorem states that for any two types `α` and `β`, if there exists an embedding function `f` from `α` to `β`, then the cardinality of `α` (denoted by `Nat.card α`) is less than or equal to the cardinality of `β` (denoted by `Nat.card β`). Additionally, it is assumed that if `β` is an infinite type (i.e., `Nat.card β = 0`), then `α` must also be an infinite type (i.e., `Nat.card α = 0`). This condition is necessary because `Nat.card` is defined to be `0` for infinite types.
More concisely: If `α` embeds into `β`, then `Nat.card α ≤ Nat.card β`, under the assumption that `β` is infinite implies `α` is infinite.
|
Finite.card_eq_zero_of_embedding
theorem Finite.card_eq_zero_of_embedding :
∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α], (α ↪ β) → Nat.card α = 0 → Nat.card β = 0
This theorem states that for any two types `α` and `β` with `α` being nonempty, if there exists an injective function (embedding) from `α` to `β`, and the cardinality of `α` (as computed by `Nat.card`) is 0, then the cardinality of `β` must also be 0. The cardinality, as computed by `Nat.card`, is the size of the set, but it is defined to be 0 for infinite sets. Thus, this theorem is saying that if `α` is infinite and there exists an injective map from `α` to `β`, then `β` must also be infinite.
More concisely: If `α` is a nonempty type with an injective function to an infinite `β`, then `β` is also infinite.
|