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.

source
instance PLift.instSubsingleton_mathlib {α : Sort u} [Subsingleton α] :
Subsingleton (PLift α)
Equations
  • ⋯ = ⋯
source
instance PLift.instNonempty_mathlib {α : Sort u} [Nonempty α] :
Nonempty (PLift α)
Equations
  • ⋯ = ⋯
source
instance PLift.instUnique {α : Sort u} [Unique α] :
Unique (PLift α)
Equations
  • PLift.instUnique = Equiv.plift.unique
source
instance PLift.instDecidableEq_mathlib {α : Sort u} [DecidableEq α] :
DecidableEq (PLift α)
Equations
  • PLift.instDecidableEq_mathlib = Equiv.plift.decidableEq
source
instance PLift.instIsEmpty {α : Sort u} [IsEmpty α] :
IsEmpty (PLift α)
Equations
  • ⋯ = ⋯
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
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 : PLift α), p x) ↔ ∃ (x : α), p { down := x }
source
@[simp]
theorem PLift.map_injective {α : Sort u} {β : Sort v} {f : α → β} :
Function.Injective (PLift.map f) ↔ Function.Injective f
source
@[simp]
theorem PLift.map_surjective {α : Sort u} {β : Sort v} {f : α → β} :
Function.Surjective (PLift.map f) ↔ Function.Surjective f
source
@[simp]
theorem PLift.map_bijective {α : Sort u} {β : Sort v} {f : α → β} :
Function.Bijective (PLift.map f) ↔ Function.Bijective f
source
instance ULift.instSubsingleton_mathlib {α : Type u} [Subsingleton α] :
Subsingleton (ULift.{u_1, u} α)
Equations
  • ⋯ = ⋯
source
instance ULift.instNonempty_mathlib {α : Type u} [Nonempty α] :
Nonempty (ULift.{u_1, u} α)
Equations
  • ⋯ = ⋯
source
instance ULift.instUnique {α : Type u} [Unique α] :
Unique (ULift.{u_1, u} α)
Equations
  • ULift.instUnique = Equiv.ulift.unique
source
instance ULift.instDecidableEq_mathlib {α : Type u} [DecidableEq α] :
DecidableEq (ULift.{u_1, u} α)
Equations
  • ULift.instDecidableEq_mathlib = Equiv.ulift.decidableEq
source
instance ULift.instIsEmpty {α : Type u} [IsEmpty α] :
IsEmpty (ULift.{u_1, u} α)
Equations
  • ⋯ = ⋯
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 : ULift.{u_1, u} α), p x) ↔ ∃ (x : α), p { down := x }
source
@[simp]
theorem ULift.map_injective {α : Type u} {β : Type v} {f : α → β} :
Function.Injective (ULift.map f) ↔ Function.Injective f
source
@[simp]
theorem ULift.map_surjective {α : Type u} {β : Type v} {f : α → β} :
Function.Surjective (ULift.map f) ↔ Function.Surjective f
source
@[simp]
theorem ULift.map_bijective {α : Type u} {β : Type v} {f : α → β} :
Function.Bijective (ULift.map f) ↔ Function.Bijective f
source
theorem ULift.ext {α : Type u} (x y : ULift.{u_1, u} α) (h : x.down = y.down) :
x = y