sentence_realize — Mathlib

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 _ _)

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