exists — Mathlib

English

For a subset s of α and a predicate p on s, there exists an element x of s with p x if and only if there exists some pair (x, h) with x ∈ α, h ∈ s, such that p ⟨x, h⟩.

Русский

Пусть s ⊆ α и p над s. Существует элемент x подтипа s с свойством p x тогда и только тогда, когда существует пара (x, h) с x ∈ α, h ∈ s, такая что p ⟨x, h⟩.

LaTeX

$$$(\exists x : s, p x) \;\iff\; \exists x : \alpha, \exists h : x \in s,\; p\langle x, h \rangle$$$

Lean4

theorem «exists» {s : Set α} {p : s → Prop} : (∃ x : s, p x) ↔ ∃ (x : _) (h : x ∈ s), p ⟨x, h⟩ :=
  Subtype.exists

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