Documentation Verification Report

Ultraproducts

📁 Source: Mathlib/ModelTheory/Ultraproducts.lean

Statistics

Metric	Count
Definitions `setoidPrestructure`, `structure`	2
Theorems `instNonempty`, `boundedFormula_realize_cast`, `funMap_cast`, `realize_formula_cast`, `sentence_realize`, `term_realize_cast`	6
Total	8

FirstOrder.Language.Ultraproduct

Definitions

Name	Category	Theorems
`setoidPrestructure` 📖	CompOp	4 math math: `realize_formula_cast`, `boundedFormula_realize_cast`, `term_realize_cast`, `funMap_cast`
`structure` 📖	CompOp	1 math math: `sentence_realize`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundedFormula_realize_cast` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.Realize` `Filter.productSetoid` `Ultrafilter.toFilter` `FirstOrder.Language.quotientStructure` `setoidPrestructure` `Filter.Eventually`	—	`Ultrafilter.neBot` `term_realize_cast` `Quotient.eq''` `FirstOrder.Language.relMap_quotient_mk'` `Ultrafilter.eventually_imp` `Quotient.forall` `Fin.snoc_last` `Fin.snoc_castSucc` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Filter.mem_of_superset` `Filter.eventually_iff`
`funMap_cast` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `Filter.productSetoid` `Ultrafilter.toFilter` `FirstOrder.Language.quotientStructure` `setoidPrestructure`	—	`FirstOrder.Language.funMap_quotient_mk'`
`realize_formula_cast` 📖	mathematical	—	`FirstOrder.Language.Formula.Realize` `Filter.productSetoid` `Ultrafilter.toFilter` `FirstOrder.Language.quotientStructure` `setoidPrestructure` `Filter.Eventually`	—	`Fin.isEmpty'` `boundedFormula_realize_cast` `iff_eq_eq` `Unique.instSubsingleton`
`sentence_realize` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `Filter.Product` `Ultrafilter.toFilter` `structure` `Filter.Eventually`	—	`Empty.instIsEmpty` `realize_formula_cast` `iff_eq_eq` `Unique.instSubsingleton`
`term_realize_cast` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `Filter.productSetoid` `Ultrafilter.toFilter` `FirstOrder.Language.quotientStructure` `setoidPrestructure`	—	`FirstOrder.Language.Term.realize_quotient_mk'`

FirstOrder.Language.Ultraproduct.Product

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonempty` 📖	mathematical	—	`Filter.Product` `Ultrafilter.toFilter`	—	—

---

← Back to Index