# mathlib3documentation

model_theory.quotients

# Quotients of First-Order Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines prestructures and quotients of first-order structures.

## Main Definitions #

• If s is a setoid (equivalence relation) on M, a first_order.language.prestructure s is the data for a first-order structure on M that will still be a structure when modded out by s.
• The structure first_order.language.quotient_structure s is the resulting structure on quotient s.
@[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
@[protected, instance]
Equations
theorem first_order.language.fun_map_quotient_mk {L : first_order.language} {M : Type u_3} [s : setoid M] [ps : L.prestructure s] {n : } (f : L.functions n) (x : fin n M) :
(λ (i : fin n), x i) =
theorem first_order.language.rel_map_quotient_mk {L : first_order.language} {M : Type u_3} [s : setoid M] [ps : L.prestructure s] {n : } (r : L.relations n) (x : fin n M) :
(λ (i : fin n), x i)
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) :