exists_coe — Mathlib

English

For a finite set s ⊆ α and a predicate p on s, there exists an element x ∈ s such that p holds for x iff there exists α-element a with a ∈ s and p ⟨a, proof⟩.

Русский

Для конечного множества s ⊆ α и предиката p на s существует элемент x ∈ s, для которого выполнено p, если и только если существует элемент a ∈ α с a ∈ s и p(⟨a, доказательство⟩).

LaTeX

$$$(\exists x : s, p x) \leftrightarrow \exists (x : α) (h : x ∈ s), p \langle x, h \rangle$$$

Lean4

protected theorem exists_coe {α : Type*} (s : Finset α) (p : s → Prop) :
    (∃ x : s, p x) ↔ ∃ (x : α) (h : x ∈ s), p ⟨x, h⟩ :=
  Subtype.exists

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