ExistsUnique

This file defines the ExistsUnique predicate, notated as ∃!, and proves some of its basic properties.

def ExistsUnique {α : Sort u_1} (p : α → Prop) : Prop

For p : α → Prop, ExistsUnique p means that there exists a unique x : α with p x.

Equations

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

def Mathlib.Notation.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 Mathlib.Notation.«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 Mathlib.Notation.unexpandExistsUnique : Lean.PrettyPrinter.Unexpander

Pretty-printing for ExistsUnique, following the same pattern as pretty printing for Exists. However, it does not merge binders.

Equations

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

def Mathlib.Notation.«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.

theorem ExistsUnique.intro {α : Sort u_1} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p y → y = w) : ∃! x : α, p x

theorem ExistsUnique.elim {α : Sort u_1} {p : α → Prop} {b : Prop} (h₂ : ∃! x : α, p x) (h₁ : ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b) : b

theorem exists_unique_of_exists_of_unique {α : Sort u_1} {p : α → Prop} (hex : ∃ (x : α), p x) (hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x : α, p x

theorem ExistsUnique.exists {α : Sort u_1} {p : α → Prop} : (∃! x : α, p x) → ∃ (x : α), p x

theorem ExistsUnique.unique {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂

theorem existsUnique_congr {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a ↔ q a) : (∃! a : α, p a) ↔ ∃! a : α, q a

@[simp]

theorem exists_unique_iff_exists {α : Sort u_1} [Subsingleton α] {p : α → Prop} : (∃! x : α, p x) ↔ ∃ (x : α), p x

theorem exists_unique_const {b : Prop} (α : Sort u_2) [i : Nonempty α] [Subsingleton α] : (∃! x : α, b) ↔ b

@[simp]

theorem exists_unique_eq {α : Sort u_1} {a' : α} : ∃! a : α, a = a'

@[simp]

theorem exists_unique_eq' {α : Sort u_1} {a' : α} : ∃! a : α, a' = a

theorem exists_unique_prop {p q : Prop} : (∃! x : p, q) ↔ p ∧ q

@[simp]

theorem exists_unique_false {α : Sort u_1} : ¬∃! x : α, False

theorem exists_unique_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃! h' : p, q h') ↔ q h

theorem ExistsUnique.elim₂ {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} {b : Prop} (h₂ : ∃! x : α, ∃! h : p x, q x h) (h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b) : b

theorem ExistsUnique.intro₂ {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} (w : α) (hp : p w) (hq : q w hp) (H : ∀ (y : α) (hy : p y), q y hy → y = w) : ∃! x : α, ∃! hx : p x, q x hx

theorem ExistsUnique.exists₂ {α : Sort u_1} {p : α → Sort u_2} {q : (x : α) → p x → Prop} (h : ∃! x : α, ∃! hx : p x, q x hx) : ∃ (x : α), ∃ (hx : p x), q x hx

theorem ExistsUnique.unique₂ {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} (h : ∃! x : α, ∃! hx : p x, q x hx) {y₁ y₂ : α} (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) : y₁ = y₂