Structures · Logic and sets
FirstOrder.Language.Structure
A first-order structure on a type M consists of interpretations of all the symbols in a given
language. Each function of arity n is interpreted as a function sending tuples of length n
(modeled as (Fin n → M)) to M, and a relation of arity n is a function from tuples of length
n to Prop.
- Defined in
- Mathlib.ModelTheory.Basic
- Shape
- 2 explicit arguments · adds funMap, RelMap
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances5
- FirstOrder.Language.sum
- FirstOrder.Language.constantsOn
- FirstOrder.Language.withConstants
- FirstOrder.Language.skolem₁
- FirstOrder.Language.presburger
How is a type an instance?
Loading the hierarchy index…
Assumed by946
- FirstOrder.Language.BoundedFormula.Realize
- FirstOrder.Language.Term.realize
- FirstOrder.Language.Formula.Realize
- FirstOrder.Language.Substructure.closure
- FirstOrder.Language.Structure.funMap
- FirstOrder.Language.Structure.RelMap
- FirstOrder.Language.Sentence.Realize
- FirstOrder.Language.Substructure.map
- FirstOrder.Language.Substructure.subtype
- FirstOrder.Language.Embedding.toHom
- Set.Definable
- FirstOrder.Language.Embedding.comp
- FirstOrder.Language.PartialEquiv.dom
- FirstOrder.Language.Substructure.FG
- FirstOrder.Language.Equiv.toEmbedding
- FirstOrder.Language.PartialEquiv.cod
- FirstOrder.Language.Equiv.symm
- FirstOrder.Language.Substructure.comap
- FirstOrder.Language.Hom.range
- FirstOrder.Language.constantMap
- FirstOrder.Language.Substructure.inclusion
- FirstOrder.Language.PartialEquiv.toEquiv
- FirstOrder.Language.DirectLimit
- FirstOrder.Language.Hom.comp
- FirstOrder.Language.ElementarilyEquivalent
- FirstOrder.Language.Substructure.CG
- FirstOrder.Language.age
- FirstOrder.Language.DirectLimit.of
- Set.DefinableFun
- FirstOrder.Language.Structure.Sigma
- FirstOrder.Language.Term.realize_relabel
- FirstOrder.Language.Substructure.gc_map_comap
- FirstOrder.Language.completeTheory
- FirstOrder.Language.Embedding.equivRange
- FirstOrder.Language.DirectLimit.setoid
- FirstOrder.Language.DefinableSet
- FirstOrder.Language.ClosedUnder
- FirstOrder.Language.Substructure.fg_iff_structure_fg
- FirstOrder.Language.Equiv.toEquiv
- FirstOrder.Language.Substructure.subset_closure
- FirstOrder.Language.Equiv.comp
- Set.TermDefinable
- FirstOrder.Language.Theory.realize_sentence_of_mem
- FirstOrder.Language.Equiv.toHom
- FirstOrder.Language.DirectLimit.unify
- FirstOrder.Language.Embedding.refl
- FirstOrder.Language.Hom.id
- FirstOrder.Language.Substructure.giMapComap
- FirstOrder.Language.FGEquiv
- FirstOrder.Language.Substructure.gciMapComap
Ancestors0
No ancestors.