Structures · Logic and sets
FirstOrder.Language.IsFraisse
A Fraïssé class is a nonempty, essentially countable class of structures satisfying the hereditary, joint embedding, and amalgamation properties.
- Defined in
- Mathlib.ModelTheory.Fraisse
- Shape
- One type argument · adds is_nonempty, FG, is_essentially_countable, hereditary, jointEmbedding, amalgamation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- FirstOrder.Language.IsFraisse.FG
- FirstOrder.Language.IsFraisse.hereditary
- FirstOrder.Language.IsFraisse.jointEmbedding
- FirstOrder.Language.IsFraisse.amalgamation
- FirstOrder.Language.IsFraisse.is_equiv_invariant
- FirstOrder.Language.IsFraisse.is_essentially_countable
- FirstOrder.Language.IsFraisse.is_nonempty
Ancestors0
No ancestors.