Theorems · Definition · logic and foundations

FirstOrder.Language.Theory.typeOf

{L : FirstOrder.Language} →
  (T : L.Theory) →
    {α : Type w} → {M : Type w'} → [inst : L.Structure M] → [Nonempty M] → [M ⊨ T] → (α → M) → T.CompleteType α

The set of all formulas true at a tuple in a structure forms a complete type.

Defined in: Mathlib.ModelTheory.Types
Cited by: 3 results in Mathlib
Foundations: Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: FirstOrder.Language.Structure Nonempty FirstOrder.Language.Theory.Model

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

FirstOrder.Languagestatement and proof · cited by 1,084
FirstOrder.Language.Structurestatement and proof · cited by 775
FirstOrder.Language.Theorystatement and proof · cited by 154
FirstOrder.Language.withConstantsproof · cited by 108
FirstOrder.Language.Theory.Modelstatement and proof · cited by 67
FirstOrder.Language.Theory.CompleteTypestatement · cited by 35
FirstOrder.Language.completeTheoryproof · cited by 14

Cited by4

Results whose statement or proof uses this declaration.

FirstOrder.Language.Theory.realizedTypesproof · cited by 1
FirstOrder.Language.Theory.typeOf.congr_simpstatement and proof · cited by 0
FirstOrder.Language.Theory.CompleteType.mem_typeOfstatement · cited by 0
FirstOrder.Language.Theory.CompleteType.formula_mem_typeOfstatement · cited by 0