Structures · Logic and sets
FirstOrder.Language.HomClass
HomClass L F M N states that F is a type of L-homomorphisms. You should extend this
typeclass when you extend FirstOrder.Language.Hom.
- 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 instances1
- FirstOrder.Language.order
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- FirstOrder.Language.HomClass.map_fun
- FirstOrder.Language.HomClass.realize_term
- FirstOrder.Language.HomClass.map_constants
- FirstOrder.Language.HomClass.map_rel
- FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective
- FirstOrder.Language.HomClass.strictMono
- FirstOrder.Language.HomClass.monotone
- FirstOrder.Language.HomClass.toHom
- FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic
- FirstOrder.Language.HomClass.toHom_toFun
- FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp
Ancestors0
No ancestors.