empty_definable_iff — Mathlib

English

The empty set is definable in any language with respect to any structure.

Русский

Пустое множество определимо в любом языке относительно любой структуры.

LaTeX

$$$(\emptyset : Set M)\Definable L s.$$$

Lean4

theorem empty_definable_iff : (∅ : Set M).Definable L s ↔ ∃ φ : L.Formula α, s = setOf φ.Realize :=
  by
  rw [Definable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onFormula]
  simp

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