small_of_injective
theorem small_of_injective :
∀ {α : Type v} {β : Type w} [inst : Small.{u, w} β] {f : α → β}, Function.Injective f → Small.{u, v} α
The theorem named `small_of_injective` states that for any types `α` and `β`, if `β` is "small" in some universe `u`, and there exists an injective function `f` from `α` to `β`, then `α` is also "small" in the same universe `u`. Here, a function `f` is said to be injective if for any two elements `a1` and `a2` in `α`, `f(a1) = f(a2)` implies `a1 = a2`. Furthermore, a type is considered "small" in a universe `u` if it can be embedded into a type of universe `u`.
More concisely: If `β` is a small type in some universe `u` and there exists an injective function from a type `α` to `β`, then `α` is also a small type in universe `u`.
|
small_of_surjective
theorem small_of_surjective :
∀ {α : Type v} {β : Type w} [inst : Small.{u, v} α] {f : α → β}, Function.Surjective f → Small.{u, w} β
The theorem `small_of_surjective` states that for all types `α` and `β`, if `α` is a "small" type and there exists a surjective function `f` from `α` to `β`, then `β` is also a "small" type. Here, a function `f` is surjective if for every element of `β`, there exists an element of `α` such that applying `f` to this element of `α` gives the element of `β`. The term "small" refers to a concept in type theory, usually referring to types that are not too large in some sense. This theorem is saying that the "smallness" property is preserved under surjective functions.
More concisely: If `α` is a small type and there exists a surjective function from `α` to `β`, then `β` is also a small type.
|
small_of_injective_of_exists
theorem small_of_injective_of_exists :
∀ {α : Type v} {β : Type w} {γ : Type v'} [inst : Small.{u, v} α] (f : α → γ) {g : β → γ},
Function.Injective g → (∀ (b : β), ∃ a, f a = g b) → Small.{u, w} β
This theorem, named `small_of_injective_of_exists`, states that for any types `α` and `β` and `γ`, given that `α` is of a smaller cardinality, if there exists a function `f` from `α` to `γ` and an injective function `g` from `β` to `γ` such that every element of `β` can be mapped to by `f` via some element of `α` (i.e., for every `b` in `β`, there exists an `a` in `α` such that `f(a)` equals `g(b)`), then `β` is also of a smaller cardinality. The theorem is a generalized version of `small_of_surjective`, which applies when `f` doesn't necessarily land in `β` but in a larger type `γ` that is related to `β` via an injective function `g`.
More concisely: If `α` is smaller than `β` and there exists an injective function `g` from `β` to `γ`, and a function `f` from `α` to `γ` such that every element in `β` is the image of some element in `α` under `f` via `g`, then `β` is also smaller than `α`.
|