mathlib3

ab60244a - feat(model_theory/basic,bundled): Structures induced by equivalences (#13124)

feat(model_theory/basic,bundled): Structures induced by equivalences (#13124) Defines `equiv.induced_Structure`, a structure on the codomain of a bijection that makes the bijection an isomorphism. Defines maps on bundled models to shift them along bijections and up and down universes.