mathlib documentation

model_theory.quotients

Quotients of First-Order Structures #

This file defines prestructures and quotients of first-order structures.

Main Definitions #

@[class]
structure first_order.language.prestructure (L : first_order.language) {M : Type u_3} (s : setoid M) :
Type (max u_1 u_2 u_3)

A prestructure is a first-order structure with a setoid equivalence relation on it, such that quotienting by that equivalence relation is still a structure.

Instances of this typeclass
Instances of other typeclasses for first_order.language.prestructure
  • first_order.language.prestructure.has_sizeof_inst
theorem first_order.language.term.realize_quotient_mk {L : first_order.language} {M : Type u_3} [s : setoid M] [ps : L.prestructure s] {β : Type u_4} (t : L.term β) (x : β → M) :