Commit 2022-03-21 09:13 8161ba28
View on Github →feat(model_theory/ultraproducts): Ultraproducts and the Compactness Theorem (#12531)
Defines filter.product, a dependent version of filter.germ.
Defines a structure on an ultraproduct (a filter.product with respect to an ultrafilter).
Proves Łoś's Theorem, characterizing when an ultraproduct realizes a formula.
Proves the Compactness theorem with ultraproducts.