English
Łoś's theorem for sentences: A sentence φ is true in the ultraproduct if and only if φ is true in almost all the component structures M(a).
Русский
Теорема Лёша для предложений: предложение φ истинно в ультропроизведении тогда и только тогда, когда φ истинно в почти всех компонентах M(a).
LaTeX
$$$(u:\text{Filter } α).Product M \models \phi \iff \forall^u a, M(a) \models \phi$$$
Lean4
/-- **Łoś's Theorem**: A sentence is true in an ultraproduct if and only if the set of structures
it is true in is in the ultrafilter. -/
theorem sentence_realize (φ : L.Sentence) : (u : Filter α).Product M ⊨ φ ↔ ∀ᶠ a : α in u, M a ⊨ φ :=
by
simp_rw [Sentence.Realize]
rw [← realize_formula_cast φ, iff_eq_eq]
exact congr rfl (Subsingleton.elim _ _)