Theorems · Inductive type · logic and foundations
FirstOrder.Language.Prestructure
FirstOrder.Language → {M : Type u_1} → Setoid M → Type (max (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.
- Defined in
- Mathlib.ModelTheory.Quotients
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Languagestatement · cited by 1,084
Cited by12
Results whose statement or proof uses this declaration.
- FirstOrder.Language.Prestructure.toStructurestatement and proof · cited by 5
- FirstOrder.Language.funMap_quotient_mk'statement and proof · cited by 3
- FirstOrder.Language.relMap_quotient_mk'statement and proof · cited by 2
- FirstOrder.Language.Term.realize_quotient_mk'statement and proof · cited by 1
- FirstOrder.Language.Prestructure.fun_equivstatement and proof · cited by 1
- FirstOrder.Language.Prestructure.rel_equivstatement and proof · cited by 1
- FirstOrder.Language.Prestructure.casesOnstatement and proof · cited by 0
- FirstOrder.Language.Prestructure.ctorIdxstatement and proof · cited by 0
- FirstOrder.Language.Prestructure.noConfusionstatement and proof · cited by 0
- FirstOrder.Language.Prestructure.noConfusionTypestatement and proof · cited by 0
- FirstOrder.Language.Prestructure.recOnstatement and proof · cited by 0
- FirstOrder.Language.Prestructure.mk.noConfusionstatement · cited by 0