Theorem FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff

Modification history

2026-01-20 15:29

Mathlib/ModelTheory/Types.lean

feat(ModelTheory/Types): Construct a topology on CompleteType and prove the space is TotallySeparated (#32215)

Added FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff View on Github →