Mathlib.Logic.Function.ULift

ULift.down_injective theorem

{α : Sort _} : Function.Injective (@ULift.down α)

Full source

theorem ULift.down_injective {α : Sort _} : Function.Injective (@ULift.down α)
  | ⟨a⟩, ⟨b⟩, _ => by congr

Injectivity of the `ULift.down` Function

Informal description

For any type `α`, the function `ULift.down` from `ULift α` to `α` is injective. That is, for any `a, b : ULift α`, if `a.down = b.down`, then `a = b`.

ULift.down_inj theorem

{α : Sort _} {a b : ULift α} : a.down = b.down ↔ a = b

Full source

@[simp] theorem ULift.down_inj {α : Sort _} {a b : ULift α} : a.down = b.down ↔ a = b :=
  ⟨fun h ↦ ULift.down_injective h, fun h ↦ by rw [h]⟩

Equality in $\mathrm{ULift}$ via Projection: $a.\mathrm{down} = b.\mathrm{down} \leftrightarrow a = b$

Informal description

For any type $\alpha$ and any elements $a, b$ of type $\mathrm{ULift}\,\alpha$, the equality $a.\mathrm{down} = b.\mathrm{down}$ holds if and only if $a = b$.

PLift.down_injective theorem

: Function.Injective (@PLift.down α)

Full source

theorem PLift.down_injective : Function.Injective (@PLift.down α)
  | ⟨a⟩, ⟨b⟩, _ => by congr

Injectivity of the Projection from `PLift` to its Underlying Type

Informal description

The projection function `PLift.down` from `PLift α` to `α` is injective. That is, for any elements `a, b : PLift α`, if `a.down = b.down`, then `a = b`.

PLift.down_inj theorem

{a b : PLift α} : a.down = b.down ↔ a = b

Full source

@[simp] theorem PLift.down_inj {a b : PLift α} : a.down = b.down ↔ a = b :=
  ⟨fun h ↦ PLift.down_injective h, fun h ↦ by rw [h]⟩

Equality in `PLift` via Projection: $a.down = b.down \leftrightarrow a = b$

Informal description

For any elements $a, b$ of type `PLift α`, the projection `a.down` equals `b.down` if and only if $a = b$.