exists' — Mathlib

English

If you have a predicate p that takes a value x and a proof that x ∈ s, then the existence statement over the subtype s is equivalent to the existence of an element x ∈ s with p x h for some h.

Русский

Если предикат p принимает значение x и доказательство x ∈ s, то существование на подтипе s эквивалентно существованию элемента x ∈ s с таким доказательством.

LaTeX

$$$(\exists x : s, p x) \;\leftrightarrow\; \exists x : s, p x.1 x.2$$$

Lean4

theorem exists' {s : Set α} {p : ∀ x, x ∈ s → Prop} : (∃ (x : _) (h : x ∈ s), p x h) ↔ ∃ x : s, p x.1 x.2 :=
  (@SetCoe.exists _ _ fun x => p x.1 x.2).symm

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