mathlib
d0efbcb0 - feat(model_theory/elementary_maps): Elementary maps respect all (bounded) formulas (#14252)

Commit

3 years ago

feat(model_theory/elementary_maps): Elementary maps respect all (bounded) formulas (#14252) Generalizes `elementary_embedding.map_formula` to more classes of formula.

Author

awainverse

Parents

599240fc

mathlib d0efbcb0 - feat(model_theory/elementary_maps): Elementary maps respect all (bounded) formulas (#14252)

mathlib
d0efbcb0 - feat(model_theory/elementary_maps): Elementary maps respect all (bounded) formulas (#14252)