Commit 2026-04-07 15:22 23b5466f

View on Github →

chore(ModelTheory/Types): expose T in typesWith and move it to Theory (#36955) Make the T : L.Theory argument explicit in typesWith and place the definition in FirstOrder.Language.Theory to enable dot notation.

Estimated changes

Modified Mathlib/ModelTheory/Topology/Types.lean

Modified Mathlib/ModelTheory/Types.lean

modified theorem FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff

deleted def FirstOrder.Language.Theory.CompleteType.typesWith

modified theorem FirstOrder.Language.Theory.CompleteType.typesWith_not

modified theorem FirstOrder.Language.Theory.CompleteType.typesWith_top

added def FirstOrder.Language.Theory.typesWith