# Formalizing "isomorphism preserves everything" using language of logic

In many areas of mathematics there is a notion of isomorphism, which is a map that preserves some structure – an algebraic structure, a topology, a sheaf etc. It is "obvious" that every isomorphism of given structures preserves everything defined by the structures. For example:

–homeomorphism preserves borelianity (image of Borel set is a Borel set);

–isomorphism of algebraic varieties preserves rational maps (composing rational map with isomorphism gives a rational map);

–isometry of metric spaces preserves balls (image of a ball is a ball of the same radius) – and it is not true for every homeomorphism, as the definition of "ball" uses the metric structure, not only the topological one.

All the above and many similar statements can be easily proved by hand, by writing all the definitions and proving, step by step, that isomorphism preserves every used object. Thus we can actually skip all those proofs and say it is all obvious.

The questions is: is there any theorem of mathematical logic that formalizes all such arguments? I would expect it to be of form "for any two sets X, Y with some structures, if some function $f:X\to Y$ preserves the structures, then every statement true for the first one and defined using the structure is true for the other after applying appropriate changes (like $A \mapsto f(A)$ for any $A\subset X$)".

Formally this can to a large extent be handled by extending the language with a new sort for real numbers, and constants for every real -- but it may be slicker to extend the notion of "logical language" with some kind of pseudo-function letters that always produce real results (or whatever one needs) and then allow one to have atomic formulas of the form $(f_1[t_{11},\ldots,t_{1n}],\ldots,f_k[t_{k1},\ldots,t_{kn}]) \in A$ where $A$ is any fixed subset of $\mathbb R^k$ at the metalevel.