Structures · Logic and sets
FirstOrder.Language.StrongHomClass
StrongHomClass L F M N states that F is a type of L-homomorphisms which preserve
relations in both directions.
- Defined in
- Mathlib.ModelTheory.Basic
- Shape
- 4 explicit arguments · adds map_fun, map_rel
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- FirstOrder.Language.order
- FirstOrder.Language.empty
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- FirstOrder.Language.StrongHomClass.map_rel
- FirstOrder.Language.StrongHomClass.toEmbedding
- FirstOrder.Language.StrongHomClass.toEquiv
- FirstOrder.Language.StrongHomClass.realize_sentence
- FirstOrder.Language.StrongHomClass.realize_formula
- FirstOrder.Language.BoundedFormula.IsQF.realize_embedding
- FirstOrder.Language.StrongHomClass.realize_boundedFormula
- FirstOrder.Language.StrongHomClass.toEquiv_toFun
- FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding
- FirstOrder.Language.StrongHomClass.homClass
- FirstOrder.Language.StrongHomClass.toOrderIsoClass
- FirstOrder.Language.StrongHomClass.elementarilyEquivalent
- FirstOrder.Language.StrongHomClass.toEmbedding_toFun
- FirstOrder.Language.StrongHomClass.toEquiv.congr_simp
- FirstOrder.Language.StrongHomClass.map_fun
- FirstOrder.Language.BoundedFormula.IsExistential.realize_embedding
- FirstOrder.Language.StrongHomClass.toEquiv_invFun
- FirstOrder.Language.StrongHomClass.theory_model
Ancestors0
No ancestors.