Quotients

📁 Source: Mathlib/ModelTheory/Quotients.lean

Statistics

Metric	Count
Definitions Prestructure, toStructure, quotientStructure	3
Theorems fun_equiv, rel_equiv, realize_quotient_mk', funMap_quotient_mk', relMap_quotient_mk'	5
Total	8

FirstOrder.Language

Definitions

Name	Category	Theorems
Prestructure 📖	CompData	—
quotientStructure 📖	CompOp	9 math math: relMap_quotient_mk', DirectLimit.funMap_quotient_mk'_sigma_mk', funMap_quotient_mk', Ultraproduct.realize_formula_cast, DirectLimit.relMap_quotient_mk'_sigma_mk', Term.realize_quotient_mk', Ultraproduct.boundedFormula_realize_cast, Ultraproduct.term_realize_cast, Ultraproduct.funMap_cast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
funMap_quotient_mk' 📖	mathematical	—	Structure.funMap quotientStructure Prestructure.toStructure	—	Prestructure.fun_equiv Quotient.finChoice_eq
relMap_quotient_mk' 📖	mathematical	—	Structure.RelMap quotientStructure Prestructure.toStructure	—	Prestructure.rel_equiv Quotient.finChoice_eq

FirstOrder.Language.Prestructure

Definitions

Name	Category	Theorems
toStructure 📖	CompOp	5 math math: FirstOrder.Language.relMap_quotient_mk', FirstOrder.Language.funMap_quotient_mk', rel_equiv, FirstOrder.Language.Term.realize_quotient_mk', fun_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_equiv 📖	mathematical	piSetoid	FirstOrder.Language.Structure.funMap toStructure	—	—
rel_equiv 📖	mathematical	piSetoid	FirstOrder.Language.Structure.RelMap toStructure	—	—

FirstOrder.Language.Term

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realize_quotient_mk' 📖	mathematical	—	realize FirstOrder.Language.quotientStructure FirstOrder.Language.Prestructure.toStructure	—	FirstOrder.Language.funMap_quotient_mk'

---

← Back to Index