def
Certifiable.IsCertifiable
{n : ℕ}
{Ω : Fin n → Type u_1}
(s : ℕ)
(A : Set ((i : Fin n) → Ω i))
:
Definition 9.5.20 ($s$-certifiable). A set $A \subseteq \prod_i \Omega_i$ is $s$-certifiable if every $x \in A$ admits an index set $I$ of size at most $s$ such that any other point $y$ agreeing with $x$ on $I$ also lies in $A$.