Commit 2026-01-20 15:29 1f5d2017

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Topology/Types.lean

Modified Mathlib/ModelTheory/Types.lean

added theorem FirstOrder.Language.Theory.CompleteType.false_of_mem_of_not_mem

added theorem FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff

added def FirstOrder.Language.Theory.CompleteType.typesWith

added theorem FirstOrder.Language.Theory.CompleteType.typesWith_eq_univ_of_mem_onTheory_lhomWithConstants

added theorem FirstOrder.Language.Theory.CompleteType.typesWith_inf

added theorem FirstOrder.Language.Theory.CompleteType.typesWith_not

added theorem FirstOrder.Language.Theory.CompleteType.typesWith_top

Modified Mathlib/Tactic/Linter/DirectoryDependency.lean