data.ulift

# Extra lemmas about ulift and plift#

In this file we provide subsingleton, unique, decidable_eq, and is_empty instances for ulift α and plift α. We also prove ulift.forall, ulift.exists, plift.forall, and plift.exists.

@[protected, instance]
def plift.subsingleton {α : Sort u} [subsingleton α] :
@[protected, instance]
def plift.unique {α : Sort u} [unique α] :
Equations
@[protected, instance]
def plift.decidable_eq {α : Sort u} [decidable_eq α] :
Equations
@[protected, instance]
def plift.is_empty {α : Sort u} [is_empty α] :
@[simp]
theorem plift.forall {α : Sort u} {p : → Prop} :
(∀ (x : plift α), p x) ∀ (x : α), p {down := x}
@[simp]
theorem plift.exists {α : Sort u} {p : → Prop} :
(∃ (x : plift α), p x) ∃ (x : α), p {down := x}
@[protected, instance]
def ulift.subsingleton {α : Type u} [subsingleton α] :
@[protected, instance]
def ulift.unique {α : Type u} [unique α] :
Equations
@[protected, instance]
def ulift.decidable_eq {α : Type u} [decidable_eq α] :
Equations
@[protected, instance]
def ulift.is_empty {α : Type u} [is_empty α] :
@[simp]
theorem ulift.forall {α : Type u} {p : → Prop} :
(∀ (x : ulift α), p x) ∀ (x : α), p {down := x}
@[simp]
theorem ulift.exists {α : Type u} {p : → Prop} :
(∃ (x : ulift α), p x) ∃ (x : α), p {down := x}