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.

source

instance PLift.instSubsingletonPLift {α : Sort u} [Subsingleton α] :

Subsingleton (PLift α)

Equations

@PLift.instSubsingletonPLift = @PLift.instSubsingletonPLift.proof_1

source

instance PLift.instNonemptyPLift {α : Sort u} [Nonempty α] :

Nonempty (PLift α)

Equations

@PLift.instNonemptyPLift = @PLift.instNonemptyPLift.proof_1

source

instance PLift.instUniquePLift {α : Sort u} [Unique α] :

Unique (PLift α)

Equations

PLift.instUniquePLift = Equiv.unique Equiv.plift

source

instance PLift.instDecidableEqPLift {α : Sort u} [DecidableEq α] :

DecidableEq (PLift α)

Equations

PLift.instDecidableEqPLift = Equiv.decidableEq Equiv.plift

source

instance PLift.instIsEmptyPLift {α : Sort u} [IsEmpty α] :

IsEmpty (PLift α)

Equations

@PLift.instIsEmptyPLift = @PLift.instIsEmptyPLift.proof_1

source

theorem PLift.up_injective {α : Sort u} :

Function.Injective PLift.up

source

theorem PLift.up_surjective {α : Sort u} :

Function.Surjective PLift.up

source

theorem PLift.up_bijective {α : Sort u} :

Function.Bijective PLift.up

source

@[simp]

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

{ down := x } = { down := y } ↔ x = y

source

theorem PLift.down_surjective {α : Sort u} :

Function.Surjective PLift.down

source

theorem PLift.down_bijective {α : Sort u} :

Function.Bijective PLift.down

source

@[simp]

theorem PLift.forall {α : Sort u} {p : PLift α → Prop} :

((x : PLift α) → p x) ↔ (x : α) → p { down := x }

source

@[simp]

theorem PLift.exists {α : Sort u} {p : PLift α → Prop} :

(∃ x, p x) ↔ ∃ x, p { down := x }

source

instance ULift.instSubsingletonULift {α : Type u} [Subsingleton α] :

Subsingleton (ULift.{u_1, u} α)

Equations

@ULift.instSubsingletonULift = @ULift.instSubsingletonULift.proof_1

source

instance ULift.instNonemptyULift {α : Type u} [Nonempty α] :

Nonempty (ULift.{u_1, u} α)

Equations

@ULift.instNonemptyULift = @ULift.instNonemptyULift.proof_1

source

instance ULift.instUniqueULift {α : Type u} [Unique α] :

Unique (ULift.{u_1, u} α)

Equations

ULift.instUniqueULift = Equiv.unique Equiv.ulift

source

instance ULift.instDecidableEqULift {α : Type u} [DecidableEq α] :

DecidableEq (ULift.{u_1, u} α)

Equations

ULift.instDecidableEqULift = Equiv.decidableEq Equiv.ulift

source

instance ULift.instIsEmptyULift {α : Type u} [IsEmpty α] :

IsEmpty (ULift.{u_1, u} α)

Equations

@ULift.instIsEmptyULift = @ULift.instIsEmptyULift.proof_1

source

theorem ULift.up_injective {α : Type u} :

Function.Injective ULift.up

source

theorem ULift.up_surjective {α : Type u} :

Function.Surjective ULift.up

source

theorem ULift.up_bijective {α : Type u} :

Function.Bijective ULift.up

source

@[simp]

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

{ down := x } = { down := y } ↔ x = y

source

theorem ULift.down_surjective {α : Type u} :

Function.Surjective ULift.down

source

theorem ULift.down_bijective {α : Type u} :

Function.Bijective ULift.down

source

@[simp]

theorem ULift.forall {α : Type u} {p : ULift.{u_1, u} α → Prop} :

((x : ULift.{u_1, u} α) → p x) ↔ (x : α) → p { down := x }

source

@[simp]

theorem ULift.exists {α : Type u} {p : ULift.{u_1, u} α → Prop} :

(∃ x, p x) ↔ ∃ x, p { down := x }

source

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

x = y

source

theorem ULift.ext_iff {α : Type u_1} (x : ULift.{u_2, u_1} α) (y : ULift.{u_2, u_1} α) :

x = y ↔ x.down = y.down

Extra lemmas about ULift and PLift #

Extra lemmas about `ULift` and `PLift` #