ULift.down_bijective
theorem ULift.down_bijective : ∀ {α : Type u}, Function.Bijective ULift.down
The theorem `ULift.down_bijective` states that for all types `α`, the function `ULift.down` is bijective. In other words, `ULift.down` is both injective (no two different inputs yield the same output) and surjective (for every possible output there exists an input that produces that output). The function `ULift.down` extracts a value from a lifted type `ULift α`, and the bijectiveness of this function ensures that each value in the lifted type corresponds to exactly one value in the original type, and vice versa.
More concisely: The function `ULift.down` is a bijection between the types `α` and `ULift α`.
|
ULift.up_surjective
theorem ULift.up_surjective : ∀ {α : Type u}, Function.Surjective ULift.up
The theorem `ULift.up_surjective` states that for every type `α`, the function `ULift.up` is surjective. In other words, given any type `α`, for every `b` in the type `ULift α`, there exists an `a` in the original type `α` such that `ULift.up a = b`. Here, `ULift.up` is a function that takes a value of some type `α` and lifts it to a value of the type `ULift α`.
More concisely: For every type `α`, the function `ULift.up` from `α` to `ULift α` is surjective.
|
PLift.down_surjective
theorem PLift.down_surjective : ∀ {α : Sort u}, Function.Surjective PLift.down
The theorem `PLift.down_surjective` states that for any type `α`, the function `PLift.down` is surjective. In other words, for any type `α` and any element of that type, there exists a lifted version of that element such that when we apply the `PLift.down` function to this lifted element, we retrieve the original element.
More concisely: For any type `α`, the function `PLift.down` has a right inverse.
|
ULift.up_injective
theorem ULift.up_injective : ∀ {α : Type u}, Function.Injective ULift.up
The theorem `ULift.up_injective` states that for any type `α`, the function `ULift.up` is injective. In other words, for any two distinct elements `x` and `y` of type `α`, their lifted versions `ULift.up x` and `ULift.up y` are also distinct. This ensures that no information is lost when elements of a type are lifted to the `ULift` type using the `ULift.up` function.
More concisely: For all types α and distinct elements x, y of α, ULift.up x and ULift.up y are distinct.
|
ULift.up_bijective
theorem ULift.up_bijective : ∀ {α : Type u}, Function.Bijective ULift.up
The theorem `ULift.up_bijective` states that for any type `α`, the function `ULift.up` is bijective. In other words, it asserts that the function `ULift.up`, which takes a value of some type and lifts it to a value of the same type within the `ULift` type wrapper, is both injective (no two different inputs produce the same output) and surjective (for every possible output there is at least one corresponding input).
More concisely: The `ULift.up` function from type `α` to `ULift α` is a bijective function.
|
ULift.ext
theorem ULift.ext : ∀ {α : Type u} (x y : ULift.{u_1, u} α), x.down = y.down → x = y
This theorem, `ULift.ext`, states that for any type `α`, given two objects `x` and `y` of the type `ULift α`, if the `down` property of `x` is equal to the `down` property of `y`, then `x` is equal to `y`. The `down` property of a `ULift` object is a value of type `α` that the `ULift` object encapsulates. Essentially, this theorem is asserting that `ULift` objects are uniquely determined by their encapsulated values.
More concisely: If two objects `x` and `y` of type `ULift α` have equal `down` values, then `x` is equal to `y`.
|
PLift.up_surjective
theorem PLift.up_surjective : ∀ {α : Sort u}, Function.Surjective PLift.up
This theorem states that for any type `α`, the function `PLift.up` is surjective. In mathematical terms, this means that for any value `b` of the type `PLift α` (which can be described as a type that contains a single element of type `α`), there exists a value `a` of type `α` such that `PLift.up a` equals `b`. In other words, every value of the lifted type `PLift α` can be obtained by lifting some value from the original type `α`.
More concisely: For any type `α`, the function `PLift.up` is a surjection from `α` to `PLift α`.
|