Mathlib.Logic.ExistsUnique

ExistsUnique definition

(p : α → Prop)

Full source

/-- For `p : α → Prop`, `ExistsUnique p` means that there exists a unique `x : α` with `p x`. -/
def ExistsUnique (p : α → Prop) := ∃ x, p x ∧ ∀ y, p y → y = x

Unique Existence

Informal description

For a predicate $ p : \alpha \to \text{Prop} $, $\text{ExistsUnique} \, p$ means that there exists a unique $ x : \alpha $ such that $ p(x) $ holds. Formally, this is defined as the conjunction of existence ($\exists x, p(x)$) and uniqueness ($\forall y, p(y) \to y = x$).

Mathlib.Notation.isExplicitBinderSingular definition

(xs : TSyntax `` explicitBinders) : Bool

Full source

/-- Checks to see that `xs` has only one binder. -/
def isExplicitBinderSingular (xs : TSyntax ``explicitBinders) : Bool :=
  match xs with
  | `(explicitBinders| $_:binderIdent $[: $_]?) => true
  | `(explicitBinders| ($_:binderIdent : $_)) => true
  | _ => false

Check for singular explicit binder

Informal description

The function checks whether a given syntax node `xs` represents a single explicit binder, which can be either an identifier with an optional type annotation or a parenthesized identifier with a type annotation. It returns `true` if the binder is singular in this sense, and `false` otherwise.

Mathlib.Notation.term∃!_,_ definition

: Lean.ParserDescr✝

Full source

macromacro "∃!" xs:explicitBinders ", " b:term : term => do
  if !isExplicitBinderSingular xs then
    Macro.throwErrorAt xs "\
      The `ExistsUnique` notation should not be used with more than one binder.\n\
      \n\
      The reason for this is that `∃! (x : α), ∃! (y : β), p x y` has a completely different \
      meaning from `∃! q : α × β, p q.1 q.2`. \
      To prevent confusion, this notation requires that you be explicit \
      and use one with the correct interpretation."
  expandExplicitBinders ``ExistsUnique xs b

Unique existential quantifier notation ($\exists!$)

Informal description

The notation $\exists! x : \alpha, p(x)$ denotes that there exists a unique element $x$ in the type $\alpha$ such that the predicate $p(x)$ holds. This is syntactic sugar for `ExistsUnique (fun (x : α) ↦ p x)`. This notation does not support multiple binders (like $\exists! (x : \alpha) (y : \beta), p(x, y)$) as a shorthand for nested uniqueness ($\exists! (x : \alpha), \exists! (y : \beta), p(x, y)$), because such usage could be ambiguous. Instead, the intended meaning is typically expressed as $\exists! q : \alpha \times \beta, p(q.1, q.2)$.

Mathlib.Notation.unexpandExistsUnique definition

: Lean.PrettyPrinter.Unexpander

Full source

/--
Pretty-printing for `ExistsUnique`, following the same pattern as pretty printing for `Exists`.
However, it does *not* merge binders.
-/
@[app_unexpander ExistsUnique] def unexpandExistsUnique : Lean.PrettyPrinter.Unexpander
  | `($(_) fun $x:ident ↦ $b)                      => `(∃! $x:ident, $b)
  | `($(_) fun ($x:ident : $t) ↦ $b)               => `(∃! $x:ident : $t, $b)
  | _                                               => throw ()

Pretty-printer for unique existence notation

Informal description

The pretty-printer for the `ExistsUnique` notation `∃!`, which formats expressions of the form `∃! x, p x` or `∃! x : α, p x` without merging binders.

Mathlib.Notation.term∃!__,_ definition

: Lean.ParserDescr✝

Full source

/--
`∃! 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.
-/
syntax "∃! " binderIdent binderPred ", " term : term

Unique existence notation with bounded quantifier

Informal description

The notation `∃! x ∈ s, p x` means that there exists a unique element `x` in the set `s` such that the property `p x` holds. This is equivalent to the statement `∃! x, x ∈ s ∧ p x`. Similarly, notations like `∃! x ≤ n, p n` are supported for any relation defined using the `binder_predicate` command.

ExistsUnique.intro theorem

{p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ y, p y → y = w) : ∃! x, p x

Full source

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

Introduction Rule for Unique Existence

Informal description

For a predicate $ p : \alpha \to \text{Prop} $, if there exists an element $ w \in \alpha $ such that $ p(w) $ holds, and for any $ y \in \alpha $ satisfying $ p(y) $ we have $ y = w $, then there exists a unique $ x \in \alpha $ such that $ p(x) $ holds. In symbols: \[ \exists! x, p(x). \]

ExistsUnique.elim theorem

{p : α → Prop} {b : Prop} (h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b

Full source

theorem ExistsUnique.elim {p : α → Prop} {b : Prop}
    (h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b :=
  Exists.elim h₂ (fun w hw ↦ h₁ w (And.left hw) (And.right hw))

Elimination Rule for Unique Existence

Informal description

Given a predicate $ p : \alpha \to \text{Prop} $ and a proposition $ b $, if there exists a unique $ x $ such that $ p(x) $ holds, and if for every $ x $ satisfying $ p(x) $ and the uniqueness condition $ \forall y, p(y) \to y = x $ we can derive $ b $, then $ b $ holds.

existsUnique_of_exists_of_unique theorem

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

Full source

theorem existsUnique_of_exists_of_unique {p : α → Prop}
    (hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x :=
  Exists.elim hex (fun x px ↦ ExistsUnique.intro x px (fun y (h : p y) ↦ hunique y x h px))

Existence and Uniqueness Imply Unique Existence

Informal description

For a predicate $ p : \alpha \to \text{Prop} $, if there exists an element $ x $ such that $ p(x) $ holds, and for any two elements $ y_1, y_2 $ satisfying $ p(y_1) $ and $ p(y_2) $ we have $ y_1 = y_2 $, then there exists a unique $ x $ such that $ p(x) $ holds. In symbols: \[ \exists! x, p(x). \]

ExistsUnique.exists theorem

{p : α → Prop} : (∃! x, p x) → ∃ x, p x

Full source

theorem ExistsUnique.exists {p : α → Prop} : (∃! x, p x) → ∃ x, p x | ⟨x, h, _⟩ => ⟨x, h⟩

Existence from Unique Existence

Informal description

For any predicate $ p : \alpha \to \text{Prop} $, if there exists a unique $ x $ such that $ p(x) $ holds, then there exists some $ x $ such that $ p(x) $ holds.

ExistsUnique.unique theorem

{p : α → Prop} (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂

Full source

theorem ExistsUnique.unique {p : α → Prop}
    (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
  let ⟨_, _, hy⟩ := h; (hy _ py₁).trans (hy _ py₂).symm

Uniqueness in Unique Existence

Informal description

For any predicate $ p : \alpha \to \text{Prop} $, if there exists a unique $ x $ such that $ p(x) $ holds, then for any $ y_1, y_2 $ satisfying $ p(y_1) $ and $ p(y_2) $, we have $ y_1 = y_2 $.

existsUnique_congr theorem

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

Full source

theorem existsUnique_congr {p q : α → Prop} (h : ∀ a, p a ↔ q a) : (∃! a, p a) ↔ ∃! a, q a :=
  exists_congr fun _ ↦ and_congr (h _) <| forall_congr' fun _ ↦ imp_congr_left (h _)

Equivalence of Unique Existence under Predicate Equivalence

Informal description

For any predicates $p$ and $q$ on a type $\alpha$, if $p(a) \leftrightarrow q(a)$ holds for all $a \in \alpha$, then there exists a unique $a$ satisfying $p(a)$ if and only if there exists a unique $a$ satisfying $q(a)$. In other words, $\exists! a, p(a) \leftrightarrow \exists! a, q(a)$.

existsUnique_iff_exists theorem

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

Full source

@[simp] theorem existsUnique_iff_exists [Subsingleton α] {p : α → Prop} :
    (∃! x, p x) ↔ ∃ x, p x :=
  ⟨fun h ↦ h.exists, Exists.imp fun x hx ↦ ⟨hx, fun y _ ↦ Subsingleton.elim y x⟩⟩

Unique existence reduces to existence in subsingleton types

Informal description

For a subsingleton type $\alpha$ (i.e., a type with at most one element) and any predicate $p : \alpha \to \text{Prop}$, the statement "there exists a unique $x \in \alpha$ such that $p(x)$ holds" is equivalent to "there exists some $x \in \alpha$ such that $p(x)$ holds". In other words, $\exists! x, p(x) \leftrightarrow \exists x, p(x)$.

existsUnique_const theorem

{b : Prop} (α : Sort*) [i : Nonempty α] [Subsingleton α] : (∃! _ : α, b) ↔ b

Full source

theorem existsUnique_const {b : Prop} (α : Sort*) [i : Nonempty α] [Subsingleton α] :
    (∃! _ : α, b) ↔ b := by simp

Unique existence in subsingleton types reduces to the proposition itself

Informal description

For any type $\alpha$ that is nonempty and has at most one element (i.e., $\alpha$ is a subsingleton), and for any proposition $b$, the statement "there exists a unique element of $\alpha$ such that $b$ holds" is equivalent to $b$ itself. In other words, $(\exists! x : \alpha, b) \leftrightarrow b$.

existsUnique_eq theorem

{a' : α} : ∃! a, a = a'

Full source

@[simp] theorem existsUnique_eq {a' : α} : ∃! a, a = a' := by
  simp only [eq_comm, ExistsUnique, and_self, forall_eq', exists_eq']

Unique existence of equal element: $a = a'$

Informal description

For any element $a'$ of type $\alpha$, there exists a unique element $a$ of type $\alpha$ such that $a = a'$.

existsUnique_eq' theorem

{a' : α} : ∃! a, a' = a

Full source

/-- The difference with `existsUnique_eq` is that the equality is reversed. -/
@[simp] theorem existsUnique_eq' {a' : α} : ∃! a, a' = a := by
  simp only [ExistsUnique, and_self, forall_eq', exists_eq']

Unique existence of equal element (reversed equality): $a' = a$

Informal description

For any element $a'$ of type $\alpha$, there exists a unique element $a$ of type $\alpha$ such that $a' = a$.

existsUnique_prop theorem

{p q : Prop} : (∃! _ : p, q) ↔ p ∧ q

Full source

theorem existsUnique_prop {p q : Prop} : (∃! _ : p, q) ↔ p ∧ q := by simp

Unique Existence in Propositions: $(\exists! \_ : p, q) \leftrightarrow (p \land q)$

Informal description

For any propositions $p$ and $q$, there exists a unique element of type $p$ satisfying $q$ if and only if both $p$ and $q$ hold. In other words, $(\exists! \_ : p, q) \leftrightarrow (p \land q)$.

existsUnique_false theorem

: ¬∃! _ : α, False

Full source

@[simp] theorem existsUnique_false : ¬∃! _ : α, False := fun ⟨_, h, _⟩ ↦ h

Nonexistence of Unique Element Satisfying False Predicate

Informal description

There does not exist a unique element of type $\alpha$ satisfying the false predicate, i.e., $\neg \exists! x : \alpha, \text{False}$.

existsUnique_prop_of_true theorem

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

Full source

theorem existsUnique_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃! h' : p, q h') ↔ q h :=
  @existsUnique_const (q h) p ⟨h⟩ _

Unique Existence in Propositions Given Truth: $(\exists! h' : p, q(h')) \leftrightarrow q(h)$

Informal description

For any proposition $p$ and predicate $q$ on $p$, if $p$ holds (i.e., $h : p$), then there exists a unique element $h'$ of type $p$ satisfying $q(h')$ if and only if $q(h)$ holds. In other words: \[ (\exists! h' : p, q(h')) \leftrightarrow q(h). \]

ExistsUnique.elim₂ theorem

 {p : α → Sort*} [∀ 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

Full source

theorem ExistsUnique.elim₂ {p : α → Sort*} [∀ 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 := by
  simp only [existsUnique_iff_exists] at h₂
  apply h₂.elim
  exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩

Elimination Rule for Nested Unique Existence with Subsingleton Condition

Informal description

Let $p : \alpha \to \text{Sort}^*$ be a family of types where each $p(x)$ is a subsingleton (i.e., has at most one element), and let $q : \forall (x : \alpha), p(x) \to \text{Prop}$ be a predicate. If there exists a unique $x$ such that there exists a unique $h : p(x)$ satisfying $q(x, h)$, and if for every $x$ and $h : p(x)$, whenever $q(x, h)$ holds and for all $y$ and $hy : p(y)$, $q(y, hy)$ implies $y = x$, then $b$ holds, then the proposition $b$ holds. In symbols: \[ \left( \exists! x, \exists! h : p(x), q(x, h) \right) \land \left( \forall x h, q(x, h) \to (\forall y hy, q(y, hy) \to y = x) \to b \right) \to b \]

ExistsUnique.intro₂ theorem

 {p : α → Sort*} [∀ 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

Full source

theorem ExistsUnique.intro₂ {p : α → Sort*} [∀ 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 := by
  simp only [existsUnique_iff_exists]
  exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq

Unique Existence for Nested Predicates with Subsingleton Condition

Informal description

For a family of types $ p : \alpha \to \text{Sort}^* $ where each $ p(x) $ is a subsingleton (i.e., has at most one element), and a predicate $ q : \forall (x : \alpha), p(x) \to \text{Prop} $, if there exists an element $ w \in \alpha $ with $ hp : p(w) $ and $ hq : q(w, hp) $, and for any $ y \in \alpha $ and $ hy : p(y) $, if $ q(y, hy) $ holds then $ y = w $, then there exists a unique $ x \in \alpha $ such that there exists a unique $ hx : p(x) $ satisfying $ q(x, hx) $. In symbols: \[ \exists! x, \exists! hx : p(x), q(x, hx). \]

ExistsUnique.exists₂ theorem

 {p : α → Sort*} {q : ∀ (x : α) (_ : p x), Prop} (h : ∃! x, ∃! hx : p x, q x hx) : ∃ (x : _) (hx : p x), q x hx

Full source

theorem ExistsUnique.exists₂ {p : α → Sort*} {q : ∀ (x : α) (_ : p x), Prop}
    (h : ∃! x, ∃! hx : p x, q x hx) : ∃ (x : _) (hx : p x), q x hx :=
  h.exists.imp fun _ hx ↦ hx.exists

Existence from Unique Nested Existence

Informal description

For a family of types $ p : \alpha \to \text{Sort}^* $ and a predicate $ q : \forall (x : \alpha), p(x) \to \text{Prop} $, if there exists a unique $ x $ such that there exists a unique $ hx : p(x) $ satisfying $ q(x, hx) $, then there exists some $ x $ and some $ hx : p(x) $ such that $ q(x, hx) $ holds. In symbols: \[ \left( \exists! x, \exists! hx : p(x), q(x, hx) \right) \to \left( \exists x, \exists hx : p(x), q(x, hx) \right). \]

ExistsUnique.unique₂ theorem

 {p : α → Sort*} [∀ 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₂

Full source

theorem ExistsUnique.unique₂ {p : α → Sort*} [∀ 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₂ := by
  simp only [existsUnique_iff_exists] at h
  exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩

Uniqueness in Nested Unique Existence with Subsingleton Condition

Informal description

For a family of types $p : \alpha \to \text{Sort}^*$ where each $p(x)$ is a subsingleton (i.e., has at most one element), and a predicate $q : \forall (x : \alpha), p(x) \to \text{Prop}$, if there exists a unique $x$ such that there exists a unique $hx : p(x)$ satisfying $q(x, hx)$, then for any $y_1, y_2 \in \alpha$ with $hpy_1 : p(y_1)$, $hqy_1 : q(y_1, hpy_1)$, $hpy_2 : p(y_2)$, and $hqy_2 : q(y_2, hpy_2)$, we have $y_1 = y_2$. In symbols: \[ \left( \exists! x, \exists! hx : p(x), q(x, hx) \right) \to \left( \forall y_1 y_2, p(y_1) \to q(y_1, hpy_1) \to p(y_2) \to q(y_2, hpy_2) \to y_1 = y_2 \right). \]