nonempty_iff — Mathlib

English

Nonempty (T.CompleteType α) is equivalent to T being satisfiable.

Русский

Не пустота (T.CompleteType α) эквивалентна тому, что T удовлетворима.

LaTeX

$$$Nonempty(T.CompleteType α) \\\\iff T.IsSatisfiable$$$

Lean4

theorem nonempty_iff : Nonempty (T.CompleteType α) ↔ T.IsSatisfiable :=
  by
  rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]
  rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne, not_iff_comm, ←
    union_empty ((L.lhomWithConstants α).onTheory T), ← setOf_subset_eq_empty_iff]
  simp

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