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.instNonempty_mathlib {α : Sort u} [Nonempty α] : Nonempty (PLift α)

@[implicit_reducible]

instance PLift.instUnique {α : Sort u} [Unique α] : Unique (PLift α)

@[implicit_reducible]

instance PLift.instDecidableEq_mathlib {α : Sort u} [DecidableEq α] : DecidableEq (PLift α)

instance PLift.instIsEmpty {α : Sort u} [IsEmpty α] : IsEmpty (PLift α)

theorem PLift.up_injective {α : Sort u} : Function.Injective up

theorem PLift.up_surjective {α : Sort u} : Function.Surjective up

theorem PLift.up_bijective {α : Sort u} : Function.Bijective up

theorem PLift.up_inj {α : Sort u} {x y : α} : { down := x } = { down := y } ↔ x = y

theorem PLift.down_surjective {α : Sort u} : Function.Surjective down

theorem PLift.down_bijective {α : Sort u} : Function.Bijective down

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 : PLift α), p x) ↔ ∃ (x : α), p { down := x }

@[simp]

theorem PLift.map_injective {α : Sort u} {β : Sort v} {f : α → β} : Function.Injective (PLift.map f) ↔ Function.Injective f

@[simp]

theorem PLift.map_surjective {α : Sort u} {β : Sort v} {f : α → β} : Function.Surjective (PLift.map f) ↔ Function.Surjective f

@[simp]

theorem PLift.map_bijective {α : Sort u} {β : Sort v} {f : α → β} : Function.Bijective (PLift.map f) ↔ Function.Bijective f

instance ULift.instNonempty_mathlib {α : Type u} [Nonempty α] : Nonempty (ULift.{u_1, u} α)

@[implicit_reducible]

instance ULift.instUnique {α : Type u} [Unique α] : Unique (ULift.{u_1, u} α)

@[implicit_reducible]

instance ULift.instDecidableEq_mathlib {α : Type u} [DecidableEq α] : DecidableEq (ULift.{u_1, u} α)

instance ULift.instIsEmpty {α : Type u} [IsEmpty α] : IsEmpty (ULift.{u_1, u} α)

theorem ULift.up_injective {α : Type u} : Function.Injective up

theorem ULift.up_surjective {α : Type u} : Function.Surjective up

theorem ULift.up_bijective {α : Type u} : Function.Bijective up

theorem ULift.up_inj {α : Type u} {x y : α} : { down := x } = { down := y } ↔ x = y

theorem ULift.down_surjective {α : Type u} : Function.Surjective down

theorem ULift.down_bijective {α : Type u} : Function.Bijective down

@[simp]

theorem ULift.forall {α : Type u} {p : ULift.{u_1, u} α → Prop} : (∀ (x : ULift.{u_1, u} α), p x) ↔ ∀ (x : α), p { down := x }

@[simp]

theorem ULift.exists {α : Type u} {p : ULift.{u_1, u} α → Prop} : (∃ (x : ULift.{u_1, u} α), p x) ↔ ∃ (x : α), p { down := x }

@[simp]

theorem ULift.map_injective {α : Type u} {β : Type v} {f : α → β} : Function.Injective (ULift.map f) ↔ Function.Injective f

@[simp]

theorem ULift.map_surjective {α : Type u} {β : Type v} {f : α → β} : Function.Surjective (ULift.map f) ↔ Function.Surjective f

@[simp]

theorem ULift.map_bijective {α : Type u} {β : Type v} {f : α → β} : Function.Bijective (ULift.map f) ↔ Function.Bijective f

theorem ULift.ext {α : Type u} (x y : ULift.{u_1, u} α) (h : x.down = y.down) : x = y

theorem ULift.ext_iff {α : Type u} {x y : ULift.{u_1, u} α} : x = y ↔ x.down = y.down

@[simp]

theorem ULift.rec_update {α : Type u} {β : ULift.{u_2, u} α → Type u_1} [DecidableEq α] (f : (a : α) → β { down := a }) (a : α) (x : β { down := a }) : (fun (t : ULift.{u_2, u} α) => rec (Function.update f a x) t) = Function.update (fun (t : ULift.{u_2, u} α) => rec f t) { down := a } x