definable_iff_empty_definable_with_params

English

A is definable from s iff the empty set is definable in the language with A-constants from the parameter set.

Русский

Определяемость множества A по параметрам эквивалентна определяемости пустого множества в языке с константами A.

LaTeX

$$$A.Definable L s \iff (\emptyset : Set M).Definable (L[[A]]) s.$$$

Lean4

theorem definable_iff_empty_definable_with_params : A.Definable L s ↔ (∅ : Set M).Definable (L[[A]]) s :=
  empty_definable_iff.symm

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