exists — Mathlib

English

There exists a p such that p holds for some element of Lex α, if and only if there exists an element a of α with p (toLex a).

Русский

Существует такое p, что оно выполняется для некоторого элемента Lex α, тогда и только тогда существует a ∈ α с p(toLex a).

LaTeX

$$$\exists a, p(a) \iff \exists a, p(\mathrm{toLex}\,a)$$$

Lean4

@[simp]
protected theorem «exists» {p : αᵒᵈ → Prop} : (∃ a, p a) ↔ ∃ a, p (toDual a) :=
  Iff.rfl

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