Theorem FirstOrder.Language.Embedding.toEmbedding_toPartialEquiv

Modification history

2024-08-06 09:11
Mathlib/ModelTheory/PartialEquiv.lean
feat(ModelTheory/Substructures): define equivalences between substructures and prove simple results (#11175) …
Added FirstOrder.Language.Embedding.toEmbedding_toPartialEquivView on Github →