mathlib3

8161ba28 - feat(model_theory/ultraproducts): Ultraproducts and the Compactness Theorem (#12531)

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. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>