Commit 2022-04-08 06:14 ab60244a
View on Github →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.