exists — Mathlib

English

The existential quantifier over a discrete type is equivalent to the existential quantifier over the underlying type.

Русский

Существование над дискретным типом эквивалентно существованию над базовым типом.

LaTeX

$$$\\exists a:\\mathrm{Discrete}(\\alpha),\\; p(a) \\quad\\Leftrightarrow\\quad \\exists a'\\in \\alpha,\\; p(\\langle a'\\rangle)$$$

Lean4

@[simp]
theorem «exists» {α : Type*} {p : Discrete α → Prop} : (∃ (a : Discrete α), p a) ↔ ∃ (a' : α), p ⟨a'⟩ :=
  by
  rw [iff_iff_eq, discreteEquiv.exists_congr_left]
  simp [discreteEquiv]

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