FirstOrder.Language.Ultraproduct.sentence_realize

theorem FirstOrder.Language.Ultraproduct.sentence_realize : ∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)] [inst_1 : ∀ (a : α), Nonempty (M a)] (φ : L.Sentence), u.Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ

**Łoś's Theorem**: This theorem states that for any given type 'α', any function 'M' mapping 'α' to another type, an ultrafilter 'u' on 'α', a first-order language 'L', and a sentence 'φ' in this language, the sentence is true in the ultraproduct of 'M' over 'u' if and only if the set of all 'α' where 'M a' satisfies 'φ' belongs to the ultrafilter 'u'. In other words, 'φ' is true in the ultraproduct of the structures if and only if it is almost true in the individual structures.

More concisely: Łoś's Theorem: An ultrafilter's membership of the set of elements satisfying a first-order property in an ultraproduct is determined by the set's membership in the ultrafilter in the base structures.