mathlib3 documentation


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 #

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