theorem imp_iff_not_imp_not {p q : Prop} : p → q ↔ ¬q → ¬p

Any implication is equivalent to its converse.

theorem func_subsingleton_iff_to_empty {α : Type u} {β : Type v} (h : α → Empty) : Subsingleton (α → β)

@[simp]

theorem eq_rec_self {α : Sort u} {x : α → Sort u} {a : α} {h : a = a} {h' : x a} : h ▸ h' = h'

transporting a proof along a path with the same basepoints doesnt yield anything new

@[simp]

theorem eq_rec_symm_self {α : Sort u} {x : α → Sort u} {a : α} {h : a = a} {h' : x a} : ⋯ ▸ h' = h'

transporting a proof along a path with the same basepoints in reverse doesnt yield anything new

class Unique (α : Sort u) extends Inhabited α : Sort (max 1 u)

• default : α
• uniq : ∀ (a : α), a = default

  In a Unique type, every term is equal to the default element (from Inhabited).

theorem Unique.ext {α : Sort u} {x y : Unique α} (default : default = default) : x = y

instance PUnit.unique : Unique PUnit

Equations

• PUnit.unique = { default := PUnit.unit, uniq := PUnit.unique.proof_1 }

@[simp]

theorem PUnit.default_eq_unit : default = PUnit.unit

def uniqueProp {p : Prop} (h : p) : Unique p

Every provable proposition is unique, as all proofs are equal.

Equations

• uniqueProp h = { default := h, uniq := ⋯ }

instance instUniqueTrue : Unique True

True has a unique term.

Equations

• instUniqueTrue = uniqueProp trivial

@[instance 100]

instance Unique.instInhabited {α : Sort u} [Unique α] : Inhabited α

Equations

• Unique.instInhabited = inst.toInhabited

theorem Unique.eq_default {α : Sort u} [Unique α] (a : α) : a = default

theorem Unique.default_eq {α : Sort u} [Unique α] (a : α) : default = a

@[instance 100]

instance Unique.instSubsingleton {α : Sort u} [Unique α] : Subsingleton α

Equations

• ⋯ = ⋯

theorem Unique.forall_iff {α : Sort u} [Unique α] {p : α → Prop} : (∀ (a : α), p a) ↔ p default

theorem Unique.exists_iff {α : Sort u} [Unique α] {p : α → Prop} : Exists p ↔ p default

def Unique.ExistsUnique {α : Type u} (p : α → Prop) : Prop

Equations

• Unique.ExistsUnique p = ∃ (x : α), p x ∧ ∀ (y : α), p y → y = x

def Unique.isExplicitBinderSingular (xs : Lean.TSyntax `Lean.explicitBinders) : Bool

Checks to see that xs has only one binder.

Equations

• One or more equations did not get rendered due to their size.

def Unique.«term∃!_,_» : Lean.ParserDescr

∃! x : α, p x means that there exists a unique x in α such that p x. This is notation for ExistsUnique (fun (x : α) ↦ p x).

This notation does not allow multiple binders like ∃! (x : α) (y : β), p x y as a shorthand for ∃! (x : α), ∃! (y : β), p x y since it is liable to be misunderstood. Often, the intended meaning is instead ∃! q : α × β, p q.1 q.2.

Equations

• One or more equations did not get rendered due to their size.

def Unique.unexpandExistsUnique : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Unique.«term∃!__,_» : Lean.ParserDescr

∃! x ∈ s, p x means ∃! x, x ∈ s ∧ p x, which is to say that there exists a unique x ∈ s such that p x. Similarly, notations such as ∃! x ≤ n, p n are supported, using any relation defined using the binder_predicate command.

Equations

• One or more equations did not get rendered due to their size.