Commit 2023-05-25 03:53 141c9c36

View on Github →

feat: port ModelTheory.Ultraproducts (#3976)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Ultraproducts.lean

added theorem FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast

added theorem FirstOrder.Language.Ultraproduct.funMap_cast

added theorem FirstOrder.Language.Ultraproduct.realize_formula_cast

added theorem FirstOrder.Language.Ultraproduct.sentence_realize

added theorem FirstOrder.Language.Ultraproduct.term_realize_cast