Documentation

Mathlib.Logic.Function.ULift

ULift and PLift #

theorem ULift.down_injective {α : Type u_1} :
@[simp]
theorem ULift.down_inj {α : Type u_1} {a : ULift.{u_2, u_1} α} {b : ULift.{u_2, u_1} α} :
a.down = b.down a = b
theorem PLift.down_injective {α : Sort u_1} :
@[simp]
theorem PLift.down_inj {α : Sort u_1} {a : PLift α} {b : PLift α} :
a.down = b.down a = b