Theorem FirstOrder.Language.Embedding.codRestrict_apply'

Modification history

2024-04-06 15:25

Mathlib/ModelTheory/Substructures.lean

feat(ModelTheory): lift of equivalences between direct limits, and direct limit of system of substructures (#11174) …

Added FirstOrder.Language.Embedding.codRestrict_apply'View on Github →