Documentation

Mathlib.Data.ULift

Extra lemmas about ULift and PLift #

In this file we provide Subsingleton, Unique, DecidableEq, and isEmpty instances for ULift α and PLift α. We also prove ULift.forall, ULift.exists, PLift.forall, and PLift.exists.

instance PLift.instUniquePLift {α : Sort u} [inst : Unique α] :
Equations
instance PLift.instDecidableEqPLift {α : Sort u} [inst : DecidableEq α] :
Equations
@[simp]
theorem PLift.up_inj {α : Sort u} {x : α} {y : α} :
{ down := x } = { down := y } x = y
@[simp]
theorem PLift.forall {α : Sort u} {p : PLift αProp} :
((x : PLift α) → p x) (x : α) → p { down := x }
@[simp]
theorem PLift.exists {α : Sort u} {p : PLift αProp} :
(x, p x) x, p { down := x }
instance ULift.instUniqueULift {α : Type u} [inst : Unique α] :
Equations
instance ULift.instDecidableEqULift {α : Type u} [inst : DecidableEq α] :
Equations
@[simp]
theorem ULift.up_inj {α : Type u} {x : α} {y : α} :
{ down := x } = { down := y } x = y
@[simp]
theorem ULift.forall {α : Type u} {p : ULift αProp} :
((x : ULift α) → p x) (x : α) → p { down := x }
@[simp]
theorem ULift.exists {α : Type u} {p : ULift αProp} :
(x, p x) x, p { down := x }
theorem ULift.ext {α : Type u} (x : ULift α) (y : ULift α) (h : x.down = y.down) :
x = y
theorem ULift.ext_iff {α : Type u_1} (x : ULift α) (y : ULift α) :
x = y x.down = y.down