English
The set {p : T.CompleteType α | S ⊆ ↑p} is empty iff the theory (L.lhomWithConstants α).onTheory T ∪ S is unsatisfiable.
Русский
Множество {p : T.CompleteType α | S ⊆ ↑p} пусто тогда и только тогда, когда теория (L.lhomWithConstants α).onTheory T ∪ S не удовлетворима.
LaTeX
$$$ {p : T.CompleteType α | S ⊆ ↑p} = ∅ \\\\iff ¬((L.lhomWithConstants α).onTheory T \\\\cup S).IsSatisfiable$$$
Lean4
theorem setOf_subset_eq_empty_iff (S : L[[α]].Theory) :
{p : T.CompleteType α | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable :=
by
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]
refine
⟨fun h =>
⟨⟨L[[α]].completeTheory h.some, (subset_union_left (t := S)).trans completeTheory.subset,
completeTheory.isMaximal (L[[α]]) h.some⟩,
(((L.lhomWithConstants α).onTheory T).subset_union_right).trans completeTheory.subset⟩,
?_⟩
rintro ⟨p, hp⟩
exact p.isMaximal.1.mono (union_subset p.subset hp)
