# `ExistsUnique` #

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

source
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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
theorem ExistsUnique.intro {α : Sort u_1} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p y → y = w) :
∃! x : α, p x
source
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
source
theorem existsUnique_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
source
theorem ExistsUnique.exists {α : Sort u_1} {p : α → Prop} :
(∃! x : α, p x) → ∃ (x : α), p x
source
theorem ExistsUnique.unique {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) :
y₁ = y₂
source
theorem existsUnique_congr {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a ↔ q a) :
(∃! a : α, p a) ↔ ∃! a : α, q a
source
@[simp]
theorem existsUnique_iff_exists {α : Sort u_1} [Subsingleton α] {p : α → Prop} :
(∃! x : α, p x) ↔ ∃ (x : α), p x
source
theorem existsUnique_const {b : Prop} (α : Sort u_2) [i : Nonempty α] [Subsingleton α] :
(∃! x : α, b) ↔ b
source
@[simp]
theorem existsUnique_eq {α : Sort u_1} {a' : α} :
∃! a : α, a = a'
source
@[simp]
theorem existsUnique_eq' {α : Sort u_1} {a' : α} :
∃! a : α, a' = a

The difference with `existsUnique_eq` is that the equality is reversed.

source
theorem existsUnique_prop {p q : Prop} :
(∃! x : p, q) ↔ p ∧ q
source
@[simp]
theorem existsUnique_false {α : Sort u_1} :
¬∃! x : α, False
source
theorem existsUnique_prop_of_true {p : Prop} {q : p → Prop} (h : p) :
(∃! h' : p, q h') ↔ q h
source
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
source
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
source
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
source
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₂
source
instance List.decidableBExistsUnique {α : Type u_2} [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) :
Decidable (∃! x : α, x ∈ l ∧ p x)

This invokes the two `Decidable` arguments $O(n)$ times.

Equations

- One or more equations did not get rendered due to their size.
- List.decidableBExistsUnique p [] = isFalse ⋯