model_nonemptyTheory_iff — Mathlib

English

A model M of the language L satisfies the nonempty theory exactly when M is nonempty.

Русский

Для любой теории L, модель M удовлетворяет теории nonemptyTheory тогда и только тогда, когда M непусто.

LaTeX

$$$M \vDash L.nonemptyTheory \iff Nonempty(M)$$$

Lean4

@[simp]
theorem model_nonemptyTheory_iff : M ⊨ L.nonemptyTheory ↔ Nonempty M := by
  simp only [nonemptyTheory, Theory.model_iff, Set.mem_singleton_iff, forall_eq, Sentence.realize_cardGe, Nat.cast_one,
    one_le_iff_ne_zero, mk_ne_zero_iff]

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