mathlib3 documentation

data.ulift

Extra lemmas about ulift and plift #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we provide subsingleton, unique, decidable_eq, and is_empty instances for ulift α and plift α. We also prove ulift.forall, ulift.exists, plift.forall, and plift.exists.

source
@[protected, instance]
def plift.subsingleton {α : Sort u} [subsingleton α] :
subsingleton (plift α)
source
@[protected, instance]
def plift.nonempty {α : Sort u} [nonempty α] :
nonempty (plift α)
source
@[protected, instance]
def plift.unique {α : Sort u} [unique α] :
unique (plift α)
Equations
source
@[protected, instance]
def plift.decidable_eq {α : Sort u} [decidable_eq α] :
decidable_eq (plift α)
Equations
source
@[protected, instance]
def plift.is_empty {α : Sort u} [is_empty α] :
is_empty (plift α)
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 : plift α), p x) ↔ ∃ (x : α), p {down := x}
source
@[protected, instance]
def ulift.subsingleton {α : Type u} [subsingleton α] :
subsingleton (ulift α)
source
@[protected, instance]
def ulift.nonempty {α : Type u} [nonempty α] :
nonempty (ulift α)
source
@[protected, instance]
def ulift.unique {α : Type u} [unique α] :
unique (ulift α)
Equations
source
@[protected, instance]
def ulift.decidable_eq {α : Type u} [decidable_eq α] :
decidable_eq (ulift α)
Equations
source
@[protected, instance]
def ulift.is_empty {α : Type u} [is_empty α] :
is_empty (ulift α)
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 α → Prop} :
(∀ (x : ulift α), p x) ↔ ∀ (x : α), p {down := x}
source
@[simp]
theorem ulift.exists {α : Type u} {p : ulift α → Prop} :
(∃ (x : ulift α), p x) ↔ ∃ (x : α), p {down := x}