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
.
Equations
@[simp]
@[simp]
@[simp]
Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[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