small_lift
theorem small_lift : ∀ (α : Type u) [hα : Small.{v, u} α], Small.{max v w, u} α
The theorem `small_lift` states that for any type `α`, if `α` is a small type in a certain sense, which is specified by the structure `Small.{v, u} α`, then `α` is also a small type in a more general sense, specified by the structure `Small.{max v w, u} α`. This theorem is essentially lifting the "smallness" of a type from one context to a larger one. This concept of "smallness" is a technical one in the type theory underlying Lean 4, involving the size of types and the hierarchy of universes of types.
More concisely: If `α` is a small type in the context `Small.{v} α`, then it is also a small type in the context `Small.{max v w, u} α`.
|
Small.mk'
theorem Small.mk' : ∀ {α : Type v} {S : Type w}, α ≃ S → Small.{w, v} α
This theorem states that for any type `α` and another type `S`, if there exists an equivalence between `α` and `S` (denoted as `α ≃ S`), then `α` can be considered "small" relative to `S` (denoted as `Small.{w, v} α`). Here, the concept of "small" is a technical notion in type theory related to the size of types.
More concisely: If `α` is equivalent to type `S`, then `α` is considered "small" relative to `S` in type theory.
|
Small.equiv_small
theorem Small.equiv_small : ∀ {α : Type v} [self : Small.{w, v} α], ∃ S, Nonempty (α ≃ S)
This theorem states that for any type `α` of some universe `v` that is "small" with respect to another universe `w` (indicated by `Small.{w, v} α`), there exists a type `S` in the universe `w` such that `α` is equivalent to `S`. In other words, there is a bijection (one-to-one correspondence) between the elements of `α` and `S`. This is the formalization of the notion of "small" types in terms of existence of an equivalence with some type in a potentially smaller universe.
More concisely: For any small type `α` of universe `v` in a larger universe `w`, there exists a type `S` in `w` with a bijection from `α` to `S`.
|
small_max
theorem small_max : ∀ (α : Type v), Small.{max w v, v} α
This theorem, `small_max`, states that for any given type `α` in Lean 4, that type is "small". In the context of Lean 4's type theory, this means that `α` can be embedded in a type universe of size `max w v`. This has implications on the computational complexity and memory usage of operations involving values of type `α`. In other words, the type `α` is small with respect to the type universe `max w v`.
More concisely: For any type `α` in Lean 4's type theory, it can be embedded in a type universe of size `max w v`, where `w` and `v` are given type universes.
|
small_map
theorem small_map : ∀ {α : Type u_1} {β : Type u_2} [hβ : Small.{w, u_2} β], α ≃ β → Small.{w, u_1} α
This theorem, `small_map`, states that for any two types `α` and `β`, if `β` is a "small" type, then any equivalence (bijective mapping) from `α` to `β` implies that `α` is also a "small" type. The concept of "small" types in Lean's type theory is a way of avoiding certain paradoxes related to sizes of infinite sets; a small type is one that is not too large in a certain precise sense.
More concisely: If `β` is a small type and there exists a bijection from `α` to `β`, then `α` is also a small type.
|