Mathlib.Data.ULift

PLift.instSubsingleton_mathlib instance

[Subsingleton α] : Subsingleton (PLift α)

Full source

instance [Subsingleton α] : Subsingleton (PLift α) :=
  Equiv.plift.subsingleton

Subsingleton Property of PLift

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements of $\alpha$ are equal), the lifted type $\mathrm{PLift}\,\alpha$ is also a subsingleton.

PLift.instNonempty_mathlib instance

[Nonempty α] : Nonempty (PLift α)

Full source

instance [Nonempty α] : Nonempty (PLift α) :=
  Equiv.plift.nonempty

Nonempty Preservation in PLift

Informal description

For any nonempty type $\alpha$, the lifted type $\mathrm{PLift}\,\alpha$ is also nonempty.

PLift.instUnique instance

[Unique α] : Unique (PLift α)

Full source

instance [Unique α] : Unique (PLift α) :=
  Equiv.plift.unique

Uniqueness Preservation in PLift

Informal description

For any type $\alpha$ with a unique element, the lifted type $\mathrm{PLift}\,\alpha$ also has a unique element.

PLift.instDecidableEq_mathlib instance

[DecidableEq α] : DecidableEq (PLift α)

Full source

instance [DecidableEq α] : DecidableEq (PLift α) :=
  Equiv.plift.decidableEq

Decidable Equality Preservation in PLift

Informal description

For any type $\alpha$ with decidable equality, the lifted type $\mathrm{PLift}\,\alpha$ also has decidable equality.

PLift.instIsEmpty instance

[IsEmpty α] : IsEmpty (PLift α)

Full source

instance [IsEmpty α] : IsEmpty (PLift α) :=
  Equiv.plift.isEmpty

Emptiness of PLift for Empty Types

Informal description

For any type $\alpha$, if $\alpha$ is empty, then the lifted type $\mathrm{PLift}\,\alpha$ is also empty.

PLift.up_injective theorem

: Injective (@up α)

Full source

theorem up_injective : Injective (@up α) :=
  Equiv.plift.symm.injective

Injectivity of the PLift.up Function

Informal description

The function $\mathrm{up} : \alpha \to \mathrm{PLift}\,\alpha$ is injective, meaning that for any $x, y \in \alpha$, if $\mathrm{up}\,x = \mathrm{up}\,y$, then $x = y$.

PLift.up_surjective theorem

: Surjective (@up α)

Full source

theorem up_surjective : Surjective (@up α) :=
  Equiv.plift.symm.surjective

Surjectivity of the PLift.up Function

Informal description

The function $\mathrm{up} : \alpha \to \mathrm{PLift}\,\alpha$ is surjective, meaning that for every element $y$ in $\mathrm{PLift}\,\alpha$, there exists an element $x$ in $\alpha$ such that $\mathrm{up}\,x = y$.

PLift.up_bijective theorem

: Bijective (@up α)

Full source

theorem up_bijective : Bijective (@up α) :=
  Equiv.plift.symm.bijective

Bijectivity of the PLift.up Function

Informal description

The function $\mathrm{up} : \alpha \to \mathrm{PLift}\,\alpha$ is bijective, meaning it is both injective and surjective. That is: 1. For any $x, y \in \alpha$, if $\mathrm{up}\,x = \mathrm{up}\,y$, then $x = y$. 2. For every $y \in \mathrm{PLift}\,\alpha$, there exists $x \in \alpha$ such that $\mathrm{up}\,x = y$.

PLift.up_inj theorem

{x y : α} : up x = up y ↔ x = y

Full source

theorem up_inj {x y : α} : upup x = up y ↔ x = y := by simp

Injectivity of the PLift.up Function: $\mathrm{up}\,x = \mathrm{up}\,y \leftrightarrow x = y$

Informal description

For any elements $x$ and $y$ of type $\alpha$, the lifted elements $\mathrm{up}\,x$ and $\mathrm{up}\,y$ are equal if and only if $x = y$.

PLift.down_surjective theorem

: Surjective (@down α)

Full source

theorem down_surjective : Surjective (@down α) :=
  Equiv.plift.surjective

Surjectivity of the $\mathrm{PLift.down}$ Function

Informal description

The function $\mathrm{down} : \mathrm{PLift}\,\alpha \to \alpha$ is surjective, meaning for every element $x \in \alpha$, there exists an element $y \in \mathrm{PLift}\,\alpha$ such that $\mathrm{down}\,y = x$.

PLift.down_bijective theorem

: Bijective (@down α)

Full source

theorem down_bijective : Bijective (@down α) :=
  Equiv.plift.bijective

Bijectivity of the $\mathrm{PLift.down}$ Function

Informal description

The function $\mathrm{down} : \mathrm{PLift}\,\alpha \to \alpha$ is bijective, meaning it is both injective (if $\mathrm{down}\,x = \mathrm{down}\,y$ then $x = y$) and surjective (for every $a \in \alpha$, there exists $b \in \mathrm{PLift}\,\alpha$ such that $\mathrm{down}\,b = a$).

PLift.forall theorem

{p : PLift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (PLift.up x)

Full source

theorem «forall» {p : PLift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (PLift.up x) :=
  up_surjective.forall

Universal Quantifier Transfer for PLift

Informal description

For any predicate $p$ on $\mathrm{PLift}\,\alpha$, the universal quantification $(\forall x \in \mathrm{PLift}\,\alpha, p(x))$ holds if and only if $(\forall x \in \alpha, p(\mathrm{up}\,x))$ holds.

PLift.exists theorem

{p : PLift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (PLift.up x)

Full source

@[simp]
theorem «exists» {p : PLift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (PLift.up x) :=
  up_surjective.exists

Existence Transfer via PLift.up

Informal description

For any predicate $p$ on $\mathrm{PLift}\,\alpha$, there exists an element $x$ in $\mathrm{PLift}\,\alpha$ satisfying $p(x)$ if and only if there exists an element $y$ in $\alpha$ such that $p(\mathrm{up}\,y)$ holds.

PLift.map_injective theorem

: Injective (PLift.map f) ↔ Injective f

Full source

@[simp] lemma map_injective : InjectiveInjective (PLift.map f) ↔ Injective f :=
  (Injective.of_comp_iff' _ down_bijective).trans <| up_injective.of_comp_iff _

Injectivity of $\mathrm{PLift.map}\,f$ $\leftrightarrow$ Injectivity of $f$

Informal description

For any function $f \colon \alpha \to \beta$, the lifted function $\mathrm{PLift.map}\,f \colon \mathrm{PLift}\,\alpha \to \mathrm{PLift}\,\beta$ is injective if and only if $f$ is injective.

PLift.map_surjective theorem

: Surjective (PLift.map f) ↔ Surjective f

Full source

@[simp] lemma map_surjective : SurjectiveSurjective (PLift.map f) ↔ Surjective f :=
  (down_surjective.of_comp_iff _).trans <| Surjective.of_comp_iff' up_bijective _

Surjectivity Preservation under PLift Mapping

Informal description

For any function $f \colon \alpha \to \beta$, the lifted function $\mathrm{PLift.map}\,f \colon \mathrm{PLift}\,\alpha \to \mathrm{PLift}\,\beta$ is surjective if and only if $f$ is surjective.

PLift.map_bijective theorem

: Bijective (PLift.map f) ↔ Bijective f

Full source

@[simp] lemma map_bijective : BijectiveBijective (PLift.map f) ↔ Bijective f :=
  (down_bijective.of_comp_iff _).trans <| Bijective.of_comp_iff' up_bijective _

Bijectivity of PLift.map $f$ $\leftrightarrow$ Bijectivity of $f$

Informal description

For any function $f : \alpha \to \beta$, the lifted function $\mathrm{PLift.map}\,f : \mathrm{PLift}\,\alpha \to \mathrm{PLift}\,\beta$ is bijective if and only if $f$ is bijective.

ULift.instSubsingleton_mathlib instance

[Subsingleton α] : Subsingleton (ULift α)

Full source

instance [Subsingleton α] : Subsingleton (ULift α) :=
  Equiv.ulift.subsingleton

Subsingleton Property Preservation under ULift

Informal description

For any subsingleton type $\alpha$ (i.e., a type with at most one element), the lifted type $\text{ULift}\,\alpha$ is also a subsingleton.

ULift.instNonempty_mathlib instance

[Nonempty α] : Nonempty (ULift α)

Full source

instance [Nonempty α] : Nonempty (ULift α) :=
  Equiv.ulift.nonempty

Nonempty Preservation under ULift

Informal description

For any nonempty type $\alpha$, the lifted type $\text{ULift}\,\alpha$ is also nonempty.

ULift.instUnique instance

[Unique α] : Unique (ULift α)

Full source

instance [Unique α] : Unique (ULift α) :=
  Equiv.ulift.unique

Uniqueness Preservation under ULift

Informal description

For any type $\alpha$ with a unique element, the lifted type $\text{ULift}\,\alpha$ also has a unique element.

ULift.instDecidableEq_mathlib instance

[DecidableEq α] : DecidableEq (ULift α)

Full source

instance [DecidableEq α] : DecidableEq (ULift α) :=
  Equiv.ulift.decidableEq

Decidable Equality Preservation under ULift

Informal description

For any type $\alpha$ with decidable equality, the lifted type $\mathrm{ULift}\,\alpha$ also has decidable equality.

ULift.instIsEmpty instance

[IsEmpty α] : IsEmpty (ULift α)

Full source

instance [IsEmpty α] : IsEmpty (ULift α) :=
  Equiv.ulift.isEmpty

Emptiness Preservation under ULift

Informal description

For any type $\alpha$ that is empty, the lifted type $\mathrm{ULift}\,\alpha$ is also empty.

ULift.up_injective theorem

: Injective (@up α)

Full source

theorem up_injective : Injective (@up α) :=
  Equiv.ulift.symm.injective

Injectivity of the Lifting Operation: $\mathrm{up} : \alpha \to \mathrm{ULift}\,\alpha$

Informal description

The lifting function $\mathrm{up} : \alpha \to \mathrm{ULift}\,\alpha$ is injective, meaning that for any $x_1, x_2 \in \alpha$, if $\mathrm{up}\,x_1 = \mathrm{up}\,x_2$, then $x_1 = x_2$.

ULift.up_surjective theorem

: Surjective (@up α)

Full source

theorem up_surjective : Surjective (@up α) :=
  Equiv.ulift.symm.surjective

Surjectivity of the Lifting Operation: $\mathrm{up} : \alpha \to \mathrm{ULift}\,\alpha$

Informal description

The lifting function $\mathrm{up} : \alpha \to \mathrm{ULift}\,\alpha$ is surjective, meaning that for every element $y$ in $\mathrm{ULift}\,\alpha$, there exists an element $x$ in $\alpha$ such that $\mathrm{up}\,x = y$.

ULift.up_bijective theorem

: Bijective (@up α)

Full source

theorem up_bijective : Bijective (@up α) :=
  Equiv.ulift.symm.bijective

Bijectivity of the Lifting Operation $\mathrm{up} : \alpha \to \mathrm{ULift}\,\alpha$

Informal description

The lifting function $\mathrm{up} : \alpha \to \mathrm{ULift}\,\alpha$ is bijective, meaning it is both injective and surjective. That is: 1. For any $x_1, x_2 \in \alpha$, if $\mathrm{up}\,x_1 = \mathrm{up}\,x_2$, then $x_1 = x_2$ (injectivity). 2. For every $y \in \mathrm{ULift}\,\alpha$, there exists $x \in \alpha$ such that $\mathrm{up}\,x = y$ (surjectivity).

ULift.up_inj theorem

{x y : α} : up x = up y ↔ x = y

Full source

theorem up_inj {x y : α} : upup x = up y ↔ x = y := by simp

Injectivity of the Lifting Operation: $\mathrm{up}\,x = \mathrm{up}\,y \leftrightarrow x = y$

Informal description

For any elements $x$ and $y$ of type $\alpha$, the lifted elements $\mathrm{up}\,x$ and $\mathrm{up}\,y$ are equal if and only if $x = y$.

ULift.down_surjective theorem

: Surjective (@down α)

Full source

theorem down_surjective : Surjective (@down α) :=
  Equiv.ulift.surjective

Surjectivity of the `down` Function on `ULift`

Informal description

The function $\mathrm{down} : \mathrm{ULift}\,\alpha \to \alpha$ is surjective, meaning for every element $x \in \alpha$, there exists an element $y \in \mathrm{ULift}\,\alpha$ such that $\mathrm{down}\,y = x$.

ULift.down_bijective theorem

: Bijective (@down α)

Full source

theorem down_bijective : Bijective (@down α) :=
  Equiv.ulift.bijective

Bijectivity of the `down` Function on `ULift`

Informal description

The function $\mathrm{down} : \mathrm{ULift}\,\alpha \to \alpha$ is bijective, meaning it is both injective (if $\mathrm{down}\,x = \mathrm{down}\,y$ then $x = y$) and surjective (for every $a \in \alpha$, there exists $b \in \mathrm{ULift}\,\alpha$ such that $\mathrm{down}\,b = a$).

ULift.forall theorem

{p : ULift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (ULift.up x)

Full source

@[simp]
theorem «forall» {p : ULift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (ULift.up x) :=
  up_surjective.forall

Universal Quantifier Equivalence for $\mathrm{ULift}$: $(\forall x \in \mathrm{ULift}\,\alpha, p(x)) \leftrightarrow (\forall x \in \alpha, p(\mathrm{up}\,x))$

Informal description

For any predicate $p$ on $\mathrm{ULift}\,\alpha$, the universal quantification $(\forall x \in \mathrm{ULift}\,\alpha, p(x))$ holds if and only if $(\forall x \in \alpha, p(\mathrm{up}\,x))$ holds.

ULift.exists theorem

{p : ULift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (ULift.up x)

Full source

@[simp]
theorem «exists» {p : ULift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (ULift.up x) :=
  up_surjective.exists

Existence Transfer via Lifting: $(\exists x \in \mathrm{ULift}\,\alpha, p(x)) \leftrightarrow (\exists y \in \alpha, p(\mathrm{up}\,y))$

Informal description

For any predicate $p$ on the lifted type $\mathrm{ULift}\,\alpha$, there exists an element $x$ in $\mathrm{ULift}\,\alpha$ satisfying $p(x)$ if and only if there exists an element $y$ in $\alpha$ such that $p(\mathrm{up}\,y)$ holds.

ULift.map_injective theorem

: Injective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Injective f

Full source

@[simp] lemma map_injective : InjectiveInjective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Injective f :=
  (Injective.of_comp_iff' _ down_bijective).trans <| up_injective.of_comp_iff _

Injectivity of Lifted Function: $\mathrm{ULift.map}\,f$ injective $\leftrightarrow$ $f$ injective

Informal description

For any function $f \colon \alpha \to \beta$, the lifted function $\mathrm{ULift.map}\,f \colon \mathrm{ULift}\,\alpha \to \mathrm{ULift}\,\beta$ is injective if and only if $f$ is injective.

ULift.map_surjective theorem

: Surjective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Surjective f

Full source

@[simp] lemma map_surjective :
    SurjectiveSurjective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Surjective f :=
  (down_surjective.of_comp_iff _).trans <| Surjective.of_comp_iff' up_bijective _

Surjectivity of Lifted Function $\mathrm{ULift.map}\,f$ is Equivalent to Surjectivity of $f$

Informal description

For any function $f \colon \alpha \to \beta$, the lifted function $\mathrm{ULift.map}\,f \colon \mathrm{ULift}\,\alpha \to \mathrm{ULift}\,\beta$ is surjective if and only if $f$ is surjective.

ULift.map_bijective theorem

: Bijective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Bijective f

Full source

@[simp] lemma map_bijective : BijectiveBijective (ULift.map f : ULift.{u'} α → ULift.{v'} β) ↔ Bijective f :=
  (down_bijective.of_comp_iff _).trans <| Bijective.of_comp_iff' up_bijective _

Bijectivity of Lifted Function: $\mathrm{ULift.map}\,f$ bijective $\leftrightarrow$ $f$ bijective

Informal description

For any function $f \colon \alpha \to \beta$, the lifted function $\mathrm{ULift.map}\,f \colon \mathrm{ULift}\,\alpha \to \mathrm{ULift}\,\beta$ is bijective if and only if $f$ is bijective.

ULift.ext theorem

(x y : ULift α) (h : x.down = y.down) : x = y

Full source

@[ext]
theorem ext (x y : ULift α) (h : x.down = y.down) : x = y :=
  congrArg up h

Extensionality for ULift: $x.\mathrm{down} = y.\mathrm{down} \Rightarrow x = y$

Informal description

For any two elements $x, y$ of the lifted type $\mathrm{ULift}\,\alpha$, if their underlying values are equal (i.e., $x.\mathrm{down} = y.\mathrm{down}$), then $x = y$.

ULift.rec_update theorem

 {β : ULift α → Type*} [DecidableEq α] (f : ∀ a, β (.up a)) (a : α) (x : β (.up a)) :
  ULift.rec (update f a x) = update (ULift.rec f) (.up a) x

Full source

@[simp]
lemma rec_update {β : ULift α → Type*} [DecidableEq α]
    (f : ∀ a, β (.up a)) (a : α) (x : β (.up a)) :
    ULift.rec (update f a x) = update (ULift.rec f) (.up a) x :=
  Function.rec_update up_injective (ULift.rec ·) (fun _ _ => rfl) (fun
    | _, _, .up _, h => (h _ rfl).elim) _ _ _

Recursor Commutation with Function Update for $\mathrm{ULift}$

Informal description

Let $\alpha$ be a type with decidable equality, and let $\beta : \mathrm{ULift}\,\alpha \to \text{Type}$ be a type family. For any function $f : \forall a : \alpha, \beta (\mathrm{up}\,a)$, any $a : \alpha$, and any $x : \beta (\mathrm{up}\,a)$, the following equality holds: \[ \mathrm{ULift.rec}\,(\text{update}\,f\,a\,x) = \text{update}\,(\mathrm{ULift.rec}\,f)\,(\mathrm{up}\,a)\,x \] Here, $\mathrm{ULift.rec}$ is the recursor for $\mathrm{ULift}$, and $\text{update}$ is the function update operation.