Theorems · Definition · logic and foundations

FirstOrder.Language.Theory.realizedTypes

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

A complete type p is realized in a particular structure when there is some tuple v whose type is p.

Defined in

Mathlib.ModelTheory.Types

Cited by

1 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureNonemptyFirstOrder.Language.Theory.Model