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.instUnique {α : Sort u} [Unique α] :
Equations
    instance PLift.instIsEmpty {α : Sort u} [IsEmpty α] :
    theorem PLift.up_inj {α : Sort u} {x y : α} :
    { down := x } = { down := y } x = y
    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 : αβ} :
    @[simp]
    theorem PLift.map_surjective {α : Sort u} {β : Sort v} {f : αβ} :
    @[simp]
    theorem PLift.map_bijective {α : Sort u} {β : Sort v} {f : αβ} :
    instance ULift.instUnique {α : Type u} [Unique α] :
    Equations
      theorem ULift.up_inj {α : Type u} {x y : α} :
      { down := x } = { down := y } x = y
      @[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 : αβ} :
      @[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 : 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