mathlib documentation


Type Spaces #

This file defines the space of complete types over a first-order theory. (Note that types in model theory are different from types in type theory.)

Main Definitions #

Main Results #

Implementation Notes #


structure first_order.language.Theory.complete_type {L : first_order.language} (T : L.Theory) (α : Type w) :
Type (max u v w)

A complete type over a given theory in a certain type of variables is a maximally consistent (with the theory) set of formulas in that type.

Instances for first_order.language.Theory.complete_type
theorem first_order.language.Theory.complete_type.Inter_set_of_subset {L : first_order.language} {T : L.Theory} {α : Type w} {ι : Type u_1} (S : ι (L.with_constants α).Theory) :
( (i : ι), {p : T.complete_type α | S i p}) = {p : T.complete_type α | ( (i : ι), S i) p}