# 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.instSubsingleton_mathlib {α : Sort u} [] :
Equations
• =
instance PLift.instNonempty_mathlib {α : Sort u} [] :
Equations
• =
instance PLift.instUnique {α : Sort u} [] :
Equations
• PLift.instUnique = Equiv.plift.unique
Equations
• PLift.instDecidableEq_mathlib = Equiv.plift.decidableEq
instance PLift.instIsEmpty {α : Sort u} [] :
Equations
• =
@[simp]
theorem PLift.up_inj {α : Sort u} {x : α} {y : α} :
{ down := x } = { down := y } x = y
@[simp]
theorem PLift.forall {α : Sort u} {p : Prop} :
(∀ (x : ), p x) ∀ (x : α), p { down := x }
@[simp]
theorem PLift.exists {α : Sort u} {p : Prop} :
(∃ (x : ), p x) ∃ (x : α), p { down := x }
@[simp]
theorem PLift.map_injective {α : Sort u} {β : Sort v} {f : αβ} :
@[simp]
theorem PLift.map_surjective {α : Sort u} {β : Sort v} {f : αβ} :
@[simp]
theorem PLift.map_bijective {α : Sort u} {β : Sort v} {f : αβ} :
Equations
• =
instance ULift.instNonempty_mathlib {α : Type u} [] :
Equations
• =
instance ULift.instUnique {α : Type u} [] :
Equations
• ULift.instUnique = Equiv.ulift.unique
Equations
• ULift.instDecidableEq_mathlib = Equiv.ulift.decidableEq
instance ULift.instIsEmpty {α : Type u} [] :
Equations
• =
@[simp]
theorem ULift.up_inj {α : Type u} {x : α} {y : α} :
{ down := x } = { down := y } x = y
@[simp]
theorem ULift.forall {α : Type u} {p : Prop} :
(∀ (x : ), p x) ∀ (x : α), p { down := x }
@[simp]
theorem ULift.exists {α : Type u} {p : Prop} :
(∃ (x : ), p x) ∃ (x : α), p { down := x }
@[simp]
theorem ULift.map_injective {α : Type u} {β : Type v} {f : αβ} :
@[simp]
theorem ULift.map_surjective {α : Type u} {β : Type v} {f : αβ} :
@[simp]
theorem ULift.map_bijective {α : Type u} {β : Type v} {f : αβ} :
theorem ULift.ext {α : Type u} (x : ) (y : ) (h : x.down = y.down) :
x = y
theorem ULift.ext_iff {α : Type u_1} (x : ) (y : ) :
x = y x.down = y.down