Structures · Logic and sets
FirstOrder.Language.Theory.Model
A model of a theory is a structure in which every sentence is realized as true.
- Defined in
- Mathlib.ModelTheory.Semantics
- Shape
- 2 explicit arguments · adds realize_of_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- FirstOrder.Language.ring
- FirstOrder.Language.graph
How is a type an instance?
Loading the hierarchy index…
Assumed by57
- FirstOrder.Language.Theory.realize_sentence_of_mem
- FirstOrder.Language.Theory.ModelType.of
- FirstOrder.Language.Theory.Iff.realize_bd_iff
- FirstOrder.Language.Theory.Model.isSatisfiable
- FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence
- FirstOrder.Language.Theory.typeOf
- FirstOrder.Field.compatibleRingOfModelField
- FirstOrder.Field.fieldOfModelACF
- FirstOrder.Field.modelField_of_modelACF
- FirstOrder.Language.Theory.IsComplete.realize_sentence_iff
- FirstOrder.Language.simpleGraphOfStructure
- FirstOrder.Language.Theory.Model.realize_of_mem
- FirstOrder.Language.Theory.IsComplete.eq_complete_theory
- FirstOrder.Language.linearOrderOfModels
- FirstOrder.Field.charP_of_model_fieldOfChar
- FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram
- FirstOrder.Field.isAlgClosed_of_model_ACF
- FirstOrder.Language.Theory.ModelsBoundedFormula.realize_formula
- FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo
- FirstOrder.Language.denselyOrdered_of_dlo
- FirstOrder.Language.Theory.IsUniversal.models_of_embedding
- FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le
- FirstOrder.Language.noBotOrder_of_dlo
- FirstOrder.Language.ElementarilyEquivalent.theory_model
- FirstOrder.Language.Theory.realizedTypes
- FirstOrder.Language.Theory.completeTheory.subset
- FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula
- FirstOrder.Language.card_le_of_model_distinctConstantsTheory
- FirstOrder.Language.dlo_isExtensionPair
- FirstOrder.Language.Theory.Iff.realize_iff
- FirstOrder.Language.dlo_age
- FirstOrder.Language.Theory.exists_large_model_of_infinite_model
- FirstOrder.Language.noTopOrder_of_dlo
- FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite
- FirstOrder.Language.realize_iff_of_model_completeTheory
- FirstOrder.Language.structure_simpleGraphOfStructure
- FirstOrder.Field.fieldOfModelField
- FirstOrder.Language.simpleGraphOfStructure_adj
- FirstOrder.Language.Theory.CompleteType.mem_typeOf
- FirstOrder.Language.Theory.ModelType.coe_of
- FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf
- FirstOrder.Language.ElementarySubstructure.theory_model
- FirstOrder.Field.FieldAxiom.toProp_of_model
- FirstOrder.Language.Theory.Iff.models_sentence_iff
- FirstOrder.Language.Theory.typeOf.congr_simp
- FirstOrder.Language.instModelLinearOrderTheoryOfDlo
- FirstOrder.Field.instModelFieldOfCharOfACF
- FirstOrder.Language.Substructure.models_of_isUniversal
- FirstOrder.Language.preorderOfModels
- FirstOrder.Language.partialOrderOfModels
Ancestors0
No ancestors.