Structures · Logic and sets
FirstOrder.Language.LHom.IsExpansionOn
A language homomorphism is an expansion on a structure if it commutes with the interpretation of all symbols on that structure.
- Defined in
- Mathlib.ModelTheory.LanguageMap
- Shape
- 2 explicit arguments · adds map_onFunction, map_onRelation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- FirstOrder.Language.order
- FirstOrder.Language.sum
- FirstOrder.Language.constantsOn
- FirstOrder.Language.withConstants
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- FirstOrder.Language.LHom.substructureReduct
- FirstOrder.Language.LHom.map_onFunction
- FirstOrder.Language.Formula.realize_equivSentence_symm_con
- FirstOrder.Language.LHom.realize_onTerm
- FirstOrder.Language.LHom.map_onRelation
- FirstOrder.Language.Term.realize_varsToConstants
- FirstOrder.Language.LHom.onTheory_model
- FirstOrder.Language.withConstants_funMap_sumInl
- FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram
- FirstOrder.Language.LHom.setOfPred_realize_onFormula
- FirstOrder.Language.LHom.realize_onBoundedFormula
- FirstOrder.Language.Formula.realize_equivSentence
- Set.TermDefinable.map_expansion
- FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv
- FirstOrder.Language.Term.realize_constantsToVars
- FirstOrder.Language.LHom.IsExpansionOn.map_onRelation
- FirstOrder.Language.LHom.realize_onFormula
- FirstOrder.Language.LHom.IsExpansionOn.map_onFunction
- FirstOrder.Language.Term.realize_constantsVarsEquivLeft
- Set.Definable.map_expansion
- FirstOrder.Language.addConstants_expansion
- FirstOrder.Language.LHom.substructureReduct.congr_simp
- FirstOrder.Language.LHom.funMap_sumInr
- FirstOrder.Language.LHom.realize_onSentence
- FirstOrder.Language.LHom.sumMap_isExpansionOn
- FirstOrder.Language.LHom.setOf_realize_onFormula
- FirstOrder.Language.withConstants_relMap_sumInl
- FirstOrder.Language.LHom.sumElim_isExpansionOn
- FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram_toFun
- FirstOrder.Language.Formula.realize_exClosure_of_realize_equivSentence
- FirstOrder.Language.instOrderedStructureOfOrderOfIsExpansionOnOrderLHom
- FirstOrder.Language.LHom.mem_substructureReduct
- FirstOrder.Language.LHom.coe_substructureReduct
- FirstOrder.Language.LHom.funMap_sumInl
Ancestors0
No ancestors.