Theorem FirstOrder.Language.Theory.CompleteType.typesWith_top

Modification history

2026-04-07 15:22
Mathlib/ModelTheory/Types.lean
chore(ModelTheory/Types): expose `T` in `typesWith` and move it to `Theory` (#36955) …
Modified FirstOrder.Language.Theory.CompleteType.typesWith_topView on Github →
2026-01-30 12:44
Mathlib/ModelTheory/Types.lean
chore: tidy various files (#34610)
Modified FirstOrder.Language.Theory.CompleteType.typesWith_topView on Github →
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.typesWith_topView on Github →