Opposite.op_unop
theorem Opposite.op_unop : ∀ {α : Sort u} (x : αᵒᵖ), Opposite.op x.unop = x
The theorem `Opposite.op_unop` asserts that for any type `α` and any element `x` of the opposite type `αᵒᵖ`, applying the function `Opposite.op` to the `unop` of `x` (i.e., the original element in `α` from which `x` was derived) will yield `x` itself. In simpler terms, this theorem states that 'unopping' an opposite element and then 'opping' it again brings us back to the original opposite element.
More concisely: For any type `α` and its opposite `αᵒᵖ,` applying the opposite operation twice to an element `x` of `αᵒᵖ` yields the original element `x.` In Lean notation, `Opposite.op (Opposite.unop x) = x.`
|
Opposite.unop_injective
theorem Opposite.unop_injective : ∀ {α : Sort u}, Function.Injective Opposite.unop
The theorem `Opposite.unop_injective` asserts that, for any type `α` (which can be a type or a sort in Lean), the canonical map `unop` from the opposite type `αᵒᵖ` to `α` is injective. In other words, if two elements from the opposite type `αᵒᵖ` have the same image under the `unop` function, then these two elements must be the same. This ensures the uniqueness of the `unop` function's preimage.
More concisely: The `unop` function from the opposite type `αᵒᵖ` to `α` in Lean is an injection.
|
Opposite.op_injective
theorem Opposite.op_injective : ∀ {α : Sort u}, Function.Injective Opposite.op
The theorem `Opposite.op_injective` states that for all types or sorts `α`, the function `Opposite.op` is injective. In other words, if we have two elements `a₁` and `a₂` from `α` such that applying the function `Opposite.op` to both `a₁` and `a₂` results in the same output, then `a₁` and `a₂` must be the same. Here, `Opposite.op` is the canonical map that maps an element `x` from a type `α` to the opposite type `αᵒᵖ`, which simply wraps `x` in a structure with a single field `unop`.
More concisely: For all types `α`, if `Opposite.op a₁ = Opposite.op a₂`, then `a₁ = a₂`.
|