Theorem FirstOrder.Language.ElementarySubstructure.realize_sentence

Modification history

2023-12-16 02:09

Mathlib/ModelTheory/ElementaryMaps.lean

chore(ModelTheory/ElementarySubstructures): Split elementary substructures into their own file (#9026) …

Modified FirstOrder.Language.ElementarySubstructure.realize_sentence View on Github →

2023-05-13 13:53

Mathlib/ModelTheory/ElementaryMaps.lean

feat: port ModelTheory.ElementaryMaps (#3931)

Added FirstOrder.Language.ElementarySubstructure.realize_sentence View on Github →