exists — Mathlib

English

A simp lemma: existence over PProd α β is equivalent to the existence of coordinates a,b with p ⟨a,b⟩.

Русский

Лемма-упрощение: существование утверждения над PProd эквивалентно существованию координат a,b с p ⟨a,b⟩.

LaTeX

$$$(\\exists x : PProd \\;α\\;β,\\; p\\,x) \\iff \\exists a : α, \\exists b : β,\\; p\\langle a,b\\rangle.$$$

Lean4

@[simp]
theorem «exists» {p : PProd α β → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ :=
  ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩

Похожие утверждения