Built with
doc-gen4, running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑Ctrl+↓to navigate,
Ctrl+🖱️to focus.
On Mac, use
Cmdinstead of
Ctrl.
/-
Copyright (c) 2021 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
! This file was ported from Lean 3 source module data.ulift
! leanprover-community/mathlib commit 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Equiv.Basic
/-!
# 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`.
-/
universe u v
open Function
namespace PLift
variable {α : Sort u} {β : Sort v}
instance [Subsingleton α] : Subsingleton (PLift α) :=
Equiv.plift.subsingleton
instance [Nonempty α] : Nonempty (PLift α) :=
Equiv.plift.nonempty
instance [Unique α] : Unique (PLift α) :=
Equiv.plift.unique
instance [DecidableEq: Sort ?u.212 → Sort (max1?u.212)
DecidableEq: Sort ?u.221 → Sort (max1?u.221)
Injective: {α : Sort ?u.477} → {β : Sort ?u.476} → (α → β) → Prop
symm: {α : Sort ?u.488} → {β : Sort ?u.487} → α ≃ β → β ≃ α
Surjective: {α : Sort ?u.516} → {β : Sort ?u.515} → (α → β) → Prop
symm: {α : Sort ?u.528} → {β : Sort ?u.527} → α ≃ β → β ≃ α
Bijective: {α : Sort ?u.555} → {β : Sort ?u.554} → (α → β) → Prop
symm: {α : Sort ?u.566} → {β : Sort ?u.565} → α ≃ β → β ≃ α
up_inj: ∀ {α : Sort u} {x y : α}, { down := x } = { down := y } ↔ x = y
eq_iff: ∀ {α : Sort ?u.608} {β : Sort ?u.609} {f : α → β}, Injective f → ∀ {a b : α}, f a = f b ↔ a = b
PLift.up_inj: ∀ {α : Sort u} {x y : α}, { down := x } = { down := y } ↔ x = y
Surjective: {α : Sort ?u.664} → {β : Sort ?u.663} → (α → β) → Prop
Bijective: {α : Sort ?u.700} → {β : Sort ?u.699} → (α → β) → Prop
«forall»: ∀ {α : Sort u} {p : PLift α → Prop}, (∀ (x : PLift α), p x) ↔ ∀ (x : α), p { down := x }
forall: ∀ {α : Sort ?u.753} {β : Sort ?u.754} {f : α → β},
Surjective f → ∀ {p : β → Prop}, (∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
PLift.forall: ∀ {α : Sort u} {p : PLift α → Prop}, (∀ (x : PLift α), p x) ↔ ∀ (x : α), p { down := x }
«exists»: ∀ {α : Sort u} {p : PLift α → Prop}, (∃ x, p x) ↔ ∃ x, p { down := x }
exists: ∀ {α : Sort ?u.822} {β : Sort ?u.823} {f : α → β}, Surjective f → ∀ {p : β → Prop}, (∃ y, p y) ↔ ∃ x, p (f x)
PLift.exists: ∀ {α : Sort u} {p : PLift α → Prop}, (∃ x, p x) ↔ ∃ x, p { down := x }
ULift: Type ?u.881 → Type (max?u.881?u.882)
ULift: Type ?u.951 → Type (max?u.951?u.952)
Unique: Sort ?u.1018 → Sort (max1?u.1018)
Unique: Sort ?u.1021 → Sort (max1?u.1021)
ULift: Type ?u.1022 → Type (max?u.1022?u.1023)
DecidableEq: Sort ?u.1091 → Sort (max1?u.1091)
DecidableEq: Sort ?u.1100 → Sort (max1?u.1100)
ULift: Type ?u.1101 → Type (max?u.1101?u.1102)
ULift: Type ?u.1298 → Type (max?u.1298?u.1299)
Injective: {α : Sort ?u.1363} → {β : Sort ?u.1362} → (α → β) → Prop
symm: {α : Sort ?u.1376} → {β : Sort ?u.1375} → α ≃ β → β ≃ α
Surjective: {α : Sort ?u.1406} → {β : Sort ?u.1405} → (α → β) → Prop
symm: {α : Sort ?u.1420} → {β : Sort ?u.1419} → α ≃ β → β ≃ α
Bijective: {α : Sort ?u.1449} → {β : Sort ?u.1448} → (α → β) → Prop
symm: {α : Sort ?u.1462} → {β : Sort ?u.1461} → α ≃ β → β ≃ α
up_inj: ∀ {α : Type u} {x y : α}, { down := x } = { down := y } ↔ x = y
eq_iff: ∀ {α : Sort ?u.1529} {β : Sort ?u.1530} {f : α → β}, Injective f → ∀ {a b : α}, f a = f b ↔ a = b
ULift.up_inj: ∀ {α : Type u} {x y : α}, { down := x } = { down := y } ↔ x = y
Surjective: {α : Sort ?u.1586} → {β : Sort ?u.1585} → (α → β) → Prop
Bijective: {α : Sort ?u.1625} → {β : Sort ?u.1624} → (α → β) → Prop
«forall»: ∀ {α : Type u} {p : ULift α → Prop}, (∀ (x : ULift α), p x) ↔ ∀ (x : α), p { down := x }
ULift: Type ?u.1661 → Type (max?u.1661?u.1662)
forall: ∀ {α : Sort ?u.1685} {β : Sort ?u.1686} {f : α → β},
Surjective f → ∀ {p : β → Prop}, (∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
ULift.forall: ∀ {α : Type u} {p : ULift α → Prop}, (∀ (x : ULift α), p x) ↔ ∀ (x : α), p { down := x }
«exists»: ∀ {α : Type u} {p : ULift α → Prop}, (∃ x, p x) ↔ ∃ x, p { down := x }
ULift: Type ?u.1731 → Type (max?u.1731?u.1732)
exists: ∀ {α : Sort ?u.1759} {β : Sort ?u.1760} {f : α → β}, Surjective f → ∀ {p : β → Prop}, (∃ y, p y) ↔ ∃ x, p (f x)
ULift.exists: ∀ {α : Type u} {p : ULift α → Prop}, (∃ x, p x) ↔ ∃ x, p { down := x }
ext: ∀ (x y : ULift α), x.down = y.down → x = y
ULift: Type ?u.1815 → Type (max?u.1815?u.1816)
congrArg: ∀ {α : Sort ?u.1859} {β : Sort ?u.1858} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
ULift.ext: ∀ {α : Type u} (x y : ULift α), x.down = y.down → x = y
ext_iff: ∀ {α : Type u_1} (x y : ULift α), x = y ↔ x.down = y.down
ULift: Type ?u.1894 → Type (max?u.1894?u.1895)
congrArg: ∀ {α : Sort ?u.1947} {β : Sort ?u.1946} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
ULift.ext: ∀ {α : Type ?u.1963} (x y : ULift α), x.down = y.down → x = y
ULift.ext_iff: ∀ {α : Type u_1} (x y : ULift α), x = y ↔ x.down = y.down