exists — Mathlib

English

There exists an x in p with property q x if and only if there exists x ∈ B and h ∈ p with q ⟨x,h⟩.

Русский

Существует x ∈ p такое, что q x, эквивалентно существованию пары (x,h) с x ∈ B и h ∈ p, где q ⟨x,h⟩ выполняется.

LaTeX

$$∃ x, q x ↔ ∃ (x : B) (h : x ∈ p), q ⟨x, h⟩$$

Lean4

protected theorem «exists» {q : p → Prop} : (∃ x, q x) ↔ ∃ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩ :=
  SetCoe.exists

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