LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.SetTheory.Cardinal.Basic

`Cardinal.aleph0_le_lift` theorem Cardinal.aleph0_le_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph0 ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 ≤ c The theorem `Cardinal.aleph0_le_lift` states that for any cardinal number `c`, the smallest infinite cardinal, also known as aleph null (`Cardinal.aleph0`), is less than or equal to the universe lifter function (`Cardinal.lift`) applied to `c`, if and only if aleph null is less than or equal to `c` itself. In other words, the inequality between aleph null and `c` is preserved under the universe lifting operation. More concisely: For any cardinal number `c`, `Cardinal.aleph0 ≤Cardinal.lift c` if and only if `Cardinal.aleph0 ≤ c`.
`Cardinal.lift_mk_eq` theorem Cardinal.lift_mk_eq : ∀ {α : Type u} {β : Type v}, Cardinal.lift.{max v w, u} (Cardinal.mk α) = Cardinal.lift.{max u w, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β) This theorem, `Cardinal.lift_mk_eq`, states that for any types `α` and `β`, the lift to a higher universe of the cardinality of `α` is equal to the lift to a higher universe of the cardinality of `β` if and only if there exists a bijection between `α` and `β`. In other words, the cardinalities of two types are the same in some higher universe if and only if the types are isomorphic, which means there is a one-to-one correspondence between their elements. More concisely: The cardinalities of types `α` and `β` are equal in some higher universe if and only if there exists a bijection between them.
`Cardinal.lift_down` theorem Cardinal.lift_down : ∀ {a : Cardinal.{u}} {b : Cardinal.{max u v}}, b ≤ Cardinal.lift.{v, u} a → ∃ a', Cardinal.lift.{v, u} a' = b := by sorry The theorem `Cardinal.lift_down` states that for any two cardinal numbers `a` and `b`, where `a` is from universe `u` and `b` is from the maximum universe of `u` and `v`, if `b` is less than or equal to the lift of `a` (which is the cardinality of the universe `u` lifted to the maximum universe of `u` and `v`), then there exists a cardinal number `a'` such that the lift of `a'` equals `b`. In other words, the theorem guarantees the existence of a cardinal number `a'` in the lower universe `v` that when lifted to the higher universe matches `b`, provided `b` does not exceed the lift of `a`. More concisely: Given any cardinal numbers `a` from universe `u` and `b` from the maximum universe of `u` and `v`, if `b` is less than or equal to the lift of `a`, then there exists a cardinal number `a'` in `v` such that the lift of `a'` equals `b`.
`Cardinal.lift_mk_le'` theorem Cardinal.lift_mk_le' : ∀ {α : Type u} {β : Type v}, Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ↪ β) This theorem, `Cardinal.lift_mk_le'`, provides a specialized variant of `Cardinal.lift_mk_le` for particular universes. It states that for any types `α` and `β` that exist in universes `u` and `v` respectively, the lift of the cardinality of `α` from universe `v` to `u` is less than or equal to the lift of the cardinality of `β` from universe `u` to `v` if and only if there exists an injective function from `α` to `β`. This theorem is provided separately as Lean often struggles to apply this specialization automatically, thus aiding in avoiding the problem of manually establishing the specialization. More concisely: For types α and β in universes u and v respectively, the lift of the cardinality of α from universe v to u is less than or equal to the cardinality of β in universe u if and only if there exists an injection from α to β.
`Cardinal.mk_eq_zero_iff` theorem Cardinal.mk_eq_zero_iff : ∀ {α : Type u}, Cardinal.mk α = 0 ↔ IsEmpty α This theorem states that for any type `α`, the cardinality of `α` is equal to zero if and only if `α` is an empty type. In more mathematical terms, it asserts that the cardinal number of a type is zero if, and only if, that type has no elements. More concisely: The theorem asserts that for any type `α`, its cardinality equals zero if and only if `α` is empty.
`Cardinal.lift_id` theorem Cardinal.lift_id : ∀ (a : Cardinal.{u}), Cardinal.lift.{u, u} a = a The theorem `Cardinal.lift_id` states that for any cardinal number `a` in a given universe `u`, lifting `a` to the same universe `u` results in the cardinal number `a` itself. In other words, the process of lifting a cardinal to its own universe does not change its value. This is expressed in the language of Lean 4's type theory and cardinal arithmetic. More concisely: For any cardinal number `a` in universe `u`, `Cardinal.lift a = a`.
`Cardinal.sum_le_iSup` theorem Cardinal.sum_le_iSup : ∀ {ι : Type u} (f : ι → Cardinal.{u}), Cardinal.sum f ≤ Cardinal.mk ι * iSup f := by sorry The theorem `Cardinal.sum_le_iSup` asserts that, for any type `ι` and any function `f` from `ι` to cardinal numbers, the sum of the cardinal numbers (as given by the function `f`) is less than or equal to the product of the cardinality of the type `ι` and the indexed supremum of the function `f`. In more familiar mathematical terms, this is stating that for a collection of sets indexed by `ι`, the total cardinality (number of elements) across all sets is less than or equal to the number of sets times the largest set's cardinality. More concisely: For any type ι and function f from ι to cardinal numbers, the sum of the images of cardinal numbers under f is less than or equal to the product of the cardinality of ι and the supremum of f.
`Cardinal.le_mk_iff_exists_set` theorem Cardinal.le_mk_iff_exists_set : ∀ {c : Cardinal.{u}} {α : Type u}, c ≤ Cardinal.mk α ↔ ∃ p, Cardinal.mk ↑p = c This theorem establishes a relationship between a given cardinal and the cardinality of a type. It asserts that for any cardinal `c` and any type `α`, `c` is less than or equal to the cardinality of `α` if and only if there exists a set `p` such that the cardinality of `p` is equal to `c`. In other words, a cardinal number is smaller than or equal to the size of a type if and only if there is a subset of the type which has the same cardinality as the cardinal number. This connects the abstract concept of cardinality with the concrete idea of subsets of a given type. More concisely: For any cardinal `c` and type `α`, `c ≤ \|α\|` if and only if there exists a set `p ⊆ α` with `\|p\| = c`.
`Cardinal.lt_aleph0_iff_fintype` theorem Cardinal.lt_aleph0_iff_fintype : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Nonempty (Fintype α) := by sorry The theorem `Cardinal.lt_aleph0_iff_fintype` establishes an equivalence between two properties of a type `α`. On one hand, we have the property that the cardinality of `α` (i.e., the number of distinct elements in `α`) is strictly less than `ℵ₀` (the smallest infinite cardinal number, representing the size of the set of natural numbers). On the other hand, we have the property that `α` is a finite type (i.e., there are only finitely many distinct values of type `α`). The theorem states that these two properties are equivalent for any type `α`: `α` has fewer elements than the set of natural numbers if and only if `α` is a finite type. More concisely: A type `α` has fewer elements than `ℵ₀` if and only if it is a finite type.
`Cardinal.mk_le_mk_of_subset` theorem Cardinal.mk_le_mk_of_subset : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → Cardinal.mk ↑s ≤ Cardinal.mk ↑t := by sorry The theorem `Cardinal.mk_le_mk_of_subset` states that for any two sets `s` and `t` of any type `α`, if `s` is a subset of `t` (represented as `s ⊆ t`), then the cardinality of `s` is less than or equal to the cardinality of `t` (denoted as `Cardinal.mk ↑s ≤ Cardinal.mk ↑t`). Cardinality, represented by `Cardinal.mk`, is a measure of the "size" or number of elements in a set, so this theorem essentially asserts that a subset can't have more elements than the set it's contained within. More concisely: If `s` is a subset of `t`, then the cardinality of `s` is less than or equal to the cardinality of `t`.
`Cardinal.lift_iSup_le_lift_iSup` theorem Cardinal.lift_iSup_le_lift_iSup : ∀ {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{w}} {f' : ι' → Cardinal.{w'}}, BddAbove (Set.range f) → BddAbove (Set.range f') → ∀ {g : ι → ι'}, (∀ (i : ι), Cardinal.lift.{w', w} (f i) ≤ Cardinal.lift.{w, w'} (f' (g i))) → Cardinal.lift.{w', w} (iSup f) ≤ Cardinal.lift.{w, w'} (iSup f') The theorem `Cardinal.lift_iSup_le_lift_iSup` states that for any two types `ι` and `ι'` and any two functions `f : ι → Cardinal.{w}` and `f' : ι' → Cardinal.{w'}`, if both the set of cardinals produced by `f` and `f'` have upper bounds, then for any function `g : ι → ι'` such that for every `i` in `ι`, the lift of `f i` to a common universe is less than or equal to the lift of `f' (g i)`, it follows that the lift of the supremum of `f` to the common universe is less than or equal to the lift to the common universe of the supremum of `f'`. In terms of cardinality, this means that if every cardinal in the first set has a corresponding cardinal in the second set that is larger, then the largest cardinal in the first set is less than or equal to the largest cardinal in the second set after both have been lifted to a common universe. More concisely: If functions `f : ι → Cardinal.{w}` and `f' : ι' → Cardinal.{w'}` have upper bounds, and for all `i` in `ι`, `Cardinal.lift (f i) ≤ Cardinal.lift (f' (g i))` for some function `g : ι → ι'`, then `Cardinal.lift (⨆ x in ι, f x) ≤ Cardinal.lift (⨆ x in ι', f' x)`.
`Cardinal.lift_monotone` theorem Cardinal.lift_monotone : Monotone Cardinal.lift.{u_2, u_1} The theorem `Cardinal.lift_monotone` states that the function `Cardinal.lift`, which performs a universe lift operation on cardinals, is monotone. In other words, if we have two cardinals `a` and `b` such that `a ≤ b`, it implies that `Cardinal.lift a ≤ Cardinal.lift b`. Here, the notation `≤` denotes a preorder (a relation that is reflexive and transitive) on the cardinals. This property ensures that lifting does not decrease cardinality, and if one cardinal is less than or equal to another, the same relationship holds after their respective lifts. More concisely: The `Cardinal.lift` function preserves the preorder relation between cardinals, that is, if `a ≤ b` then `Cardinal.lift a ≤ Cardinal.lift b`.
`Cardinal.mk_preimage_of_subset_range_lift` theorem Cardinal.mk_preimage_of_subset_range_lift : ∀ {α : Type u} {β : Type v} (f : α → β), ∀ s ⊆ Set.range f, Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s)) The theorem `Cardinal.mk_preimage_of_subset_range_lift` states that for any types `α` and `β` and any function `f` from `α` to `β`, if a set `s` is a subset of the range of `f`, then the cardinality of `s` lifted from universe `u` to `v` is less than or equal to the cardinality of the preimage of `s` under the function `f` lifted from universe `v` to `u`. In more mathematical terms, given any set $s$ that is a subset of the image of a function $f : \alpha \rightarrow \beta$, the cardinality of $s$ when regard as an element of the larger universe (represented in Lean as `Cardinal.lift.{u, v} (Cardinal.mk ↑s)`) is always less than or equal to the cardinality of the set of all elements in $\alpha$ that map to an element in $s$ (represented in Lean as `Cardinal.mk ↑(f ⁻¹' s)`), when the latter is regarded as an element of the larger universe. More concisely: For any function `f` from type `α` to type `β` and subset `s` of `f`'s range, the lifted cardinality of `s` is less than or equal to the lifted cardinality of `f`'s preimage of `s`.
`Cardinal.mk_singleton` theorem Cardinal.mk_singleton : ∀ {α : Type u} (x : α), Cardinal.mk ↑{x} = 1 This theorem states that for any type `α` and a value `x` of that type, the cardinal number (or size) of the singleton set containing `x` is 1. In other words, the cardinality of a singleton set is always 1, regardless of which type and value we use to create it. More concisely: The cardinality of a singleton set is equal to 1.
`Cardinal.power_le_power_left` theorem Cardinal.power_le_power_left : ∀ {a b c : Cardinal.{u_1}}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c The theorem `Cardinal.power_le_power_left` states that for any three cardinal numbers `a`, `b`, and `c`, if `a` is not zero and `b` is less than or equal to `c`, then `a` raised to the power `b` is less than or equal to `a` raised to the power `c`. It illustrates a property of exponentiation in the context of cardinal numbers. More concisely: For any cardinal numbers `a`, `b`, and `c` with `a > 0` and `b <= c`, we have `a^b <= a^c`.
`Cardinal.mk_fintype` theorem Cardinal.mk_fintype : ∀ (α : Type u) [h : Fintype α], Cardinal.mk α = ↑(Fintype.card α) The theorem `Cardinal.mk_fintype` states that for any type `α` that is a finite type (i.e., it has a `Fintype α` instance), the cardinality of `α` (denoted by `Cardinal.mk α`) is equal to the natural number representation (indicated by `↑`) of the cardinality of `α` when `α` is considered as a finite type (given by `Fintype.card α`). In other words, this theorem is asserting that the cardinality of a finite type as a type is the same as its cardinality as a finite type. More concisely: For any finite type α, the cardinality of α as a type (`Cardinal.mk α`) equals the cardinality of α as a finite type (`Fintype.card α`).
`Cardinal.mk_iUnion_le` theorem Cardinal.mk_iUnion_le : ∀ {α ι : Type u} (f : ι → Set α), Cardinal.mk ↑(⋃ i, f i) ≤ Cardinal.mk ι * ⨆ i, Cardinal.mk ↑(f i) This theorem states that for any types `α` and `ι`, and for any function `f` that takes an element of type `ι` and returns a set of elements of type `α`, the cardinality (or size) of the union of all sets `f i` (for all `i` in `ι`) is less than or equal to the product of the cardinality of `ι` and the supremum of the cardinalities of all the sets `f i`. In simpler words, it's saying that the total number of unique elements in all the sets can't be more than the number of sets times the size of the biggest set. More concisely: For any function from a type `ι` to sets of type `α`, the cardinality of the union of all images is less than or equal to the cardinality of `ι` times the supremum of the cardinalities of the images.
`Cardinal.infinite_iff` theorem Cardinal.infinite_iff : ∀ {α : Type u}, Infinite α ↔ Cardinal.aleph0 ≤ Cardinal.mk α The theorem `Cardinal.infinite_iff` states that for any type `α`, `α` is infinite if and only if the cardinality of `α` is greater than or equal to `ℵ₀`, the smallest infinite cardinal number. The cardinality of `α` is denoted as `Cardinal.mk α`, while `ℵ₀` is represented as `Cardinal.aleph0`. Essentially, this theorem provides a condition for a type to be infinite, namely, that its cardinality must be at least as large as that of the set of natural numbers. More concisely: A type `α` is infinite if and only if `Cardinal.mk α ≥ Cardinal.aleph0`.
`Cardinal.mk_range_eq_of_injective` theorem Cardinal.mk_range_eq_of_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{v, u} (Cardinal.mk α) This theorem states that for any two types `α` and `β`, and any injective function `f` from `α` to `β`, the cardinality (the measure of the "size" of the set) of the range of `f` (the set of all outputs of `f`) is equal to the cardinality of `α`. This equality is maintained even when the cardinalities are lifted to higher universes. The lifting operation is used here to ensure that the cardinalities are comparable, as they might be from different universes. More concisely: For any injective functions $f : \alpha \rightarrow \beta$ between types, the cardinality of $\alpha$ and the cardinality of the range of $f$ are equal. (This equality holds even when the cardinalities are lifted to higher universes.)
`Cardinal.mk_congr` theorem Cardinal.mk_congr : ∀ {α β : Type u}, α ≃ β → Cardinal.mk α = Cardinal.mk β This theorem, named `Cardinal.mk_congr`, states that for any two types `α` and `β` in the same universe `u`, if there exists a bijective mapping (an equivalence) between `α` and `β`, then the cardinality of `α` is equal to the cardinality of `β`. In mathematical terms, given any two sets `α` and `β` such that there exists a bijection between them, their cardinal numbers are equal. More concisely: If there exists a bijection between sets `α` and `β`, then `α` and `β` have equal cardinality.
`Cardinal.nat_succ` theorem Cardinal.nat_succ : ∀ (n : ℕ), ↑n.succ = Order.succ ↑n The theorem `Cardinal.nat_succ` asserts that for every natural number 'n', the cardinality of the successor of 'n' is equal to the successor of the cardinality of 'n'. In other words, it states that the operation of finding the successor (the next number) in the natural numbers is compatible with the operation of finding the successor in the order structure. More concisely: For every natural number n, the cardinality of the set of natural numbers up to n's successor is the successor of the cardinality of the set of natural numbers up to n.
`Cardinal.mk_coe_finset` theorem Cardinal.mk_coe_finset : ∀ {α : Type u} {s : Finset α}, Cardinal.mk { x // x ∈ s } = ↑s.card This theorem states that for any type `α` and any finite set `s` of that type, the cardinality of the set of elements `x` such that `x` belongs to `s` (denoted as `{ x // x ∈ s }`), is equal to the cardinality of `s` (denoted as `s.card`). In other words, the cardinality of a subset of a finite set `s` where each element is in `s`, is the same as the cardinality of `s` itself. More concisely: For any finite type `α` and set `s` of type `α`, the cardinality of the subset `{ x // x ∈ s }` equals the cardinality of `s`.
`Cardinal.IsLimit.aleph0_le` theorem Cardinal.IsLimit.aleph0_le : ∀ {c : Cardinal.{u_1}}, c.IsLimit → Cardinal.aleph0 ≤ c The theorem `Cardinal.IsLimit.aleph0_le` states that for any cardinal number `c`, if `c` is a limit cardinal (i.e., it is not zero and not a successor cardinal), then `ℵ₀` (aleph null), which is the smallest infinite cardinal, is less than or equal to `c`. In other words, every limit cardinal is at least as large as the smallest infinite cardinal. More concisely: For any limit cardinal `c`, we have `ℵ₀ ≤ c`.
`Cardinal.mk_ne_zero` theorem Cardinal.mk_ne_zero : ∀ (α : Type u) [inst : Nonempty α], Cardinal.mk α ≠ 0 The theorem `Cardinal.mk_ne_zero` states that for any given type `α`, if `α` is nonempty (i.e., there exists at least one element in `α`), then the cardinality of `α` is not zero. In other words, it affirms that any nonempty type has a cardinality that is not zero. More concisely: If a type `α` is nonempty, then its cardinality is nonzero.
`Cardinal.power_def` theorem Cardinal.power_def : ∀ (α β : Type u), Cardinal.mk α ^ Cardinal.mk β = Cardinal.mk (β → α) This theorem, `Cardinal.power_def`, states that for any two types `α` and `β`, the cardinality of `α` raised to the power of the cardinality of `β` is equal to the cardinality of the type of functions from `β` to `α`. In mathematical notation, this can be written as \|α\|^\|β\| = \|β → α\|. This corresponds to the standard set-theoretic definition of exponentiation in cardinal numbers, i.e., the size of the set of all functions from a set of size `β` to a set of size `α`. More concisely: The cardinality of a type raised to the power of another cardinality is equal to the cardinality of the type of functions from that cardinality to the first type. \|α\|^\|β\| = \|β → α\|.
`Cardinal.nsmul_lt_aleph0_iff` theorem Cardinal.nsmul_lt_aleph0_iff : ∀ {n : ℕ} {a : Cardinal.{u_1}}, n • a < Cardinal.aleph0 ↔ n = 0 ∨ a < Cardinal.aleph0 The theorem `Cardinal.nsmul_lt_aleph0_iff` states that for any natural number `n` and any cardinal `a`, the inequality `n • a < Cardinal.aleph0` holds if and only if `n` is zero or `a` is less than `Cardinal.aleph0`. Here, `Cardinal.aleph0` represents the smallest infinite cardinal, `n • a` is the n-folded sum of `a`, and the symbol `<` represents the notion of less than in the context of cardinal numbers. This theorem is particularly useful when dealing with cardinal arithmetic and comparing different cardinalities. For a special case where `n ≠ 0`, refer to `Cardinal.nsmul_lt_aleph0_iff_of_ne_zero`. More concisely: For any natural number $n$ and cardinal $a$, $n \cdot a < \aleph\_0$ if and only if $n = 0$ or $a < \aleph\_0$.
`Set.Finite.lt_aleph0` theorem Set.Finite.lt_aleph0 : ∀ {α : Type u} {S : Set α}, S.Finite → Cardinal.mk ↑S < Cardinal.aleph0 This theorem, referred to as `Set.Finite.lt_aleph0`, states that for any type `α` and any set `S` of this type, if `S` is finite then the cardinality of `S` is strictly less than `ℵ₀` (aleph-zero), which is the smallest infinite cardinal number. Essentially, this theorem is asserting that the cardinal number of any finite set is less than the cardinal number of countably infinite sets, such as the set of natural numbers. More concisely: For any type `α` and finite set `S` of that type, the cardinality of `S` is strictly less than that of the set of natural numbers.
`Cardinal.succ_zero` theorem Cardinal.succ_zero : Order.succ 0 = 1 This theorem states that the successor of zero is one in the context of an ordered set. In more detail, it specifies that when the "Order.succ" function, which gives the next element in an ordered set, is applied to the element zero, the output is the element one. This is analogous to the familiar concept in the natural numbers where the successor of 0 is 1. More concisely: In an ordered set, Order.succ(0) = 1.
`Cardinal.mk_set_le` theorem Cardinal.mk_set_le : ∀ {α : Type u} (s : Set α), Cardinal.mk ↑s ≤ Cardinal.mk α This theorem states that for any type `α` and any set `s` of elements from `α`, the cardinality of the set `s` is less than or equal to the cardinality of the type `α`. In other words, this theorem states that the size of any subset is always less than or equal to the size of the whole set. More concisely: For any type `α` and subset `s` of `α`, the cardinality of `s` is less than or equal to the cardinality of `α`.
`Set.Countable.le_aleph0` theorem Set.Countable.le_aleph0 : ∀ {α : Type u} {s : Set α}, s.Countable → Cardinal.mk ↑s ≤ Cardinal.aleph0 This theorem, known as `Set.Countable.le_aleph0`, states that for any type `α` and any set `s` of type `α`, if the set `s` is countable, then the cardinality of the set `s` is less than or equal to `ℵ0` (aleph null). In other words, this theorem shows that the cardinal number of any countable set does not exceed the smallest infinite cardinal number, `ℵ0`. The cardinality of a set is a measure of the "number of elements" in the set. More concisely: If a set is countable, then its cardinality is less than or equal to the first infinite cardinal number, `ℵ0`.
`Cardinal.card_le_of` theorem Cardinal.card_le_of : ∀ {α : Type u} {n : ℕ}, (∀ (s : Finset α), s.card ≤ n) → Cardinal.mk α ≤ ↑n The theorem `Cardinal.card_le_of` states that for any type `α` and any natural number `n`, if every finite set `s` of type `α` has a cardinality that is less than or equal to `n`, then the cardinal number of the type `α` is less than or equal to the cardinality of `n`. In other words, if all finite sets from a certain type do not exceed a certain size, then the cardinality of the entire type does not exceed that size. More concisely: If every finite subset of type `α` has cardinality less than or equal to `n`, then the cardinality of `α` is less than or equal to `n`.
`Cardinal.mk_le_of_surjective` theorem Cardinal.mk_le_of_surjective : ∀ {α β : Type u} {f : α → β}, Function.Surjective f → Cardinal.mk β ≤ Cardinal.mk α The theorem `Cardinal.mk_le_of_surjective` states that for any two types `α` and `β` and a function `f` from `α` to `β`, if `f` is surjective (meaning that for every element of `β`, there exists an element of `α` such that `f` maps this `α` element to the `β` element), then the cardinality of `β` is less than or equal to the cardinality of `α`. This theorem encapsulates the intuitive idea that a surjective function cannot map a type with fewer elements to a type with more elements. More concisely: If `f` is a surjective function from a set `α` to a set `β`, then `\|α\| ≥ \|β\|`. (The symbol `\|.\|` represents the cardinality of a set.)
`Cardinal.lift_umax` theorem Cardinal.lift_umax : Cardinal.lift.{max u v, u} = Cardinal.lift.{v, u} This theorem states that for any two universes `u` and `v`, the operation of "lifting" a cardinal from universe `v` to `u` (denoted by `Cardinal.lift.{v, u}`) is equivalent to the operation of "lifting" a cardinal from the universe `max(u, v)` to `u` (denoted by `Cardinal.lift.{max u v, u}`). In other words, for any cardinal, whether we first lift it to a larger universe and then to `u`, or directly lift it to `u`, the result will be the same. More concisely: For any cardinals $c$ and universes $u$ and $v$, the lifting of $c$ from universe $v$ to $u$ is equal to the lifting of $c$ from the maximum of $u$ and $v$ to $u$ in Lean 4. (i.e., `Cardinal.lift.{v, u} c = Cardinal.lift.{max u v, u} c`).
`Cardinal.lift_id'` theorem Cardinal.lift_id' : ∀ (a : Cardinal.{max u v}), Cardinal.lift.{u, max u v} a = a This theorem, `Cardinal.lift_id'`, states that for any cardinal number `a` defined in the maximum of universe `u` and `v`, if we perform a universe lift operation on `a` to a universe which is lower than or equal to its original universe (`max u v`), the lifted cardinal number remains the same as `a`. In mathematical terms, this means that lifting a cardinal to a universe no greater than its current one will not change the cardinality. More concisely: For any cardinal number `a` and universes `u` and `v` with `u` being an upper bound of their maximum, the cardinality lifted from `u` to a universe `w` with `w <= u` remains equal to `a`.
`Set.Subsingleton.cardinal_mk_le_one` theorem Set.Subsingleton.cardinal_mk_le_one : ∀ {α : Type u} {s : Set α}, s.Subsingleton → Cardinal.mk ↑s ≤ 1 := by sorry This theorem, named `Set.Subsingleton.cardinal_mk_le_one`, establishes a relationship between the concept of a subsingleton and the cardinality of a set in the context of type theory. Specifically, it states that for any type `α` and any set `s` of that type, if `s` is a subsingleton (that is, it contains at most one element), then the cardinality of the type of the set `s` (as denoted by `Cardinal.mk ↑s`) is less than or equal to one. In simpler terms, if a set contains at most one member, its size (or cardinality) is 1 or less. More concisely: If a set is a subsingleton, then its cardinality is at most 1.
`Cardinal.mk_out` theorem Cardinal.mk_out : ∀ (c : Cardinal.{u_1}), Cardinal.mk (Quotient.out c) = c The theorem `Cardinal.mk_out` asserts that for every cardinal number `c`, when we choose an element from the equivalence class of `c` using the noncomputable function `Quotient.out`, and then compute the cardinality of the resulting set, we get back the original cardinal number `c`. In other words, choosing an element from the equivalence class of a cardinal number does not change its cardinality. This theorem is a statement about the consistency of cardinal numbers under the operation of choosing an element from their equivalence classes. More concisely: For every cardinal number `c`, the cardinality of the set obtained by choosing an element from the equivalence class of `c` using `Quotient.out` function is equal to `c`.
`Cardinal.lt_aleph0_iff_set_finite` theorem Cardinal.lt_aleph0_iff_set_finite : ∀ {α : Type u} {S : Set α}, Cardinal.mk ↑S < Cardinal.aleph0 ↔ S.Finite This theorem is stating a relationship between the cardinality of a set and the notion of finiteness. More specifically, for any type `α` and a set `S` of this type, the cardinality of set `S` is strictly less than the smallest infinite cardinal (`ℵ₀` or `aleph0`) if and only if the set `S` is finite. In other words, it provides a condition to determine whether a set is finite: a set is finite if and only if its cardinality is less than the smallest infinite cardinal. More concisely: A set is finite if and only if its cardinality is strictly less than the smallest infinite cardinal.
`Cardinal.nat_lt_aleph0` theorem Cardinal.nat_lt_aleph0 : ∀ (n : ℕ), ↑n < Cardinal.aleph0 The theorem `Cardinal.nat_lt_aleph0` states that for every natural number `n`, the cardinality of `n` is less than `ℵ₀` (aleph null), which is the smallest infinite cardinal. In other words, the size of any finite set of natural numbers is always smaller than the size of the set of all natural numbers. More concisely: The theorem `Cardinal.nat_lt_aleph0` asserts that for all natural numbers `n`, the cardinality of `Finset.nat n` is strictly less than the cardinality of `Nat`.
`Cardinal.mk_le_aleph0_iff` theorem Cardinal.mk_le_aleph0_iff : ∀ {α : Type u}, Cardinal.mk α ≤ Cardinal.aleph0 ↔ Countable α This theorem states that for any type `α`, the cardinality of `α` is less than or equal to the smallest infinite cardinal (`ℵ₀`) if and only if `α` is countable. In mathematical terms, it establishes a relationship between the cardinality of a set (or type in Lean's context) and its countability, specifying that a type has cardinality at most `ℵ₀` precisely when it is countable, i.e., there exists an injective function from the type to the natural numbers. More concisely: A type `α` has cardinality at most that of the first infinite ordinal (`ℵ₀`) if and only if `α` is countable, i.e., there exists an injective function from `α` to the natural numbers.
`Cardinal.le_powerlt` theorem Cardinal.le_powerlt : ∀ {b c : Cardinal.{u}} (a : Cardinal.{u}), c < b → a ^ c ≤ a.powerlt b The theorem `Cardinal.le_powerlt` states that for any three cardinal numbers `a`, `b`, and `c` in a specific type `u`, if `c` is less than `b`, then `a` raised to the power of `c` is less than or equal to `a` raised to the cardinal exponent of `b`. This theorem essentially deals with the properties of exponents in the context of cardinal numbers. More concisely: For any cardinal numbers `a`, `b`, and `c`, if `c` is less than `b`, then `a^c <= a^b`.
`Cardinal.lift_zero` theorem Cardinal.lift_zero : Cardinal.lift.{u_2, u_1} 0 = 0 This theorem states that the cardinality of the empty set remains zero even after the universe lift operation. In other words, when the universe lift operation, denoted by `Cardinal.lift`, is applied to the cardinal number `0` (which represents the cardinality of the empty set), the resulting cardinal number in a potentially higher universe is still `0`. More concisely: The cardinality of the empty set is zero in all universes.
`Cardinal.mk_uLift` theorem Cardinal.mk_uLift : ∀ (α : Type u), Cardinal.mk (ULift.{v, u} α) = Cardinal.lift.{v, u} (Cardinal.mk α) := by sorry The theorem `Cardinal.mk_uLift` states that for any type `α` in universe `u`, the cardinality of the lifted type `ULift.{v, u} α` is equal to the lifted cardinality `Cardinal.lift.{v, u} (Cardinal.mk α)`. In other words, taking a type and lifting it to a higher universe, then computing its cardinality is the same as computing the cardinality in the original universe and then lifting the cardinality to the higher universe. Here, cardinality refers to the size of a set or type, and universe refers to a hierarchical level in Lean's type theory where types and sets can exist. More concisely: The cardinality of `ULift.{v, u} α` is equal to the lifted cardinality `Cardinal.lift.{v, u} (Cardinal.mk α)` for any type `α` in universe `u`.
`Cardinal.sum_const` theorem Cardinal.sum_const : ∀ (ι : Type u) (a : Cardinal.{v}), (Cardinal.sum fun x => a) = Cardinal.lift.{v, u} (Cardinal.mk ι) * Cardinal.lift.{u, v} a The theorem `Cardinal.sum_const` states that for any type `ι` and any cardinal number `a`, the sum of constant `a` across all elements of type `ι` is equal to the product of the cardinality of type `ι` and `a` after both have been lifted to the correct universe. This corresponds to the mathematical notion that the cardinality of a product set is the product of the cardinalities of the individual sets. More concisely: For any cardinal number `a` and type `ι`, the sum of `a` in `ι` is equal to the product of the cardinality of `ι` and `a`.
`Cardinal.power_zero` theorem Cardinal.power_zero : ∀ {a : Cardinal.{u_1}}, a ^ 0 = 1 This theorem, denoted as `Cardinal.power_zero`, states that for any cardinal number `a`, raising `a` to the power of `0` results in `1`. In mathematical terms, for any cardinal number $a$, $a^0 = 1$. Equivalently, it asserts that the zeroth power of any cardinal number is always equal to the cardinal number `1`. More concisely: For any cardinal number `a`, `a^0 = 1`.
`Cardinal.natCast_le` theorem Cardinal.natCast_le : ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n This theorem states that for any two natural numbers `m` and `n`, the inequality `m ≤ n` holds if and only if the same inequality `↑m ≤ ↑n` holds when both numbers are cast to cardinals, where `↑m` and `↑n` represent the cardinal numbers corresponding to `m` and `n` respectively. In other words, the natural order of the numbers is preserved upon cardinality casting. More concisely: For all natural numbers m and n, m <= n if and only if the cardinal numbers of m and n satisfy the inequality ↑m <= ↑n.
`Cardinal.mk_iUnion_le_sum_mk` theorem Cardinal.mk_iUnion_le_sum_mk : ∀ {α ι : Type u} {f : ι → Set α}, Cardinal.mk ↑(⋃ i, f i) ≤ Cardinal.sum fun i => Cardinal.mk ↑(f i) This theorem states that for any types `α` and `ι`, and any function `f` mapping from `ι` to a set of `α`, the cardinality (size) of the union of all sets `f i` (for all `i` in `ι`) is less than or equal to the total sum of the cardinalities of each individual set `f i`. In mathematical terms, it is saying that the cardinality of the union of sets is always less than or equal to the sum of the cardinalities of the individual sets. This is analogous to the principle that the total size of a union of sets is less than or equal to the sum of the sizes of those sets, because there may be overlapping elements. More concisely: For any function from a set to a type, the cardinality of its image (the sets' union) is less than or equal to the sum of the cardinalities of the sets in the domain.
`Cardinal.aleph0_le_mul_iff` theorem Cardinal.aleph0_le_mul_iff : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (Cardinal.aleph0 ≤ a ∨ Cardinal.aleph0 ≤ b) The theorem `Cardinal.aleph0_le_mul_iff` says that for any two cardinals `a` and `b`, the smallest infinite cardinal `ℵ₀` (aleph null) is less than or equal to the product of `a` and `b` if and only if both `a` and `b` are not zero and at least one of `a` or `b` is greater than or equal to `ℵ₀`. This theorem connects the concepts of cardinal multiplication with the notion of cardinality of infinite sets. More concisely: The smallest infinite cardinal `ℵ₀` is less than or equal to the product of cardinals `a` and `b` if and only if `a` and `b` are both non-zero and at least one is greater than or equal to `ℵ₀`.
`Cardinal.mk_pi` theorem Cardinal.mk_pi : ∀ {ι : Type u} (α : ι → Type v), Cardinal.mk ((i : ι) → α i) = Cardinal.prod fun i => Cardinal.mk (α i) This theorem, `Cardinal.mk_pi`, states that for any type `ι` and a function `α : ι → Type v`, the cardinality of the dependent product type `(i : ι) → α i` is equal to the indexed product of the cardinalities of the types `α i`. In other words, the cardinality of a dependent product type is the product of the cardinalities of each of the types involved, where the types are indexed by elements of type `ι`. More concisely: The cardinality of a dependent product type `(i : ι) → α i` is equal to the product of the cardinalities of the types `α i` indexed by `ι`.
`Cardinal.mk_univ` theorem Cardinal.mk_univ : ∀ {α : Type u}, Cardinal.mk ↑Set.univ = Cardinal.mk α This theorem states that for any type `α`, the cardinal number (or size) of the universal set of `α` is equal to the cardinal number of the type `α` itself. In other words, it asserts that there is a one-to-one correspondence (or a bijection) between the set of all elements of type `α` and the universal set on `α`. This means that the number of elements in the universal set on a type is equal to the number of elements of that type. More concisely: For any type `α`, the cardinality of `α` equals the cardinality of its universe.
`Cardinal.bddAbove_image` theorem Cardinal.bddAbove_image : ∀ (f : Cardinal.{u} → Cardinal.{max u v}) {s : Set Cardinal.{u}}, BddAbove s → BddAbove (f '' s) This theorem states that for any function `f` which maps a cardinal number of type `u` to a cardinal number of the maximum type of `u` and `v`, and any set `s` of cardinal numbers of type `u`, if the set `s` is bounded above (i.e., there exists an upper bound for the cardinal numbers in `s`), then the image of the set `s` under the function `f` (i.e., the set of all cardinal numbers obtained by applying `f` to every element of `s`) is also bounded above. This means that an upper bound also exists for all cardinal numbers that can be obtained from `s` by applying `f`. More concisely: If `f` is a function mapping cardinal numbers of type `u` to the maximum of `u` and `v`, and `s` is a bounded set of cardinal numbers of type `u`, then the image of `s` under `f` is also a bounded set.
`Cardinal.lift_iSup_le` theorem Cardinal.lift_iSup_le : ∀ {ι : Type v} {f : ι → Cardinal.{w}} {t : Cardinal.{max u w}}, BddAbove (Set.range f) → (∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t) → Cardinal.lift.{u, w} (iSup f) ≤ t This theorem states that for a given type `ι`, a function `f` from `ι` to a cardinal number, and a cardinal `t`, if the set of cardinal numbers produced by `f` is bounded above and each cardinal number produced by `f` after being lifted to the universe `u` is less than or equal to `t`, then the lift to the universe `u` of the supremum of the cardinal numbers produced by `f` is also less than or equal to `t`. In other words, it states that the lift of the supremum of a set of cardinal numbers is bounded above by a certain cardinal if the lift of each individual cardinal number in the set is also bounded above by that cardinal. More concisely: If `f : ι -> Card`, `t : Card`, and the set `{cf (lift ι x) \| x ∈ image f}` is bounded above, then `lift ι (sup (image f)) ≤ t`.
`Cardinal.lift_lt_aleph0` theorem Cardinal.lift_lt_aleph0 : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c < Cardinal.aleph0 ↔ c < Cardinal.aleph0 The theorem `Cardinal.lift_lt_aleph0` states that for all cardinals `c` in universe `u`, the lift operation on `c` to universe `v` (`Cardinal.lift.{v, u} c`) is less than the smallest infinite cardinal (`Cardinal.aleph0`) if and only if `c` itself is less than `Cardinal.aleph0`. This means that the relationship of being less than `ℵ₀` is preserved under the universe lift operation on cardinals. More concisely: For all cardinals `c` in universe `u`, `Cardinal.lift.{v, u} c < Cardinal.aleph0` if and only if `c < Cardinal.aleph0`.
`Cardinal.mk_eq_zero` theorem Cardinal.mk_eq_zero : ∀ (α : Type u) [inst : IsEmpty α], Cardinal.mk α = 0 The theorem `Cardinal.mk_eq_zero` states that for any type `α`, if `α` is an empty type (i.e., it has no elements), then the cardinality of `α` is zero. In other words, the number of elements in an empty type is zero. More concisely: If a type has no elements, then its cardinality is zero.
`Cardinal.one_lt_iff_nontrivial` theorem Cardinal.one_lt_iff_nontrivial : ∀ {α : Type u}, 1 < Cardinal.mk α ↔ Nontrivial α This theorem states that for any type `α`, the cardinality of `α` is greater than 1 if and only if `α` is nontrivial. Here, a nontrivial type is one that has at least two distinct elements. In the context of cardinality, this means that there are at least two distinguishable "sizes" or "amounts" within the type. This is expressed mathematically as $1 < \|α\|$ if and only if `α` is nontrivial. More concisely: For any type `α`, the cardinality `\|α\|` is greater than 1 if and only if `α` has at least two distinct elements.
`Cardinal.lift_mk_fin` theorem Cardinal.lift_mk_fin : ∀ (n : ℕ), Cardinal.lift.{u_1, 0} (Cardinal.mk (Fin n)) = ↑n This theorem states that for any natural number `n`, lifting the cardinality of the finite type `Fin n` from universe 0 to any universe `u_1` is equal to `n`. Here, `Fin n` is a type that represents numbers less than `n`, so its cardinality is `n`. The "universe lift operation" on cardinals, denoted by `Cardinal.lift`, allows us to lift a cardinal from a certain universe to a higher one, and `Cardinal.mk` is a function that gives us the cardinal number of a type. The theorem therefore confirms that lifting the cardinality doesn't change the size of the set, even when we change the universe of the set. More concisely: The cardinality of the finite type `Fin n` is equal to `Cardinal.lift (Cardinal.mk n)`, where `Cardinal.lift` lifts the cardinality from universe 0 to any universe `u_1`.
`Cardinal.lift_mk_le` theorem Cardinal.lift_mk_le : ∀ {α : Type v} {β : Type w}, Cardinal.lift.{max u w, v} (Cardinal.mk α) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk β) ↔ Nonempty (α ↪ β) The theorem `Cardinal.lift_mk_le` states that for all types `α` and `β`, the lifted cardinality of `α` is less than or equal to the lifted cardinality of `β` if and only if there exists an injective function from `α` to `β`. Here, "lifted cardinality" refers to the cardinal number of a type after applying the universe lift operation, which lifts the universe level of the cardinal. The cardinality of a type is defined as the size of the set of all elements of that type. More concisely: For types α and β, the lifted cardinalities are equal if and only if there exists an injective function from α to β. (Note that this is equivalent to the original statement but phrased in terms of cardinalities rather than lifted cardinalities.)
`Cardinal.mk_prod` theorem Cardinal.mk_prod : ∀ (α : Type u) (β : Type v), Cardinal.mk (α × β) = Cardinal.lift.{v, u} (Cardinal.mk α) * Cardinal.lift.{u, v} (Cardinal.mk β) This theorem, `Cardinal.mk_prod`, states that for any two types `α` and `β`, the cardinality of the product type `(α × β)` is equal to the product of the cardinalities of `α` and `β` after applying the universe lift operation. In mathematical terms, if `\|α\|` and `\|β\|` represent the cardinalities of types `α` and `β` respectively, then the cardinality of the product type `(α × β)` is equal to `\|α\| * \|β\|`, where the multiplication is performed after lifting the cardinalities to appropriate universe levels. More concisely: The cardinality of a product type equals the product of the cardinalities after lifting to appropriate universes.
`Cardinal.lift_aleph0` theorem Cardinal.lift_aleph0 : Cardinal.lift.{u_1, u_2} Cardinal.aleph0 = Cardinal.aleph0 The theorem `Cardinal.lift_aleph0` states that the lift operation on the smallest infinite cardinal, often denoted as `ℵ₀` (or `aleph0` in Lean), is equal to `ℵ₀` itself. This means if we take the smallest infinite cardinal and lift it to a different universe (in the context of type theory), the cardinality remains the same. In other words, the cardinality of the set of natural numbers is the same in any universe. More concisely: The theorem `Cardinal.lift_aleph0` asserts that the lift of the smallest infinite cardinal `ℵ₀` to any universe is equal to `ℵ₀`.
`Cardinal.lift_injective` theorem Cardinal.lift_injective : Function.Injective Cardinal.lift.{u, v} The theorem `Cardinal.lift_injective` asserts that the `lift` operation on cardinals is injective. In other words, if we have two cardinals `a` and `b` such that their lifts (with the same pair of universes `u` and `v`) are equal (i.e., `Cardinal.lift.{u, v} a = Cardinal.lift.{u, v} b`), then the original cardinals `a` and `b` themselves are equal. This property essentially guarantees that the process of lifting a cardinal to a higher universe doesn't conflate distinct cardinals. More concisely: If two cardinals have equal lifts in the same universes, then the original cardinals are equal.
`Cardinal.power_lt_aleph0` theorem Cardinal.power_lt_aleph0 : ∀ {a b : Cardinal.{u_1}}, a < Cardinal.aleph0 → b < Cardinal.aleph0 → a ^ b < Cardinal.aleph0 The theorem `Cardinal.power_lt_aleph0` states that for any two cardinal numbers `a` and `b`, if both `a` and `b` are less than `ℵ₀` (the smallest infinite cardinal), then `a` to the power `b` is also less than `ℵ₀`. In other words, raising one cardinal number that is less than `ℵ₀` to the power of another cardinal number that is also less than `ℵ₀` results in a cardinal number that is still less than `ℵ₀`. More concisely: For any cardinal numbers `a` and `b` less than `ℵ₀`, `a^b` is also less than `ℵ₀`.
`Cardinal.mk_eq_aleph0` theorem Cardinal.mk_eq_aleph0 : ∀ (α : Type u_1) [inst : Countable α] [inst : Infinite α], Cardinal.mk α = Cardinal.aleph0 The theorem `Cardinal.mk_eq_aleph0` asserts that for any type `α` that is both countable and infinite, the cardinal number of `α` is equal to `ℵ₀`, the smallest infinite cardinal (which is the cardinality of the set of natural numbers). In other words, any infinite set that can be put into a one-to-one correspondence with the natural numbers has the same cardinality as the set of natural numbers, denoted as `ℵ₀` (aleph-null). More concisely: For any countable and infinite type `α`, its cardinality equals that of the natural numbers, denoted as `ℵ₀`.
`Cardinal.lift_add` theorem Cardinal.lift_add : ∀ (a b : Cardinal.{u}), Cardinal.lift.{v, u} (a + b) = Cardinal.lift.{v, u} a + Cardinal.lift.{v, u} b The theorem `Cardinal.lift_add` states that for all cardinal numbers `a` and `b` in a particular universe `u`, the operation of lifting the sum of `a` and `b` to a larger universe `v` (via `Cardinal.lift`) is equivalent to separately lifting `a` and `b` to universe `v` and then adding them. In mathematical terms, this property can be represented as `lift(a + b) = lift(a) + lift(b)`. This theorem essentially shows the compatibility of the lift operation with the addition operation on cardinal numbers. More concisely: For all cardinal numbers `a` and `b`, the operation of lifting their sum to a larger universe is equal to the sum of their individual lifts: `Cardinal.lift (a + b) = Cardinal.lift a + Cardinal.lift b`.
`Cardinal.lift_le_aleph0` theorem Cardinal.lift_le_aleph0 : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c ≤ Cardinal.aleph0 ↔ c ≤ Cardinal.aleph0 The theorem `Cardinal.lift_le_aleph0` asserts that for each cardinal number `c` in universe `u`, the universe-lifted version of `c` (from universe `v` to universe `u`) is less than or equal to the smallest infinite cardinal (`ℵ₀`) if and only if `c` itself is less than or equal to `ℵ₀`. In other words, the process of lifting a cardinal to a different universe preserves the property of being less than or equal to `ℵ₀`. More concisely: For all cardinal numbers `c` in a universe, `c ≤ ℵ₀` if and only if the lifted version of `c` in a higher universe is also less than or equal to `ℵ₀`.
`Cardinal.lift_uzero` theorem Cardinal.lift_uzero : ∀ (a : Cardinal.{u}), Cardinal.lift.{0, u} a = a This theorem states that for any cardinal number `a` in any universe `u`, lifting `a` to the zero universe results in `a` itself. In other words, the operation of lifting a cardinal to the zero universe is an identity operation. It doesn't change the cardinal number. This is formally represented in Lean 4 as `Cardinal.lift.{0, u} a = a` for any `a : Cardinal.{u}`. More concisely: For any cardinal number `a` in any universe, the operation of lifting `a` to the zero universe results in `a` itself. In Lean 4 notation: `Cardinal.lift.{0, u} a = a` for any `a : Cardinal.{u}` .
`Cardinal.add_lt_aleph0` theorem Cardinal.add_lt_aleph0 : ∀ {a b : Cardinal.{u_1}}, a < Cardinal.aleph0 → b < Cardinal.aleph0 → a + b < Cardinal.aleph0 The theorem `Cardinal.add_lt_aleph0` states that for any two cardinal numbers `a` and `b` belonging to `Type u_1`, if both `a` and `b` are less than the smallest infinite cardinal (`ℵ₀`), then the sum of `a` and `b` is also less than `ℵ₀`. In other words, the sum of two cardinal numbers that are less than infinity (in this case represented by `ℵ₀`) remains less than infinity. More concisely: For any cardinal numbers `a` and `b`, if `a < ℵ₀` and `b < ℵ₀`, then `a + b < ℵ₀`.
`Cardinal.exists_eq_of_iSup_eq_of_not_isLimit` theorem Cardinal.exists_eq_of_iSup_eq_of_not_isLimit : ∀ {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}), BddAbove (Set.range f) → ∀ (ω : Cardinal.{v}), ¬ω.IsLimit → ⨆ i, f i = ω → ∃ i, f i = ω The theorem `Cardinal.exists_eq_of_iSup_eq_of_not_isLimit` states that for any type `ι` which is nonempty and a function `f` from `ι` to a cardinal number, if the range of `f` is bounded above and `ω` is a cardinal number that is not a limit cardinal, then if the supremum of `f` over `ι` is equal to `ω`, there exists an element in `ι` such that applying `f` to this element yields `ω`. Essentially, it means if a cardinal number is the least upper bound of a set of cardinals and it's not a limit cardinal, then this cardinal is in the image of the function defining the set. More concisely: If `ι` is a nonempty type, `f: ι → cardinal` has a bounded range, and `ω` is a non-limit cardinal, then `sup (range f) = ω` implies the existence of `x ∈ ι` such that `f x = ω`.
`Cardinal.mk_ne_zero_iff` theorem Cardinal.mk_ne_zero_iff : ∀ {α : Type u}, Cardinal.mk α ≠ 0 ↔ Nonempty α The theorem `Cardinal.mk_ne_zero_iff` establishes a bi-conditional relationship between a type `α` having a non-zero cardinality and the type `α` being nonempty. In other words, it states that for any type `α`, the cardinality of `α` is not zero if and only if `α` is nonempty. This theorem is a key aspect of cardinality theory in set theory, determining the link between cardinality and the existence of elements in a particular type. More concisely: A type has a non-zero cardinality if and only if it is nonempty.
`Cardinal.lift_power` theorem Cardinal.lift_power : ∀ (a b : Cardinal.{u}), Cardinal.lift.{v, u} (a ^ b) = Cardinal.lift.{v, u} a ^ Cardinal.lift.{v, u} b The theorem `Cardinal.lift_power` states that for any two cardinal numbers `a` and `b` in a certain universe `u`, the lift operation of the cardinal number resulting from raising `a` to the power `b` to a higher universe `v` is equivalent to first individually lifting `a` and `b` to the higher universe `v` and then raising the lifted `a` to the power of the lifted `b`. In mathematical terms, this theorem asserts the equality `Cardinal.lift (a ^ b) = (Cardinal.lift a) ^ (Cardinal.lift b)` under the universe lift operation on cardinals. More concisely: The `Cardinal.lift_power` theorem in Lean 4 asserts that lifting a cardinal number `a` to the power `b` in a higher universe `v` is equivalent to first lifting `a` and `b` individually to `v` and then raising the lifted `a` to the power of the lifted `b`, i.e., `Cardinal.lift (a ^ b) = (Cardinal.lift a) ^ (Cardinal.lift b)`.
`Cardinal.lift_lift` theorem Cardinal.lift_lift : ∀ (a : Cardinal.{u_1}), Cardinal.lift.{w, max v u_1} (Cardinal.lift.{v, u_1} a) = Cardinal.lift.{max v w, u_1} a The theorem `Cardinal.lift_lift` states that for every cardinal number `a` in the universe `u_1`, lifting `a` first to the universe `max v u_1` and then to the universe `max w (max v u_1)` is the same as lifting `a` directly to the universe `max v w u_1`. This means that the process of lifting cardinal numbers to higher universes is associative, i.e., the order in which we perform the lifting operations does not affect the final result. More concisely: For any cardinal number `a` and universes `v`, `w`, the cardinal liftings `Cardinal.lift a v u_1` and `Cardinal.lift (Cardinal.lift a v) w (u_1)` are equal to `Cardinal.lift a w u_1`.
`Cardinal.lift_sSup` theorem Cardinal.lift_sSup : ∀ {s : Set Cardinal.{u_1}}, BddAbove s → Cardinal.lift.{u, u_1} (sSup s) = sSup (Cardinal.lift.{u, u_1} '' s) := by sorry The theorem `Cardinal.lift_sSup` states that for any set `s` of cardinal numbers, if `s` is bounded above, then the lift operation (which raises the universe level of a cardinal number) applied to the supremum (the least upper bound) of `s` is equivalent to the supremum of the set obtained by applying the lift operation to each element of `s`. In simpler terms, lifting the supremum of a set of cardinals gives the same result as first lifting each cardinal in the set and then taking the supremum. This demonstrates the interplay between the lift operation and the supremum operation in the context of cardinal numbers. More concisely: For any set of cardinal numbers `s` with a supremum, the lift of the supremum is equal to the supremum of the set of lifted cardinals.
`Cardinal.mk_set` theorem Cardinal.mk_set : ∀ {α : Type u}, Cardinal.mk (Set α) = 2 ^ Cardinal.mk α This theorem states that for any type `α`, the cardinality of the Set of `α` is equal to 2 raised to the power of the cardinality of `α`. In other words, the number of distinct sets that can be formed using elements of type `α` is equivalent to the total number of subsets of a set with cardinality equal to that of type `α`. This is the mathematical concept of the power set, where the cardinality of the power set of a set with cardinality `n` is `2^n`. More concisely: For any type `α`, the cardinality of its power set is 2 raised to the power of the cardinality of `α`.
`Cardinal.inductionOn₃` theorem Cardinal.inductionOn₃ : ∀ {p : Cardinal.{u_1} → Cardinal.{u_2} → Cardinal.{u_3} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}) (c₃ : Cardinal.{u_3}), (∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), p (Cardinal.mk α) (Cardinal.mk β) (Cardinal.mk γ)) → p c₁ c₂ c₃ The theorem `Cardinal.inductionOn₃` states that for all properties `p` about three cardinal numbers `c₁`, `c₂`, and `c₃`, if the property `p` is true for the cardinalities of any three types `α`, `β`, and `γ`, then the property `p` is also true for the cardinal numbers `c₁`, `c₂`, and `c₃`. In this context, a property about cardinal numbers is a logical statement that can either be true or false for given cardinal numbers. The theorem is a form of induction principle for cardinal numbers, but instead of a single cardinal number, it deals with three cardinal numbers at a time. More concisely: If a property holds for the cardinalities of any types α, β, and γ, then it holds for the cardinal numbers c₁, c₂, and c₃.
`Cardinal.lift_umax'` theorem Cardinal.lift_umax' : Cardinal.lift.{max v u, u} = Cardinal.lift.{v, u} This theorem states that the lift operation on cardinals, when applied to the maximum of two universes `v` and `u` and then `u`, is the same as when it is applied to the universes `v` and `u` directly. In other words, the order of lifting doesn't matter when we are taking the maximum of the two universes. More concisely: The lift operation on cardinals commutes with taking the maximum, i.e., `card.lift v (max u v) = max (card.lift u v) (card.lift u v)`.
`Cardinal.lift_one` theorem Cardinal.lift_one : Cardinal.lift.{u_2, u_1} 1 = 1 The theorem `Cardinal.lift_one` states that the cardinality of the singleton set, when lifted from one universe to another, remains 1. In simpler terms, it states that lifting the cardinality of a single-element set does not change its cardinality, regardless of the source and target universes involved. More concisely: The cardinality of a singleton set is preserved under set theoretic lifting between universes.
`Cardinal.le_one_iff_subsingleton` theorem Cardinal.le_one_iff_subsingleton : ∀ {α : Type u}, Cardinal.mk α ≤ 1 ↔ Subsingleton α This theorem states that for any type `α`, the cardinality of `α` is less than or equal to one if and only if `α` is a subsingleton. In other words, a type `α` has at most one element (i.e., its cardinality is less than or equal to one) if and only if every pair of elements of `α` is identical (i.e., `α` is a subsingleton). More concisely: A type `α` has at most one element if and only if it is a subsingleton (i.e., every pair of elements is identical).
`Cardinal.nat_mul_aleph0` theorem Cardinal.nat_mul_aleph0 : ∀ {n : ℕ}, n ≠ 0 → ↑n * Cardinal.aleph0 = Cardinal.aleph0 This theorem states that for any natural number `n`, as long as `n` is not equal to zero, the product of `n` and the smallest infinite cardinal number (denoted as `\aleph_0` or aleph-null) is equal to `aleph_0`. Here, `aleph_0` represents the cardinality of the set of natural numbers. This is essentially saying that multiplying any nonzero natural number with the size of an infinite set (like the set of Natural numbers) still gives an infinite set of the same size. More concisely: For any nonzero natural number `n`, the product of `n` and the cardinality of the set of natural numbers (denoted as `\aleph_0`) equals `\aleph_0`.
`Mathlib.SetTheory.Cardinal.Basic._auxLemma.23` theorem Mathlib.SetTheory.Cardinal.Basic._auxLemma.23 : ∀ {ι : Type v} {f : ι → Cardinal.{w}}, BddAbove (Set.range f) → ∀ {t : Cardinal.{max u w}}, (Cardinal.lift.{u, w} (iSup f) ≤ t) = ∀ (i : ι), Cardinal.lift.{u, w} (f i) ≤ t The theorem `Mathlib.SetTheory.Cardinal.Basic._auxLemma.23` states that for any type `ι` and a function `f` from `ι` to Cardinal numbers, if the set of all function values (i.e., the range of `f`) is bounded above, then for any Cardinal number `t`, the statement "`t` is greater than or equal to the lifted supremum of `f`" is equivalent to the statement "for all `i` in `ι`, `t` is greater than or equal to the lift of `f(i)`". Here, "lifted supremum" refers to the supremum (i.e., least upper bound) of `f`'s range, lifted from one universe to another, and "lift of `f(i)`" refers to the Cardinal number `f(i)` lifted from one universe to another. More concisely: For any type ι and function f from ι to Cardinal numbers, if the range of f is bounded above, then the lifted supremum of f is equal to the least upper bound of the lifted images of f(i) for all i in ι.
`Cardinal.lift_inj` theorem Cardinal.lift_inj : ∀ {a b : Cardinal.{u}}, Cardinal.lift.{v, u} a = Cardinal.lift.{v, u} b ↔ a = b This theorem, named `Cardinal.lift_inj`, states that for any two cardinals 'a' and 'b' in a certain universe 'u', the lifting of 'a' and 'b' to a potentially larger universe 'v' are equal if and only if 'a' and 'b' themselves are equal. In other words, the lift operation on cardinals is injective, meaning it preserves distinctness: distinct cardinals in the original universe remain distinct when lifted. More concisely: For any cardinals 'a' and 'b' in universe 'u', if the lift of 'a' to universe 'v' equals the lift of 'b' to 'v', then 'a' = 'b'.
`Cardinal.lift_mul` theorem Cardinal.lift_mul : ∀ (a b : Cardinal.{u}), Cardinal.lift.{v, u} (a * b) = Cardinal.lift.{v, u} a * Cardinal.lift.{v, u} b The theorem `Cardinal.lift_mul` states that for any two cardinal numbers `a` and `b` in a certain universe `u`, the cardinality of their product when lifted to a potentially larger universe `v`, is equal to the product of their individually lifted cardinalities. In other words, lifting the universe of the product of two cardinal numbers is the same as multiplying the lifted cardinal numbers. This theorem reflects the property of cardinal multiplication being preserved under universe lifting. More concisely: For any cardinal numbers `a` and `b` in universe `u`, the lifted product of `a` and `b` in universe `v` equals the product of their individual lifted cardinalities in `v`.
`Cardinal.mk_powerset` theorem Cardinal.mk_powerset : ∀ {α : Type u} (s : Set α), Cardinal.mk ↑s.powerset = 2 ^ Cardinal.mk ↑s This theorem, referred to as `Cardinal.mk_powerset`, states that for any given type `α` and a set `s` of this type, the cardinality (or size) of the powerset of `s` (i.e., the set of all subsets of `s`) is equal to 2 raised to the power of the cardinality of `s`. Here, `s.powerset` represents the powerset of `s`, and `Cardinal.mk` calculates the cardinality of a set or type. This theorem is essentially a formalization of the well-known mathematical fact that the size of the powerset of a set with `n` elements is `2^n`. More concisely: The cardinality of a set's powerset is equal to 2 raised to the power of the set's cardinality.
`Cardinal.lift_two_power` theorem Cardinal.lift_two_power : ∀ (a : Cardinal.{u_1}), Cardinal.lift.{v, u_1} (2 ^ a) = 2 ^ Cardinal.lift.{v, u_1} a This theorem states that for any cardinal number `a` in a given universe `u_1`, lifting the cardinality of the set `{0, 1}` raised to the power `a` to a bigger universe is equivalent to the set `{0, 1}` raised to the power of the lifted cardinality of `a`. In other words, the operation of lifting the universe of a cardinal number commutes with the operation of taking a power of 2. This asserts the consistency of cardinal arithmetic across different universe levels. More concisely: For any cardinal number `a` in a universe `u_1`, the cardinality of `{0, 1}^a` in a bigger universe is equal to the cardinality of the lifted cardinality of `{0, 1}^a` in `u_1`.
`Cardinal.iSup_of_empty` theorem Cardinal.iSup_of_empty : ∀ {ι : Sort u_1} (f : ι → Cardinal.{u_2}) [inst : IsEmpty ι], iSup f = 0 The theorem `Cardinal.iSup_of_empty` states that for any index set `ι` and any function `f` from `ι` to the set of cardinal numbers `Cardinal`, if `ι` is an empty set (as ensured by the instance `IsEmpty ι`), then the indexed supremum of `f` (denoted by `iSup f`) is equal to zero. In simpler terms, if you have a function that maps from an empty set to a set of cardinal numbers, the supremum of the values that function takes (over all elements in the index set) is zero, because there are no elements in the index set to begin with. More concisely: If `ι` is an empty index set, then `Cardinal.iSup (λ i : ι, f i) = 0` for any function `f` from `ι` to `Cardinal`.
`Cardinal.mk_sum` theorem Cardinal.mk_sum : ∀ (α : Type u) (β : Type v), Cardinal.mk (α ⊕ β) = Cardinal.lift.{v, u} (Cardinal.mk α) + Cardinal.lift.{u, v} (Cardinal.mk β) This theorem states that for any two types `α` and `β`, the cardinality of the sum type (`α ⊕ β`), which essentially represents the disjoint union of `α` and `β`, is equal to the sum of the cardinalities of `α` and `β`, each lifted to the maximum of their respective universes. In other words, if we consider the total number of distinct elements in `α` and `β` (represented by their cardinalities), then creating a new type that can be either an element of `α` or an element of `β` will have a cardinality equal to the sum of the cardinalities of `α` and `β`. This result parallels the familiar principle from set theory, where the cardinality of the union of two disjoint sets is the sum of their cardinalities. More concisely: The theorem asserts that the cardinality of the sum type `α ⊕ β` equals the sum of the lifted cardinalities of `α` and `β` in Lean 4.
`Cardinal.lift_iSup_le_lift_iSup'` theorem Cardinal.lift_iSup_le_lift_iSup' : ∀ {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{v}} {f' : ι' → Cardinal.{v'}}, BddAbove (Set.range f) → BddAbove (Set.range f') → ∀ (g : ι → ι'), (∀ (i : ι), Cardinal.lift.{v', v} (f i) ≤ Cardinal.lift.{v, v'} (f' (g i))) → Cardinal.lift.{v', v} (iSup f) ≤ Cardinal.lift.{v, v'} (iSup f') The theorem `Cardinal.lift_iSup_le_lift_iSup'` states that for any two types `ι` and `ι'` and any two functions `f : ι → Cardinal.{v}` and `f' : ι' → Cardinal.{v'}`, if the set of values of both functions are bounded above, then for any function `g : ι → ι'` such that for every `i : ι`, the cardinality obtained by lifting the function `f` evaluated at `i` is less than or equal to the cardinality obtained by lifting the function `f'` evaluated at `g(i)`, then the cardinality obtained by lifting the supremum of `f` is also less than or equal to the cardinality obtained by lifting the supremum of `f'`. In simpler terms, this theorem ensures a kind of order preservation property for the operation of taking supremum and applying the lift operation in the context of cardinalities. More concisely: Given functions `f : ι → Cardinal` and `f' : ι' → Cardinal` with bounded above domains, if for all `i : ι`, `Cardinal.lift(f i) ≤ Cardinal.lift(f' (g i))` for some function `g : ι → ι'`, then `Cardinal.lift (sup (range f)) ≤ Cardinal.lift (sup (range f'))`.
`Cardinal.lift_natCast` theorem Cardinal.lift_natCast : ∀ (n : ℕ), Cardinal.lift.{u, v} ↑n = ↑n This theorem states that for any natural number `n`, the "universe lift" operation on the cardinal number represented by `n` is equal to the cardinal number represented by `n` itself. In other words, lifting the cardinality of a set from one universe to another doesn't change the cardinality when the cardinality is a natural number. This is expressed in Lean 4 as `Cardinal.lift.{u, v} ↑n = ↑n` for all natural numbers `n`. More concisely: For all natural numbers `n`, the cardinality lift operations from universe `u` to `v` equal the identity on `n`. (`Cardinal.lift.{u, v} ↑n = ↑n`)
`Equiv.cardinal_eq` theorem Equiv.cardinal_eq : ∀ {α β : Type u}, α ≃ β → Cardinal.mk α = Cardinal.mk β This theorem, referred to as `Equiv.cardinal_eq`, states that for any two types `α` and `β` at the same universe level `u`, if `α` is equivalent to `β` (denoted by `α ≃ β`), then the cardinality of `α` (denoted by `Cardinal.mk α`) is equal to the cardinality of `β` (denoted by `Cardinal.mk β`). In other words, equivalent types have the same cardinality. This is an alias of the theorem `Cardinal.mk_congr`. More concisely: If two types `α` and `β` are equivalent, then they have the same cardinality.
`Cardinal.aleph0_le_mk` theorem Cardinal.aleph0_le_mk : ∀ (α : Type u) [inst : Infinite α], Cardinal.aleph0 ≤ Cardinal.mk α The theorem `Cardinal.aleph0_le_mk` states that for every type `α` that is infinite, the smallest infinite cardinal number, `ℵ₀` (aleph null), is less than or equal to the cardinality of the type `α`. The cardinality of a type is a measure of the "size" of the type, or the number of elements it contains. Hence, this theorem essentially states that any infinite type has a cardinality at least as large as `ℵ₀`. More concisely: For every infinite type `α`, the cardinality of `α` is greater than or equal to the smallest infinite cardinal number `ℵ₀`. (Note that the theorem in Lean actually states that `ℵ₀` is less than or equal to the cardinality of `α`, which is the negative of the statement you provided.)
`Cardinal.mk_eq_one` theorem Cardinal.mk_eq_one : ∀ (α : Type u) [inst : Unique α], Cardinal.mk α = 1 The theorem `Cardinal.mk_eq_one` states that for any type `α`, if `α` is unique, i.e., it has exactly one element, then the cardinality of `α` is 1. Here, `Cardinal.mk α` is a function that returns the cardinal number of type `α`, and `Unique α` is a typeclass assumption indicating that there is exactly one element of type `α`. In mathematical terms, this theorem is saying that the cardinality of a singleton set is 1. More concisely: If a type `α` has exactly one element, then the cardinality of `α` is 1.
`Mathlib.SetTheory.Cardinal.Basic._auxLemma.8` theorem Mathlib.SetTheory.Cardinal.Basic._auxLemma.8 : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 2 = 1 + 1 := by sorry This theorem states that for any type `α` which is an instance of the `AddMonoidWithOne` class, the number 2 is equal to the sum of 1 and 1. Here, `AddMonoidWithOne` represents a set equipped with an associative addition operation and a distinct element of the set, usually denoted as 1, that serves as a neutral element for the addition. In simpler terms, it's the mathematical way of expressing that 1 + 1 equals 2 in any additively monoidal set with a distinct 1 element. More concisely: For any type `α` instancing `AddMonoidWithOne`, 1 + 1 equals 2.
`Cardinal.mk_union_le` theorem Cardinal.mk_union_le : ∀ {α : Type u} (S T : Set α), Cardinal.mk ↑(S ∪ T) ≤ Cardinal.mk ↑S + Cardinal.mk ↑T This theorem states that for any type `α` and any two sets `S` and `T` of that type, the cardinality (number of elements) of the union of `S` and `T` is less than or equal to the sum of the cardinalities of `S` and `T`. This theorem formalizes the intuitive idea that the size of a union of two sets is at most the sum of the sizes of the two sets. More concisely: For any types `α` and sets `S` and `T` of that type, the cardinality of `S ∪ T` is less than or equal to the cardinality of `S` plus the cardinality of `T`.
`Cardinal.powerlt_le` theorem Cardinal.powerlt_le : ∀ {a b c : Cardinal.{u}}, a.powerlt b ≤ c ↔ ∀ x < b, a ^ x ≤ c The theorem `Cardinal.powerlt_le` is about cardinal numbers and their powers in set theory. It states that for any three cardinal numbers `a`, `b`, and `c`, the power of `a` to the cardinal less than `b` is less than or equal to `c` if and only if for all cardinal numbers `x` less than `b`, the power of `a` to `x` is less than or equal to `c`. In mathematical terms, it says that $a^{ More concisely: For any cardinal numbers \(a, b, c$, \(a^{
`Cardinal.mk_le_aleph0` theorem Cardinal.mk_le_aleph0 : ∀ {α : Type u} [inst : Countable α], Cardinal.mk α ≤ Cardinal.aleph0 This theorem states that for any type `α` that is countable (i.e., has the same or less number of elements as the natural numbers `ℕ`), the cardinality of `α` is less than or equal to `ℵ₀`, which is the smallest infinite cardinal number. In other words, the size of any countable set will always be less than or equal to the size of the set of natural numbers. More concisely: Any countable type `α` has cardinality less than or equal to that of the natural numbers `ℕ`, which is smaller than `ℵ₀`.
`Cardinal.power_add` theorem Cardinal.power_add : ∀ {a b c : Cardinal.{u_1}}, a ^ (b + c) = a ^ b * a ^ c This theorem, `Cardinal.power_add`, states that for any three cardinal numbers `a`, `b`, and `c`, the cardinality of the power set of `a` with `b + c` as exponent is equal to the product of the cardinality of the power set of `a` with `b` as exponent and the cardinality of the power set of `a` with `c` as exponent. This is analogous to the power of sums rule in algebra, which states for any real numbers x, y and z, (x^(y+z)) = x^y * x^z. More concisely: For any cardinal number `a`, the cardinality of the power set of `a` raised to the power of `b + c` is equal to the product of the cardinalities of the power sets of `a` raised to the powers of `b` and `c`.
`Cardinal.bddAbove_of_small` theorem Cardinal.bddAbove_of_small : ∀ (s : Set Cardinal.{u}) [h : Small.{u, u + 1} ↑s], BddAbove s The theorem `Cardinal.bddAbove_of_small` states that for any set `s` of Cardinal numbers, if `s` is small (i.e., there exists an injection from `s` to a type in Universe `u`), then `s` is bounded above. In other words, there exists a cardinal number that serves as an upper bound for all the elements in the set `s`. More concisely: If a set `s` of Cardinal numbers is small, then it is bounded above.
`Cardinal.sum_le_sum` theorem Cardinal.sum_le_sum : ∀ {ι : Type u_1} (f g : ι → Cardinal.{u_2}), (∀ (i : ι), f i ≤ g i) → Cardinal.sum f ≤ Cardinal.sum g The theorem `Cardinal.sum_le_sum` states that for any indexed type `ι` and any two functions `f` and `g` from this index type to Cardinal numbers, if for each index `i` the Cardinal number given by `f` at `i` is less than or equal to the Cardinal number given by `g` at `i`, then the sum of the Cardinal numbers given by `f` (which corresponds to the cardinality of the disjoint union indexed by `ι` with cardinalities given by `f`) is less than or equal to the sum of the Cardinal numbers given by `g` (which corresponds to the cardinality of the disjoint union indexed by `ι` with cardinalities given by `g`). More concisely: For any indexed type ι and functions f, g from ι to Cardinal numbers, if for all i in ι, f(i) ≤ g(i), then Σ i : ι, f(i) ≤ Σ i : ι, g(i).
`Cardinal.mk_range_le_lift` theorem Cardinal.mk_range_le_lift : ∀ {α : Type u} {β : Type v} {f : α → β}, Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) ≤ Cardinal.lift.{v, u} (Cardinal.mk α) This theorem states that for all types `α` and `β`, and any function `f` from `α` to `β`, the cardinality of the image of `f` when lifted to a higher universe (which is represented as `Cardinal.lift (Cardinal.mk ↑(Set.range f))`) is less than or equal to the cardinality of `α` lifted to a higher universe (represented by `Cardinal.lift (Cardinal.mk α)`). This essentially captures the mathematical concept that the size of the image of a function cannot exceed the size of its domain, even when considering cardinalities in different type universes. More concisely: For any function between types `α` and `β`, the cardinality of its image, lifted to a higher universe, is less than or equal to the cardinality of `α`, lifted to the same universe.
`Cardinal.le_aleph0_iff_set_countable` theorem Cardinal.le_aleph0_iff_set_countable : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑s ≤ Cardinal.aleph0 ↔ s.Countable This theorem states that for any arbitrary type `α` and a set `s` of this type, the cardinality of the set `s` is less than or equal to the smallest infinite cardinal number (`ℵ₀`) if and only if the set `s` is countable. In other words, it provides a characterization of countable sets in terms of their cardinality, implying that a set is countable if its size does not exceed the size of the set of natural numbers. More concisely: A set `s` of type `α` is countable if and only if its cardinality is less than or equal to the first infinite cardinal number `ℵ₀`.
`Cardinal.natCast_lt` theorem Cardinal.natCast_lt : ∀ {m n : ℕ}, ↑m < ↑n ↔ m < n This theorem, `Cardinal.natCast_lt`, states that for all natural numbers `m` and `n`, the cardinality of `m`, denoted by `↑m`, is less than the cardinality of `n`, denoted by `↑n`, if and only if `m` is less than `n`. In other words, it provides a relationship between the less-than relation `<` on natural numbers and the less-than relation `<` on their corresponding cardinal numbers. More concisely: For all natural numbers m and n, `↑m` < `↑n` if and only if m < n.
`Cardinal.lift_iSup` theorem Cardinal.lift_iSup : ∀ {ι : Type v} {f : ι → Cardinal.{w}}, BddAbove (Set.range f) → Cardinal.lift.{u, w} (iSup f) = ⨆ i, Cardinal.lift.{u, w} (f i) The theorem `Cardinal.lift_iSup` states that for any type `ι` and any function `f` from `ι` to Cardinals, if the range of `f` is bounded above, then lifting the supremum of `f` (i.e., the largest cardinal number in the image of `f`) to the maximum of the universes `u` and `w` is the same as taking the supremum of the set of all cardinals obtained by lifting each value of `f(i)` to the same universes. In other words, the lift operation commutes with the supremum operation. More concisely: For any type `ι` and function `f` from `ι` to Cardinals with a bounded above range, the supremum of the cardinals obtained by lifting each `f(i)` equals the lift of the supremum of `f(i)`.
`Cardinal.eq` theorem Cardinal.eq : ∀ {α β : Type u}, Cardinal.mk α = Cardinal.mk β ↔ Nonempty (α ≃ β) This theorem states that for any two types `α` and `β`, the cardinality of `α` is equal to the cardinality of `β` if and only if there exists a bijection between `α` and `β`. In other words, there's a one-to-one correspondence between the elements of `α` and `β`. More concisely: For types `α` and `β`, their cardinalities are equal if and only if there exists a bijection between them.
`Cardinal.aleph0_le_mul_iff'` theorem Cardinal.aleph0_le_mul_iff' : ∀ {a b : Cardinal.{u}}, Cardinal.aleph0 ≤ a * b ↔ a ≠ 0 ∧ Cardinal.aleph0 ≤ b ∨ Cardinal.aleph0 ≤ a ∧ b ≠ 0 := by sorry This theorem, `Cardinal.aleph0_le_mul_iff'`, states that for any two cardinal numbers `a` and `b`, the condition that the smallest infinite cardinal number (`ℵ₀` or `Cardinal.aleph0`) is less than or equal to the product of `a` and `b` is equivalent to one of two possibilities: either `a` is not zero and `ℵ₀` is less than or equal to `b`, or `ℵ₀` is less than or equal to `a` and `b` is not zero. More concisely: The theorem `Cardinal.aleph0_le_mul` asserts that for any cardinal numbers `a` and `b`, `ℵ₀ ≤ a × b` if and only if either `a ≠ 0` and `ℵ₀ ≤ b`, or `ℵ₀ ≤ a` and `b ≠ 0`.
`Cardinal.bddAbove_range` theorem Cardinal.bddAbove_range : ∀ {ι : Type u} (f : ι → Cardinal.{max u v}), BddAbove (Set.range f) This theorem states that for any type `ι` and a function `f` from `ι` to a cardinal number in a universe that is potentially larger than the universe of `ι`, the range of `f` is always bounded above. In the language of mathematics, this means there exists an upper bound for the set of cardinal numbers that are produced as outputs by the function `f`. More concisely: For any type `ι` and function `f` from `ι` to a cardinal number, there exists a cardinal number that is an upper bound for the range of `f`.
`Cardinal.lift_le` theorem Cardinal.lift_le : ∀ {a b : Cardinal.{v}}, Cardinal.lift.{u, v} a ≤ Cardinal.lift.{u, v} b ↔ a ≤ b The theorem `Cardinal.lift_le` states that for any two cardinal numbers `a` and `b` in a certain type universe `v`, the universe lift operation `Cardinal.lift` to a larger type universe `u` preserves the order of these cardinal numbers. More specifically, the lifted cardinal `a` is less than or equal to the lifted cardinal `b` if and only if the original cardinal `a` is less than or equal to the original cardinal `b`. More concisely: For all cardinal numbers `a` and `b` in universe `v`, `Cardinal.lift a < Cardinal.lift b` if and only if `a <= b`.
`Cardinal.one_lt_aleph0` theorem Cardinal.one_lt_aleph0 : 1 < Cardinal.aleph0 The theorem `Cardinal.one_lt_aleph0` states that the cardinality of the set of natural numbers (also known as `ℵ₀` or `aleph0`) is greater than one. In other words, the size of the set of natural numbers is larger than the size of a singleton set, confirming the intuitive idea that there are infinitely many natural numbers. More concisely: The cardinality of the set of natural numbers is strictly greater than that of a singleton set.
`Cardinal.nat_lt_lift_iff` theorem Cardinal.nat_lt_lift_iff : ∀ {n : ℕ} {a : Cardinal.{u}}, ↑n < Cardinal.lift.{v, u} a ↔ ↑n < a This theorem, `Cardinal.nat_lt_lift_iff`, states that for any natural number `n` and any cardinal number `a` of any type `u`, the embedding of `n` into the cardinal numbers is less than the universe lift of `a` to `max v u` if and only if the embedding of `n` is less than `a`. In other words, lifting a cardinal to a higher universe level does not change its comparison with a natural number. More concisely: For any natural number `n` and cardinal number `a` of type `u`, `n < a` if and only if `nat_cast n < lift_card a (max v u)` in Lean 4.
`Cardinal.lt_aleph0_iff_finite` theorem Cardinal.lt_aleph0_iff_finite : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Finite α This theorem states that for any type `α`, the cardinality of `α` is less than `aleph0` (the smallest infinite cardinal number, often used to represent the cardinality of the set of natural numbers) if and only if `α` is a finite set. In other words, it establishes a correspondence between the finiteness of a set in terms of set theory, and its cardinality being less than the first infinite cardinal number, `aleph0`. More concisely: A set `α` is finite if and only if the cardinality of `α` is less than the first infinite cardinal number `aleph0`.
`Cardinal.power_le_power_right` theorem Cardinal.power_le_power_right : ∀ {a b c : Cardinal.{u_1}}, a ≤ b → a ^ c ≤ b ^ c This theorem, named `Cardinal.power_le_power_right`, states that for every three cardinal numbers `a`, `b`, and `c` in a particular universe `u_1`, if `a` is less than or equal to `b`, then `a` raised to the power of `c` is less than or equal to `b` raised to the power of `c`. This is a statement about the preservation of order under exponentiation in the context of cardinal numbers. More concisely: For all cardinal numbers `a`, `b`, and `c`, if `a ≤ b` then `a^c ≤ b^c`.
`Cardinal.aleph0_ne_zero` theorem Cardinal.aleph0_ne_zero : Cardinal.aleph0 ≠ 0 This theorem states that the smallest infinite cardinal number, often represented as `ℵ₀` (aleph null), is not equal to zero. In the context of set theory, `ℵ₀` is the cardinality of the set of natural numbers, implying that the set of natural numbers is not empty, hence its cardinality cannot be zero. More concisely: The theorem asserts that `ℵ₀ ≠ 0`, where `ℵ₀` is the cardinality of the set of natural numbers.
`Cardinal.lift_lt` theorem Cardinal.lift_lt : ∀ {a b : Cardinal.{u}}, Cardinal.lift.{v, u} a < Cardinal.lift.{v, u} b ↔ a < b This theorem states that for any two cardinal numbers `a` and `b` in a certain type universe `u`, the lifting of `a` and `b` to a potentially larger universe `v` preserves the order relation. In other words, `a` is less than `b` in the original universe if and only if the lift of `a` is less than the lift of `b` in the larger universe. Here, 'less than' refers to cardinality, meaning that there is no bijection between the two sets, but there is an injective (one-to-one) function from the set with smaller cardinality to the set with larger cardinality. More concisely: For any cardinal numbers `a` and `b` in universe `u`, if `a` is smaller than `b` in cardinality, then their liftings to universe `v` also satisfy `lift a < lift b`.
`Cardinal.le_sum` theorem Cardinal.le_sum : ∀ {ι : Type u_1} (f : ι → Cardinal.{max u_1 u_2}) (i : ι), f i ≤ Cardinal.sum f The theorem `Cardinal.le_sum` states that for any type `ι` and a function `f` mapping each element of `ι` to a cardinal number, the cardinality of any single `i` in `ι` (given by `f i`) is less than or equal to the sum of the cardinalities of all elements in `ι` (given by `Cardinal.sum f`). In other words, the size of any individual component in the disjoint union of sets (represented by the sum of cardinals) is at most the size of the entire disjoint union. More concisely: For any type `ι` and function `f` mapping each element of `ι` to a cardinal number, the cardinality of each `i` in `ι` (`f i`) is less than or equal to the sum of the cardinalities of all `i` in `ι` (`Cardinal.sum f`).
`Cardinal.aleph0_pos` theorem Cardinal.aleph0_pos : 0 < Cardinal.aleph0 This theorem states that Aleph-zero (ℵ₀), which is known as the smallest infinite cardinal number or the cardinality of the set of natural numbers, is greater than zero. In the context of set theory, it establishes that the size of the set of natural numbers is not empty, but rather infinitely countable, and hence larger than zero. More concisely: The theorem asserts that ℵ₀, the cardinality of the set of natural numbers, is strictly greater than 0.
`Cardinal.mk_le_of_module` theorem Cardinal.mk_le_of_module : ∀ (R : Type u) (E : Type v) [inst : AddCommGroup E] [inst_1 : Ring R] [inst_2 : Module R E] [inst_3 : Nontrivial E] [inst : NoZeroSMulDivisors R E], Cardinal.lift.{v, u} (Cardinal.mk R) ≤ Cardinal.lift.{u, v} (Cardinal.mk E) This theorem states that for any ring `R` and module `E` over `R` which forms an additive commutative group and does not contain any zero scalar divisors, if `E` is nontrivial, then the cardinality of `R` (after universe lift operation) is less than or equal to the cardinality of `E` (after universe lift operation). In other words, given a nontrivial module without zero scalar multiplication divisors, the cardinality (size) of the ring it is built on can't be greater than the cardinality (size) of the module itself. This is especially applicable when the ring is a field. More concisely: If `R` is a nontrivial ring without zero scalar divisors and `E` is a nontrivial additive commutative group module over `R`, then the cardinality of `R` is less than or equal to the cardinality of `E`.
`Cardinal.mk_image_le` theorem Cardinal.mk_image_le : ∀ {α β : Type u} {f : α → β} {s : Set α}, Cardinal.mk ↑(f '' s) ≤ Cardinal.mk ↑s := by sorry The theorem `Cardinal.mk_image_le` states that for any types `α` and `β`, and for any function `f` from `α` to `β` and any set `s` of type `α`, the cardinality of the image of `s` under `f` is less than or equal to the cardinality of `s`. In other words, the function `f` cannot increase the cardinality of the set `s` through its mapping. More concisely: For any function from a type to another and any subset of the domain, the cardinality of the image of the subset under the function is less than or equal to the cardinality of the subset.
`Mathlib.SetTheory.Cardinal.Basic._auxLemma.78` theorem Mathlib.SetTheory.Cardinal.Basic._auxLemma.78 : ∀ {α : Type u}, (Cardinal.aleph0 ≤ Cardinal.mk α) = Infinite α This theorem states that for any type `α`, the cardinality of `α` is greater than or equal to `ℵ₀` (the smallest infinite cardinal, which is the cardinality of the set of natural numbers) if and only if `α` is an infinite set. In other words, if a set has cardinality at least as large as the set of natural numbers, then it is an infinite set. More concisely: A set `α` has cardinality greater than or equal to that of the natural numbers if and only if `α` is infinite.
`Mathlib.SetTheory.Cardinal.Basic._auxLemma.26` theorem Mathlib.SetTheory.Cardinal.Basic._auxLemma.26 : ∀ {c : Cardinal.{u}}, (Cardinal.aleph0 < Cardinal.lift.{v, u} c) = (Cardinal.aleph0 < c) The theorem `Mathlib.SetTheory.Cardinal.Basic._auxLemma.26` states that, for any cardinal number `c`, the statement that the cardinal number `ℵ₀` (also known as aleph null, which represents the cardinality of the set of natural numbers and is the smallest infinite cardinal) is less than the lift of `c` to a possibly larger universe is equivalent to the statement that `ℵ₀` is less than `c` in the original universe. This means that lifting a cardinal to a larger universe does not change its comparison with `ℵ₀`. More concisely: For any cardinal number `c`, the lift of `c` to a larger universe maintains the strict inequality with `ℵ₀` if and only if `c` strictly precedes `ℵ₀` in the cardinal order of the original universe.
`Cardinal.lift_mk_eq'` theorem Cardinal.lift_mk_eq' : ∀ {α : Type u} {β : Type v}, Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β) This theorem, named `Cardinal.lift_mk_eq'`, asserts a property about the cardinality of types and their equivalence in different universes in Lean. Specifically, for any types `α` and `β` in universes `u` and `v`, respectively, the universe lift operation on the cardinality of `α`, taken from universe `v` to `u`, is equal to the universe lift operation on the cardinality of `β`, taken from universe `u` to `v`, if and only if there is a nonempty equivalence between `α` and `β`. This theorem is a specialized version of `Cardinal.lift_mk_eq`, provided separately because Lean often cannot automatically apply the correct specialization. More concisely: For any types α and β in universes u and v, respectively, the universe-lifted cardinalities of α and β are equal if and only if there exists a nonempty equivalence between them.
`Cardinal.inductionOn` theorem Cardinal.inductionOn : ∀ {p : Cardinal.{u_1} → Prop} (c : Cardinal.{u_1}), (∀ (α : Type u_1), p (Cardinal.mk α)) → p c The theorem `Cardinal.inductionOn` is a principle of mathematical induction for cardinal numbers. Given a property `p` that applies to cardinal numbers, and a specific cardinal number `c`, if we can show that the property `p` holds for the cardinality of any type `α`, then it must also hold for the cardinal number `c`. More concisely: If a property holds for the cardinality of every type, then it holds for a given cardinal number. (Cardinal induction)
`Cardinal.cantor` theorem Cardinal.cantor : ∀ (a : Cardinal.{u}), a < 2 ^ a Cantor's theorem states that for any cardinal number `a`, `a` is strictly less than `2 ^ a`. In other words, the cardinality of any set is always less than the cardinality of the power set of that set. The power set of a set is the set of all of its subsets, and its cardinality (or size) is represented in Lean by `2 ^ a`. This theorem is a fundamental result in set theory and reveals the existence of different "sizes" of infinity in mathematics. More concisely: For any cardinal number `a`, the cardinality of a set is strictly less than the cardinality of its power set, `2 ^ a`.
`Cardinal.nsmul_lt_aleph0_iff_of_ne_zero` theorem Cardinal.nsmul_lt_aleph0_iff_of_ne_zero : ∀ {n : ℕ} {a : Cardinal.{u_1}}, n ≠ 0 → (n • a < Cardinal.aleph0 ↔ a < Cardinal.aleph0) The theorem `Cardinal.nsmul_lt_aleph0_iff_of_ne_zero` establishes a condition for comparing cardinals and the smallest infinite cardinal, `aleph0`. Specifically, for any natural number `n` and any cardinal number `a`, if `n` is not zero, then the result of `n`-times scalar multiplication of `a` is less than `aleph0` if and only if `a` is itself less than `aleph0`. This provides a way to infer the relative size of `a` in the context of infinite cardinality, based on the scalar multiplication of `a`. More concisely: For any natural number $n \neq 0$ and cardinal number $a$, $n \cdot a < \aleph\_0 \iff a < \aleph\_0$.
`Cardinal.one_le_iff_ne_zero` theorem Cardinal.one_le_iff_ne_zero : ∀ {c : Cardinal.{u_1}}, 1 ≤ c ↔ c ≠ 0 This theorem states that for any cardinal number `c` from the universe `u_1`, the cardinal number `c` is greater than or equal to one if and only if `c` is not equal to zero. In other words, in the context of cardinal numbers, a cardinal number is non-zero if and only if it is at least one. More concisely: For any cardinal number `c`, `c` is non-zero if and only if `c` is greater than or equal to one.
`Cardinal.lt_aleph0` theorem Cardinal.lt_aleph0 : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph0 ↔ ∃ n, c = ↑n The theorem `Cardinal.lt_aleph0` asserts that for any cardinal number `c`, the condition `c` being less than `ℵ₀` (the smallest infinite cardinal, also known as the cardinality of natural numbers) is equivalent to the existence of a natural number `n` such that `c` is equal to the cardinality of `n`. In other words, a cardinal number is less than the smallest infinite cardinal if and only if it corresponds to a finite set. More concisely: A cardinal number `c` is less than the first infinite cardinal `ℵ₀` if and only if it is the cardinality of a finite set.
`Cardinal.bddAbove_iff_small` theorem Cardinal.bddAbove_iff_small : ∀ {s : Set Cardinal.{u}}, BddAbove s ↔ Small.{u, u + 1} ↑s The theorem `Cardinal.bddAbove_iff_small` states that for any set of cardinal numbers (a set `s` of type `Cardinal`), this set has an upper bound if and only if it is a small set. In the context of this theorem, a "small" set is one that corresponds to a usual Zermelo-Fraenkel set theory (ZFC) set. The notation `Small.{u, u + 1}` denotes a small set in the type universe `u` that maps to the universe `u + 1`. More concisely: A set of cardinal numbers has an upper bound if and only if it is a small set.
`Cardinal.sum_lt_prod` theorem Cardinal.sum_lt_prod : ∀ {ι : Type u_1} (f g : ι → Cardinal.{u_2}), (∀ (i : ι), f i < g i) → Cardinal.sum f < Cardinal.prod g König's theorem states that for any indexed set of cardinals, denoted by ι, and any two cardinal-valued functions f and g over ι, if each cardinal produced by f is strictly less than the corresponding cardinal produced by g for every index i, then the cardinality of the indexed sum (or disjoint union) of f is strictly less than the cardinality of the indexed product (or dependent product) of g. More concisely: If for every index i, the cardinal produced by function f(i) is strictly less than the cardinal produced by function g(i), then the cardinality of the disjoint union of the sets indexed by f is strictly less than the cardinality of the dependent product of the sets indexed by g.
`Cardinal.sum_le_iSup_lift` theorem Cardinal.sum_le_iSup_lift : ∀ {ι : Type u} (f : ι → Cardinal.{max u v}), Cardinal.sum f ≤ Cardinal.lift.{v, u} (Cardinal.mk ι) * iSup f := by sorry This theorem states that for any type `ι` and a function `f` from `ι` to a cardinal number, the indexed sum of cardinal numbers (which is the cardinality of the indexed disjoint union), denoted by `Cardinal.sum f`, is less than or equal to the product of the universe lift of the cardinal number of `ι` and the indexed supremum of `f`. In other words, for any type and a function mapping the type to cardinal numbers, the total cardinality of the disjoint union indexed by the type is at most the product of the cardinality of the type and the supremum of the cardinalities that the function maps to. More concisely: For any type `ι` and function `f` from `ι` to cardinal numbers, the cardinality of the indexed sum of `ι` is less than or equal to the product of the cardinality of `ι` and the supremum of `f`.
`Cardinal.power_mul` theorem Cardinal.power_mul : ∀ {a b c : Cardinal.{u_1}}, a ^ (b * c) = (a ^ b) ^ c The theorem `Cardinal.power_mul` states that for any three cardinal numbers `a`, `b`, and `c`, the cardinal number `a` raised to the power of the product of `b` and `c` equals the cardinal number `a` raised to the power `b` and then that result raised to the power `c`. This theorem effectively establishes the law of exponentiation for cardinal numbers, namely that $(a^{b})^{c} = a^{b \times c}$. More concisely: For any cardinal numbers `a`, `b`, and `c`, `a^(bc) = a^b ^ c`.
`Cardinal.le_def` theorem Cardinal.le_def : ∀ (α β : Type u), Cardinal.mk α ≤ Cardinal.mk β ↔ Nonempty (α ↪ β) The theorem `Cardinal.le_def` states that for any two types `α` and `β`, the cardinality of `α` is less than or equal to the cardinality of `β` if and only if there is a nonempty injective function from `α` to `β`. Here, `Cardinal.mk α` represents the cardinal number of the type `α`, and `α ↪ β` indicates an injective (one-to-one) function from `α` to `β`. This theorem asserts a fundamental relationship between cardinality comparison and the existence of injective functions between types. More concisely: For any types α and β, the cardinality of α is less than or equal to the cardinality of β if and only if there exists an injective function from α to β.
`Cardinal.lift_max` theorem Cardinal.lift_max : ∀ {a b : Cardinal.{v}}, Cardinal.lift.{u, v} (max a b) = max (Cardinal.lift.{u, v} a) (Cardinal.lift.{u, v} b) := by sorry The theorem `Cardinal.lift_max` states that for any two cardinal numbers `a` and `b` in some universe `v`, lifting the maximum of `a` and `b` to a larger universe `u` is the same as taking the maximum of the lifts of `a` and `b` to this larger universe. In other words, the operation of "lifting" a cardinal to a larger universe commutes with taking the maximum. More concisely: For any cardinal numbers `a` and `b` and universes `v` and `u` with `v` a subuniverse of `u`, the lift of the maximum of `a` and `b` to `u` equals the maximum of the lifts of `a` and `b` to `u`.
`Cardinal.power_one` theorem Cardinal.power_one : ∀ {a : Cardinal.{u}}, a ^ 1 = a This theorem states that for any cardinal number `a`, when `a` is raised to the power of one, the result is `a` itself. This is consistent with the general mathematical rule that any number (including cardinal numbers) to the power of one equals the number itself. The power operation in this context is defined in terms of cardinal numbers, a type used to represent the size of a set in set theory, abstracted to higher type levels in Lean. More concisely: For any cardinal number `a`, `a^1` equals `a`.
`Cardinal.lift_sum` theorem Cardinal.lift_sum : ∀ {ι : Type u} (f : ι → Cardinal.{v}), Cardinal.lift.{w, max v u} (Cardinal.sum f) = Cardinal.sum fun i => Cardinal.lift.{w, v} (f i) The theorem `Cardinal.lift_sum` states that for any type ι and a function `f` from ι to the set of cardinal numbers, lifting the cardinality of the indexed sum (the disjoint union of the sets indexed by ι) to a larger universe is the same as taking the indexed sum of the cardinals of the sets after individually lifting them to the larger universe. In more mathematical terms, for any ι and a function `f : ι → Cardinal`, we have `Cardinal.lift (Cardinal.sum f) = Cardinal.sum (λ i => Cardinal.lift (f i))`. This theorem essentially shows that lifting to a larger universe commutes with taking an indexed sum in the context of cardinal numbers. More concisely: The theorem asserts that lifting the cardinality of the indexed sum of a function from a type to cardinal numbers, to a larger universe, is equivalent to summing the individually lifted cardinals.
`Cardinal.mk_arrow` theorem Cardinal.mk_arrow : ∀ (α : Type u) (β : Type v), Cardinal.mk (α → β) = Cardinal.lift.{u, v} (Cardinal.mk β) ^ Cardinal.lift.{v, u} (Cardinal.mk α) The theorem `Cardinal.mk_arrow` states that for any two types `α` and `β`, the cardinality of the function type from `α` to `β` (`α → β`) is equal to the cardinality of `β` lifted to the maximum of universe levels of `α` and `β`, raised to the power of the cardinality of `α` lifted to the maximum of universe levels of `α` and `β`. Here, cardinality is a measure of the "size" of a type, the lift operation adjusts the universe level of a cardinal number, and `α → β` represents the type of functions from `α` to `β`. More concisely: The cardinality of the function type `α → β` is equal to the cardinality of `β` lifted to the maximum of the universe levels of `α` and `β`, raised to the power of the cardinality of `α` lifted to the maximum of the universe levels of `α` and `β`.
`Cardinal.mk_le_of_injective` theorem Cardinal.mk_le_of_injective : ∀ {α β : Type u} {f : α → β}, Function.Injective f → Cardinal.mk α ≤ Cardinal.mk β This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, if the function `f` is injective (i.e., no two different elements in `α` map to the same element in `β`), then the cardinality of `α` (denoted as `Cardinal.mk α`) is less than or equal to the cardinality of `β` (denoted as `Cardinal.mk β`). In other words, the size of `α` is no larger than the size of `β` when there is an injective function from `α` to `β`. More concisely: If `f` is an injective function from type `α` to type `β`, then `Cardinal.mk α ≤ Cardinal.mk β`.
`Cardinal.mk_denumerable` theorem Cardinal.mk_denumerable : ∀ (α : Type u) [inst : Denumerable α], Cardinal.mk α = Cardinal.aleph0 The theorem `Cardinal.mk_denumerable` states that for any type `α` which is denumerable (i.e., it can be put into a one-to-one correspondence with the set of natural numbers), the cardinality (or size) of `α` is equal to `ℵ₀`, the smallest infinite cardinal number. In other words, if a type can be listed in a sequence like the natural numbers, then it has the same size as the set of natural numbers. More concisely: If a type `α` is denumerable, then its cardinality equals that of the natural numbers, i.e., `α` is equinumerous with `ℕ` and therefore has cardinality `ℵ₀`.
`Cardinal.nat_eq_lift_iff` theorem Cardinal.nat_eq_lift_iff : ∀ {n : ℕ} {a : Cardinal.{u}}, ↑n = Cardinal.lift.{v, u} a ↔ ↑n = a This theorem states that for any natural number `n` and any cardinal number `a` in the universe `u`, the cardinal number equivalent of `n` is equal to the universe lift of `a` (i.e., `a` moved to a potentially larger universe `v`) if and only if the cardinal number equivalent of `n` is equal to `a`. In other words, it asserts the equivalence between the two conditions: the cardinality of `n` being equal to the universe lift of `a` and the cardinality of `n` being equal to `a`. More concisely: For any natural number `n` and cardinal number `a`, the cardinality of `n` equals the universe lift of `a` if and only if the cardinality of `n` equals `a`.
`Cardinal.inductionOn₂` theorem Cardinal.inductionOn₂ : ∀ {p : Cardinal.{u_1} → Cardinal.{u_2} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}), (∀ (α : Type u_1) (β : Type u_2), p (Cardinal.mk α) (Cardinal.mk β)) → p c₁ c₂ The theorem `Cardinal.inductionOn₂` is a principle of mathematical induction for two cardinal numbers. It states that for all properties `p`, defined on two cardinal numbers `c₁` and `c₂` in different type universes `u_1` and `u_2`, if the property `p` holds for all pairs of types `α` and `β` (where type `α` is in universe `u_1` and type `β` is in universe `u_2`, and the cardinal numbers of these types are `Cardinal.mk α` and `Cardinal.mk β` respectively), then the property `p` also holds for the cardinal numbers `c₁` and `c₂`. More concisely: If `p` is a property of cardinal numbers `Cardinal.mk α` and `Cardinal.mk β`, and `p` holds for all pairs of types `α` and `β` with cardinalities `α` and `β`, then `p` holds for the cardinal numbers `c₁` and `c₂` where `c₁ = Cardinal.mk α` and `c₂ = Cardinal.mk β`.
`Cardinal.one_le_aleph0` theorem Cardinal.one_le_aleph0 : 1 ≤ Cardinal.aleph0 This theorem states that the cardinal number one is less than or equal to aleph zero. Aleph zero, denoted as `ℵ₀`, is the smallest infinite cardinal number, typically corresponding to the cardinality (size) of the set of natural numbers. In other words, the size of any set with at least one element cannot be larger than the size of the set of natural numbers. More concisely: One is less than or equal to aleph zero (ℵ₀).
`Cardinal.prod_const` theorem Cardinal.prod_const : ∀ (ι : Type u) (a : Cardinal.{v}), (Cardinal.prod fun x => a) = Cardinal.lift.{u, v} a ^ Cardinal.lift.{v, u} (Cardinal.mk ι) The theorem `Cardinal.prod_const` states that for any type `ι` and any cardinal number `a`, the cardinality of the product type where each type in the product has the cardinality `a` is equal to `a` to the power of the cardinality of `ι`. This is expressed in the theorem as `(Cardinal.prod fun x => a) = Cardinal.lift.{u, v} a ^ Cardinal.lift.{v, u} (Cardinal.mk ι)`. Here, `Cardinal.prod` is the cardinality of the dependent product of a type-indexed family of types, `Cardinal.lift` raises the level of a cardinal number, and `Cardinal.mk` gives the cardinality of a type. The theorem essentially expresses a property of cardinal arithmetic for type-indexed products of types. More concisely: The theorem `Cardinal.prod_const` asserts that the cardinality of the product of `ι` types, each having cardinality `a`, equals `a` raised to the power of the cardinality of `ι`.
`Cardinal.lt_aleph0_of_finite` theorem Cardinal.lt_aleph0_of_finite : ∀ (α : Type u) [inst : Finite α], Cardinal.mk α < Cardinal.aleph0 The theorem `Cardinal.lt_aleph0_of_finite` states that for any type `α` that is finite (as indicated by the instance `inst : Finite α`), the cardinality of `α` (represented as `Cardinal.mk α`) is less than `ℵ₀` (aleph-zero), which is the cardinality of the set of natural numbers. In other words, the size of any finite set is less than the size of the set of natural numbers. More concisely: For any finite type `α`, the cardinality of `α` is strictly less than that of the natural numbers.
`Cardinal.mk_sigma` theorem Cardinal.mk_sigma : ∀ {ι : Type u_2} (f : ι → Type u_1), Cardinal.mk ((i : ι) × f i) = Cardinal.sum fun i => Cardinal.mk (f i) := by sorry The theorem `Cardinal.mk_sigma` states that for any type `ι` and a function `f` from `ι` to another type, the cardinality of the sigma type (i.e., dependent pair type) `(i : ι) × f i` is equal to the sum of the cardinalities of the types `f i` for each `i` in `ι`. In other words, the size of the disjoint union of all types `f i` (where `i` ranges over `ι`) is the same as the total size of all these types counted separately. More concisely: The theorem asserts that the cardinality of the dependent sum (sigma type) over a type `ι` and a function `f` from `ι` to another type equals the sum of the cardinalities of the images `f i` for all `i` in `ι`.

LeanAide GPT-4 documentation

Module: Mathlib.SetTheory.Cardinal.Basic

Cardinal.aleph0_le_lift

theorem Cardinal.aleph0_le_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph0 ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 ≤ c

Cardinal.lift_mk_eq

theorem Cardinal.lift_mk_eq : ∀ {α : Type u} {β : Type v}, Cardinal.lift.{max v w, u} (Cardinal.mk α) = Cardinal.lift.{max u w, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β)

Cardinal.lift_down

theorem Cardinal.lift_down : ∀ {a : Cardinal.{u}} {b : Cardinal.{max u v}}, b ≤ Cardinal.lift.{v, u} a → ∃ a', Cardinal.lift.{v, u} a' = b := by sorry

Cardinal.lift_mk_le'

theorem Cardinal.lift_mk_le' : ∀ {α : Type u} {β : Type v}, Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ↪ β)

Cardinal.mk_eq_zero_iff

theorem Cardinal.mk_eq_zero_iff : ∀ {α : Type u}, Cardinal.mk α = 0 ↔ IsEmpty α

Cardinal.lift_id

theorem Cardinal.lift_id : ∀ (a : Cardinal.{u}), Cardinal.lift.{u, u} a = a

Cardinal.sum_le_iSup

theorem Cardinal.sum_le_iSup : ∀ {ι : Type u} (f : ι → Cardinal.{u}), Cardinal.sum f ≤ Cardinal.mk ι * iSup f := by sorry

Cardinal.le_mk_iff_exists_set

theorem Cardinal.le_mk_iff_exists_set : ∀ {c : Cardinal.{u}} {α : Type u}, c ≤ Cardinal.mk α ↔ ∃ p, Cardinal.mk ↑p = c

Cardinal.lt_aleph0_iff_fintype

theorem Cardinal.lt_aleph0_iff_fintype : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Nonempty (Fintype α) := by sorry

Cardinal.mk_le_mk_of_subset

theorem Cardinal.mk_le_mk_of_subset : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → Cardinal.mk ↑s ≤ Cardinal.mk ↑t := by sorry

Cardinal.lift_iSup_le_lift_iSup

Cardinal.lift_monotone

theorem Cardinal.lift_monotone : Monotone Cardinal.lift.{u_2, u_1}

Cardinal.mk_preimage_of_subset_range_lift

theorem Cardinal.mk_preimage_of_subset_range_lift : ∀ {α : Type u} {β : Type v} (f : α → β), ∀ s ⊆ Set.range f, Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑(f ⁻¹' s))

Cardinal.mk_singleton

theorem Cardinal.mk_singleton : ∀ {α : Type u} (x : α), Cardinal.mk ↑{x} = 1

Cardinal.power_le_power_left

theorem Cardinal.power_le_power_left : ∀ {a b c : Cardinal.{u_1}}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

Cardinal.mk_fintype

theorem Cardinal.mk_fintype : ∀ (α : Type u) [h : Fintype α], Cardinal.mk α = ↑(Fintype.card α)

Cardinal.mk_iUnion_le

theorem Cardinal.mk_iUnion_le : ∀ {α ι : Type u} (f : ι → Set α), Cardinal.mk ↑(⋃ i, f i) ≤ Cardinal.mk ι * ⨆ i, Cardinal.mk ↑(f i)

Cardinal.infinite_iff

theorem Cardinal.infinite_iff : ∀ {α : Type u}, Infinite α ↔ Cardinal.aleph0 ≤ Cardinal.mk α

Cardinal.mk_range_eq_of_injective

theorem Cardinal.mk_range_eq_of_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{v, u} (Cardinal.mk α)

Cardinal.mk_congr

theorem Cardinal.mk_congr : ∀ {α β : Type u}, α ≃ β → Cardinal.mk α = Cardinal.mk β

Cardinal.nat_succ

theorem Cardinal.nat_succ : ∀ (n : ℕ), ↑n.succ = Order.succ ↑n

Cardinal.mk_coe_finset

theorem Cardinal.mk_coe_finset : ∀ {α : Type u} {s : Finset α}, Cardinal.mk { x // x ∈ s } = ↑s.card

Cardinal.IsLimit.aleph0_le

theorem Cardinal.IsLimit.aleph0_le : ∀ {c : Cardinal.{u_1}}, c.IsLimit → Cardinal.aleph0 ≤ c

Cardinal.mk_ne_zero

theorem Cardinal.mk_ne_zero : ∀ (α : Type u) [inst : Nonempty α], Cardinal.mk α ≠ 0

Cardinal.power_def

theorem Cardinal.power_def : ∀ (α β : Type u), Cardinal.mk α ^ Cardinal.mk β = Cardinal.mk (β → α)

Cardinal.nsmul_lt_aleph0_iff

theorem Cardinal.nsmul_lt_aleph0_iff : ∀ {n : ℕ} {a : Cardinal.{u_1}}, n • a < Cardinal.aleph0 ↔ n = 0 ∨ a < Cardinal.aleph0

Set.Finite.lt_aleph0

theorem Set.Finite.lt_aleph0 : ∀ {α : Type u} {S : Set α}, S.Finite → Cardinal.mk ↑S < Cardinal.aleph0

Cardinal.succ_zero

theorem Cardinal.succ_zero : Order.succ 0 = 1

Cardinal.mk_set_le

theorem Cardinal.mk_set_le : ∀ {α : Type u} (s : Set α), Cardinal.mk ↑s ≤ Cardinal.mk α

Set.Countable.le_aleph0

theorem Set.Countable.le_aleph0 : ∀ {α : Type u} {s : Set α}, s.Countable → Cardinal.mk ↑s ≤ Cardinal.aleph0

Cardinal.card_le_of

theorem Cardinal.card_le_of : ∀ {α : Type u} {n : ℕ}, (∀ (s : Finset α), s.card ≤ n) → Cardinal.mk α ≤ ↑n

Cardinal.mk_le_of_surjective

theorem Cardinal.mk_le_of_surjective : ∀ {α β : Type u} {f : α → β}, Function.Surjective f → Cardinal.mk β ≤ Cardinal.mk α

Cardinal.lift_umax

theorem Cardinal.lift_umax : Cardinal.lift.{max u v, u} = Cardinal.lift.{v, u}

Cardinal.lift_id'

theorem Cardinal.lift_id' : ∀ (a : Cardinal.{max u v}), Cardinal.lift.{u, max u v} a = a

Set.Subsingleton.cardinal_mk_le_one

theorem Set.Subsingleton.cardinal_mk_le_one : ∀ {α : Type u} {s : Set α}, s.Subsingleton → Cardinal.mk ↑s ≤ 1 := by sorry

Cardinal.mk_out

theorem Cardinal.mk_out : ∀ (c : Cardinal.{u_1}), Cardinal.mk (Quotient.out c) = c

Cardinal.lt_aleph0_iff_set_finite

theorem Cardinal.lt_aleph0_iff_set_finite : ∀ {α : Type u} {S : Set α}, Cardinal.mk ↑S < Cardinal.aleph0 ↔ S.Finite

Cardinal.nat_lt_aleph0

theorem Cardinal.nat_lt_aleph0 : ∀ (n : ℕ), ↑n < Cardinal.aleph0

Cardinal.mk_le_aleph0_iff

theorem Cardinal.mk_le_aleph0_iff : ∀ {α : Type u}, Cardinal.mk α ≤ Cardinal.aleph0 ↔ Countable α

Cardinal.le_powerlt

`Cardinal.aleph0_le_lift`

`Cardinal.lift_mk_eq`

`Cardinal.lift_down`

`Cardinal.lift_mk_le'`

`Cardinal.mk_eq_zero_iff`

`Cardinal.lift_id`

`Cardinal.sum_le_iSup`

`Cardinal.le_mk_iff_exists_set`

`Cardinal.lt_aleph0_iff_fintype`

`Cardinal.mk_le_mk_of_subset`

`Cardinal.lift_iSup_le_lift_iSup`

`Cardinal.lift_monotone`

`Cardinal.mk_preimage_of_subset_range_lift`

`Cardinal.mk_singleton`

`Cardinal.power_le_power_left`

`Cardinal.mk_fintype`

`Cardinal.mk_iUnion_le`

`Cardinal.infinite_iff`

`Cardinal.mk_range_eq_of_injective`

`Cardinal.mk_congr`

`Cardinal.nat_succ`

`Cardinal.mk_coe_finset`

`Cardinal.IsLimit.aleph0_le`

`Cardinal.mk_ne_zero`

`Cardinal.power_def`

`Cardinal.nsmul_lt_aleph0_iff`

`Set.Finite.lt_aleph0`

`Cardinal.succ_zero`

`Cardinal.mk_set_le`

`Set.Countable.le_aleph0`

`Cardinal.card_le_of`

`Cardinal.mk_le_of_surjective`

`Cardinal.lift_umax`

`Cardinal.lift_id'`

`Set.Subsingleton.cardinal_mk_le_one`

`Cardinal.mk_out`

`Cardinal.lt_aleph0_iff_set_finite`

`Cardinal.nat_lt_aleph0`

`Cardinal.mk_le_aleph0_iff`

`Cardinal.le_powerlt`

`Cardinal.lift_zero`

`Cardinal.mk_uLift`

`Cardinal.sum_const`

`Cardinal.power_zero`

`Cardinal.natCast_le`

`Cardinal.mk_iUnion_le_sum_mk`

`Cardinal.aleph0_le_mul_iff`

`Cardinal.mk_pi`

`Cardinal.mk_univ`

`Cardinal.bddAbove_image`

`Cardinal.lift_iSup_le`

`Cardinal.lift_lt_aleph0`

`Cardinal.mk_eq_zero`

`Cardinal.one_lt_iff_nontrivial`

`Cardinal.lift_mk_fin`

`Cardinal.lift_mk_le`

`Cardinal.mk_prod`

`Cardinal.lift_aleph0`

`Cardinal.lift_injective`

`Cardinal.power_lt_aleph0`

`Cardinal.mk_eq_aleph0`

`Cardinal.lift_add`

`Cardinal.lift_le_aleph0`

`Cardinal.lift_uzero`

`Cardinal.add_lt_aleph0`

`Cardinal.exists_eq_of_iSup_eq_of_not_isLimit`

`Cardinal.mk_ne_zero_iff`

`Cardinal.lift_power`

`Cardinal.lift_lift`

`Cardinal.lift_sSup`

`Cardinal.mk_set`

`Cardinal.inductionOn₃`

`Cardinal.lift_umax'`

`Cardinal.lift_one`