L : Language
T : Theory L
α : Type w
⊢ Nonempty (CompleteType T α) ↔ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T)
L : Language
T : Theory L
α : Type w
⊢ Nonempty (CompleteType T α) ↔ IsSatisfiable T
rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]
L : Language
T : Theory L
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅
L : Language
T : Theory L
α : Type w
⊢ Nonempty (CompleteType T α) ↔ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T)
rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne.def, not_iff_comm,
  ← union_empty ((L.lhomWithConstants α).onTheory T), ← setOf_subset_eq_empty_iff]
no goals
L : Language
T : Theory L
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅
simp