exists_coe — Mathlib

English

There exists an element x in m such that p x holds if and only if there exists some (a,i) with p ⟨a,i⟩.

Русский

Существует элемент x в m такой, что p x, тогда и только тогда существует пара (a,i) с p ⟨a,i⟩.

LaTeX

$$∃ x : m, p x ↔ ∃ (a : α) (i : Fin (m.count a)), p ⟨a,i⟩$$

Lean4

@[simp]
protected theorem exists_coe (p : m → Prop) : (∃ x : m, p x) ↔ ∃ (x : α) (i : Fin (m.count x)), p ⟨x, i⟩ :=
  Sigma.exists

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