Finite.of_not_infinite
theorem Finite.of_not_infinite : ∀ {α : Sort u_1}, ¬Infinite α → Finite α
This theorem, referred to as `Finite.of_not_infinite`, states that for all types `α`, if `α` is not infinite, then `α` is finite. In other words, it establishes the forward direction of the equivalence between the negation of infinite and finite for any given type. This essentially captures the intuitive understanding of an absence of infiniteness implying finiteness.
More concisely: If a type `α` is not infinite, then `α` is finite.
|
Infinite.not_finite
theorem Infinite.not_finite : ∀ {α : Sort u_3} [self : Infinite α], ¬Finite α
This theorem states that for any type `α`, if `α` is infinite (denoted by `Infinite α`), then it cannot be finite (denoted by `¬Finite α`). This is a universal principle that applies to all types `α`. It reflects the fundamental concept in mathematics that a set cannot be both finite and infinite at the same time.
More concisely: For any type `α`, if it is infinite (`Infinite α`), then it cannot be finite (`¬Finite α`). In other words, an infinite type is not finite.
|
not_finite
theorem not_finite : ∀ (α : Sort u_3) [inst : Infinite α] [inst : Finite α], False
This theorem states that a type `α` cannot be both `Infinite` and `Finite` at the same time. In other words, it's impossible for a type to simultaneously possess both the `Infinite` and `Finite` properties. This theorem is a contradiction, meaning that if you assume that a type is both `Infinite` and `Finite`, you will end up with a contradiction (denoted by `False` in Lean).
More concisely: A type cannot be both infinite and finite.
|
Infinite.false
theorem Infinite.false : ∀ {α : Sort u_1} [inst : Finite α], Infinite α → False
This theorem states that for any type α, if α is finite, then it cannot be infinite. In other words, it's a contradiction to assert that a certain type is both finite and infinite at the same time. This is represented by the `False` return value, which in Lean's logic represents a contradiction or an impossible scenario.
More concisely: A finite type cannot be infinite.
|
not_finite_iff_infinite
theorem not_finite_iff_infinite : ∀ {α : Sort u_1}, ¬Finite α ↔ Infinite α
This theorem states that for any type `α`, it is not finite if and only if it is infinite. In other words, a type `α` is infinite if it is not finite, and vice versa. This provides a direct connection between the two concepts of finiteness and infiniteness.
More concisely: A type `α` is infinite if and only if it is not finite.
|
Finite.false
theorem Finite.false : ∀ {α : Sort u_1} [inst : Infinite α], Finite α → False
This theorem is stating that for any type `α`, if `α` is infinite (as denoted by the `Infinite α` instance), then it cannot also be finite (`Finite α`). In other words, a type can't be both finite and infinite at the same time. If we assume that `α` is both finite and infinite, we arrive at a contradiction, which is the `False` in the theorem statement.
More concisely: A type cannot be both finite and infinite.
|
Equiv.finite_iff
theorem Equiv.finite_iff : ∀ {α : Sort u_1} {β : Sort u_2}, α ≃ β → (Finite α ↔ Finite β)
This theorem states that for any two types `α` and `β`, if `α` is equivalent to `β` (expressed as `α ≃ β` in Lean), then `α` is finite if and only if `β` is finite. In other words, the finiteness of `α` and `β` is equivalent if `α` and `β` are equivalent. This theorem is an important property of equivalence relations and finiteness in the context of type theory.
More concisely: For any types `α` and `β`, if `α ≃ β`, then `α` is finite if and only if `β` is finite.
|
Finite.exists_equiv_fin
theorem Finite.exists_equiv_fin : ∀ (α : Sort u_3) [h : Finite α], ∃ n, Nonempty (α ≃ Fin n)
For any type or sort `α` that is finite (as indicated by `h : Finite α`), there exists a natural number `n` such that there is a nonempty equivalence between type `α` and the finite sequence of natural numbers less than `n` (denoted by `Fin n`). Essentially, this theorem states that we can map any finite type to a finite sequence of natural numbers.
More concisely: For any finite type `α`, there exists a natural number `n` such that there exists a bijective function from `α` to `Fin n`.
|
Finite.not_infinite
theorem Finite.not_infinite : ∀ {α : Sort u_1}, Finite α → ¬Infinite α
This theorem, named `Finite.not_infinite`, states that for any type `α`, if `α` is finite, then it cannot be infinite. It is an alias for the reverse direction of another theorem `not_infinite_iff_finite`. In other words, it establishes that the property of being finite is the negation of the property of being infinite in a certain type.
More concisely: If a type `α` is finite, then it is not infinite.
|
finite_or_infinite
theorem finite_or_infinite : ∀ (α : Sort u_3), Finite α ∨ Infinite α
This theorem states that for any type `α`, it is either finite (`Finite α`) or infinite (`Infinite α`). In more traditional mathematical terms, given any set `α`, it either has a finite number of elements or an infinite number of elements. The `Finite` and `Infinite` classes in Lean are used to represent these two possibilities.
More concisely: Every set can be classified as finite or infinite.
|
Finite.of_equiv
theorem Finite.of_equiv : ∀ {β : Sort u_2} (α : Sort u_3) [h : Finite α], α ≃ β → Finite β
This theorem, `Finite.of_equiv`, states that for any types `α` and `β`, if `α` is finite and there exists an equivalence between `α` and `β`, then `β` is also finite. The theorem relies on the assumption that there is a one-to-one correspondence (bijective function) between `α` and `β`, meaning that each element in `α` corresponds to a unique element in `β` and vice versa, hence their sizes are identical. Therefore, if `α` is finite, `β` must also be finite.
More concisely: If `α` is a finite type and there exists a bijection between `α` and `β`, then `β` is also finite.
|
Equiv.infinite_iff
theorem Equiv.infinite_iff : ∀ {α : Sort u_1} {β : Sort u_2}, α ≃ β → (Infinite α ↔ Infinite β)
This theorem states that for any two types `α` and `β`, if `α` is equivalent to `β` (denoted as `α ≃ β`), then `α` is infinite if and only if `β` is infinite. In the context of set theory, two types are equivalent if there is a bijection between them. Therefore, this theorem essentially says that the property of being infinite is preserved under bijection.
More concisely: If `α` is equivalent to `β` (`α ≃ β`), then `α` is infinite if and only if `β` is infinite.
|