English
A union of theories {T_i} is satisfiable iff every finite subunion is satisfiable.
Русский
Объединение теорий {T_i} удовлетворимо тогда и только тогда, когда удовлетворимо каждое конечное подобъединение.
LaTeX
$$$\\mathrm{IsSatisfiable}\\left(\\bigcup_i T_i\\right) \\iff \\forall s \\in \\mathrm{Finset}(\\iota),\\; \\mathrm{IsSatisfiable}\\left(\\bigcup_{i \\in s} T_i\\right).$$$
Lean4
theorem isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset {ι : Type*} (T : ι → L.Theory) :
IsSatisfiable (⋃ i, T i) ↔ ∀ s : Finset ι, IsSatisfiable (⋃ i ∈ s, T i) := by
classical
refine ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _), fun h => ?_⟩
rw [isSatisfiable_iff_isFinitelySatisfiable]
intro s hs
rw [Set.iUnion_eq_iUnion_finset] at hs
obtain ⟨t, ht⟩ :=
Directed.exists_mem_subset_of_finset_subset_biUnion
(by
exact
Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩)
hs
exact (h t).mono ht
