Documentation Verification Report

Complexity

📁 Source: Mathlib/ModelTheory/Complexity.lean

Statistics

Metric	Count
Definitions `IsAtomic`, `IsExistential`, `IsPrenex`, `IsQF`, `IsUniversal`, `toPrenex`, `toPrenexImp`, `toPrenexImpRight`, `IsUniversal`	9
Theorems `castLE`, `isExistential`, `isPrenex`, `isQF`, `isUniversal`, `liftAt`, `realize_comp`, `realize_comp_of_injective`, `relabel`, `realize_embedding`, `castLE`, `induction_on_all_not`, `liftAt`, `relabel`, `castLE`, `induction_on_inf_not`, `induction_on_sup_not`, `inf`, `isExistential`, `isPrenex`, `isUniversal`, `liftAt`, `not`, `realize_embedding`, `relabel`, `sup`, `toPrenexImp`, `toPrenexImpRight`, `top`, `realize_embedding`, `iff_toPrenex`, `induction_on_all_ex`, `induction_on_exists_not`, `isPrenex_toPrenexImp`, `isPrenex_toPrenexImpRight`, `isQF_bot`, `not_all_isAtomic`, `not_all_isQF`, `not_ex_isAtomic`, `not_ex_isQF`, `realize_toPrenex`, `realize_toPrenexImp`, `realize_toPrenexImpRight`, `toPrenex_isPrenex`, `isAtomic_graph`, `isAtomic`, `isQF`, `isUniversal_antisymmetric`, `isUniversal_irreflexive`, `isUniversal_reflexive`, `isUniversal_symmetric`, `isUniversal_total`, `isUniversal_transitive`, `models_of_isUniversal`, `insert`, `isUniversal_of_mem`, `models_of_embedding`	57
Total	66

FirstOrder.Language.BoundedFormula

Definitions

Name	Category	Theorems
`IsAtomic` 📖	CompData	7 math math: `not_ex_isAtomic`, `FirstOrder.Language.Relations.isAtomic`, `FirstOrder.Language.Formula.isAtomic_graph`, `not_all_isAtomic`, `IsAtomic.castLE`, `IsAtomic.relabel`, `IsAtomic.liftAt`
`IsExistential` 📖	CompData	2 math math: `IsAtomic.isExistential`, `IsQF.isExistential`
`IsPrenex` 📖	CompData	8 math math: `IsAtomic.isPrenex`, `isPrenex_toPrenexImpRight`, `IsQF.isPrenex`, `toPrenex_isPrenex`, `IsPrenex.castLE`, `IsPrenex.relabel`, `IsPrenex.liftAt`, `isPrenex_toPrenexImp`
`IsQF` 📖	CompData	12 math math: `not_all_isQF`, `IsQF.inf`, `IsQF.sup`, `IsQF.relabel`, `IsQF.top`, `isQF_bot`, `IsQF.liftAt`, `IsQF.not`, `not_ex_isQF`, `FirstOrder.Language.Relations.isQF`, `IsQF.castLE`, `IsAtomic.isQF`
`IsUniversal` 📖	CompData	9 math math: `FirstOrder.Language.Relations.isUniversal_total`, `FirstOrder.Language.Relations.isUniversal_symmetric`, `FirstOrder.Language.Relations.isUniversal_irreflexive`, `IsQF.isUniversal`, `FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem`, `FirstOrder.Language.Relations.isUniversal_antisymmetric`, `IsAtomic.isUniversal`, `FirstOrder.Language.Relations.isUniversal_reflexive`, `FirstOrder.Language.Relations.isUniversal_transitive`
`toPrenex` 📖	CompOp	3 math math: `iff_toPrenex`, `realize_toPrenex`, `toPrenex_isPrenex`
`toPrenexImp` 📖	CompOp	3 math math: `realize_toPrenexImp`, `IsQF.toPrenexImp`, `isPrenex_toPrenexImp`
`toPrenexImpRight` 📖	CompOp	4 math math: `isPrenex_toPrenexImpRight`, `IsQF.toPrenexImpRight`, `IsQF.toPrenexImp`, `realize_toPrenexImpRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_toPrenex` 📖	mathematical	—	`FirstOrder.Language.Theory.Iff` `FirstOrder.Language.Theory` `Set.instEmptyCollection` `FirstOrder.Language.Sentence` `toPrenex`	—	`realize_iff` `realize_toPrenex` `FirstOrder.Language.Theory.ModelType.nonempty'`
`induction_on_all_ex` 📖	—	`all` `ex`	—	—	`iff_toPrenex` `toPrenex_isPrenex`
`induction_on_exists_not` 📖	—	`not` `ex`	—	—	`induction_on_all_ex` `all_iff_not_ex_not`
`isPrenex_toPrenexImp` 📖	mathematical	`IsPrenex`	`IsPrenex` `toPrenexImp`	—	`IsQF.toPrenexImp` `isPrenex_toPrenexImpRight` `IsPrenex.liftAt`
`isPrenex_toPrenexImpRight` 📖	mathematical	`IsQF` `IsPrenex`	`IsPrenex` `toPrenexImpRight`	—	`IsQF.toPrenexImpRight` `IsQF.isPrenex` `IsQF.liftAt`
`isQF_bot` 📖	mathematical	—	`IsQF` `Bot.bot` `FirstOrder.Language.BoundedFormula` `instBot`	—	—
`not_all_isAtomic` 📖	mathematical	—	`IsAtomic` `all`	—	—
`not_all_isQF` 📖	mathematical	—	`IsQF` `all`	—	`not_all_isAtomic`
`not_ex_isAtomic` 📖	mathematical	—	`IsAtomic` `ex`	—	—
`not_ex_isQF` 📖	mathematical	—	`IsQF` `ex`	—	`not_ex_isAtomic` `not_all_isQF`
`realize_toPrenex` 📖	mathematical	—	`Realize` `toPrenex`	—	`toPrenex.eq_4` `realize_toPrenexImp` `toPrenex_isPrenex` `realize_imp` `realize_all` `toPrenex.eq_5`
`realize_toPrenexImp` 📖	mathematical	`IsPrenex`	`Realize` `toPrenexImp` `imp`	—	`IsQF.toPrenexImp` `realize_toPrenexImpRight` `toPrenexImp.eq_def` `realize_ex` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `iff_isEquiv` `IsPrenex.liftAt` `Fin.snoc_comp_castSucc` `forall_imp_iff_exists_imp`
`realize_toPrenexImpRight` 📖	mathematical	`IsQF` `IsPrenex`	`Realize` `toPrenexImpRight` `imp`	—	`IsQF.toPrenexImpRight` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `iff_isEquiv` `IsQF.liftAt` `Fin.snoc_comp_castSucc` `toPrenexImpRight.eq_def` `realize_ex`
`toPrenex_isPrenex` 📖	mathematical	—	`IsPrenex` `toPrenex`	—	`IsQF.isPrenex` `isQF_bot` `IsAtomic.isPrenex` `isPrenex_toPrenexImp`

FirstOrder.Language.BoundedFormula.IsAtomic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castLE` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic`	`FirstOrder.Language.BoundedFormula.IsAtomic` `FirstOrder.Language.BoundedFormula.castLE`	—	—
`isExistential` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic`	`FirstOrder.Language.BoundedFormula.IsExistential`	—	`FirstOrder.Language.BoundedFormula.IsQF.isExistential` `isQF`
`isPrenex` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic`	`FirstOrder.Language.BoundedFormula.IsPrenex`	—	`FirstOrder.Language.BoundedFormula.IsQF.isPrenex` `isQF`
`isQF` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic`	`FirstOrder.Language.BoundedFormula.IsQF`	—	—
`isUniversal` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic`	`FirstOrder.Language.BoundedFormula.IsUniversal`	—	`FirstOrder.Language.BoundedFormula.IsQF.isUniversal` `isQF`
`liftAt` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic`	`FirstOrder.Language.BoundedFormula.IsAtomic` `FirstOrder.Language.BoundedFormula.liftAt`	—	—
`realize_comp` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic` `FirstOrder.Language.BoundedFormula.Realize`	`FirstOrder.Language.BoundedFormula.Realize` `DFunLike.coe`	—	`realize_comp_of_injective` `EmbeddingLike.injective`
`realize_comp_of_injective` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic` `DFunLike.coe` `FirstOrder.Language.BoundedFormula.Realize`	`FirstOrder.Language.BoundedFormula.Realize` `DFunLike.coe`	—	`FirstOrder.Language.HomClass.realize_term` `FirstOrder.Language.HomClass.map_rel`
`relabel` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsAtomic`	`FirstOrder.Language.BoundedFormula.IsAtomic` `FirstOrder.Language.BoundedFormula.relabel`	—	—

FirstOrder.Language.BoundedFormula.IsExistential

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_embedding` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsExistential` `FirstOrder.Language.BoundedFormula.Realize`	`FirstOrder.Language.BoundedFormula.Realize` `DFunLike.coe`	—	`FirstOrder.Language.BoundedFormula.IsQF.realize_embedding` `Fin.comp_snoc`

FirstOrder.Language.BoundedFormula.IsPrenex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castLE` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsPrenex`	`FirstOrder.Language.BoundedFormula.IsPrenex` `FirstOrder.Language.BoundedFormula.castLE`	—	`FirstOrder.Language.BoundedFormula.IsQF.isPrenex` `FirstOrder.Language.BoundedFormula.IsQF.castLE`
`induction_on_all_not` 📖	—	`FirstOrder.Language.BoundedFormula.IsPrenex` `FirstOrder.Language.BoundedFormula.all` `FirstOrder.Language.BoundedFormula.not`	—	—	—
`liftAt` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsPrenex`	`FirstOrder.Language.BoundedFormula.IsPrenex` `FirstOrder.Language.BoundedFormula.liftAt`	—	`FirstOrder.Language.BoundedFormula.IsQF.isPrenex` `FirstOrder.Language.BoundedFormula.IsQF.liftAt` `castLE`
`relabel` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsPrenex`	`FirstOrder.Language.BoundedFormula.IsPrenex` `FirstOrder.Language.BoundedFormula.relabel`	—	`FirstOrder.Language.BoundedFormula.IsQF.isPrenex` `FirstOrder.Language.BoundedFormula.IsQF.relabel` `FirstOrder.Language.BoundedFormula.relabel_all` `FirstOrder.Language.BoundedFormula.relabel_ex`

FirstOrder.Language.BoundedFormula.IsQF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castLE` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsQF` `FirstOrder.Language.BoundedFormula.castLE`	—	`FirstOrder.Language.BoundedFormula.isQF_bot` `FirstOrder.Language.BoundedFormula.IsAtomic.isQF` `FirstOrder.Language.BoundedFormula.IsAtomic.castLE`
`induction_on_inf_not` 📖	—	`FirstOrder.Language.BoundedFormula.IsQF` `Bot.bot` `FirstOrder.Language.BoundedFormula` `FirstOrder.Language.BoundedFormula.instBot` `FirstOrder.Language.BoundedFormula.instMin` `FirstOrder.Language.BoundedFormula.not`	—	—	`induction_on_sup_not` `FirstOrder.Language.BoundedFormula.sup_iff_not_inf_not`
`induction_on_sup_not` 📖	—	`FirstOrder.Language.BoundedFormula.IsQF` `Bot.bot` `FirstOrder.Language.BoundedFormula` `FirstOrder.Language.BoundedFormula.instBot` `FirstOrder.Language.BoundedFormula.instMax` `FirstOrder.Language.BoundedFormula.not`	—	—	`FirstOrder.Language.BoundedFormula.imp_iff_not_sup`
`inf` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsQF` `FirstOrder.Language.BoundedFormula` `FirstOrder.Language.BoundedFormula.instMin`	—	`not`
`isExistential` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsExistential`	—	—
`isPrenex` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsPrenex`	—	—
`isUniversal` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsUniversal`	—	—
`liftAt` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsQF` `FirstOrder.Language.BoundedFormula.liftAt`	—	`FirstOrder.Language.BoundedFormula.isQF_bot` `FirstOrder.Language.BoundedFormula.IsAtomic.isQF` `FirstOrder.Language.BoundedFormula.IsAtomic.liftAt`
`not` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsQF` `FirstOrder.Language.BoundedFormula.not`	—	`FirstOrder.Language.BoundedFormula.isQF_bot`
`realize_embedding` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.Realize` `DFunLike.coe`	—	`FirstOrder.Language.HomClass.realize_term` `FirstOrder.Language.StrongHomClass.homClass` `EmbeddingLike.injective` `FirstOrder.Language.StrongHomClass.map_rel`
`relabel` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsQF` `FirstOrder.Language.BoundedFormula.relabel`	—	`FirstOrder.Language.BoundedFormula.isQF_bot` `FirstOrder.Language.BoundedFormula.IsAtomic.isQF` `FirstOrder.Language.BoundedFormula.IsAtomic.relabel`
`sup` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.IsQF` `FirstOrder.Language.BoundedFormula` `FirstOrder.Language.BoundedFormula.instMax`	—	`not`
`toPrenexImp` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.toPrenexImp` `FirstOrder.Language.BoundedFormula.toPrenexImpRight`	—	—
`toPrenexImpRight` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsQF`	`FirstOrder.Language.BoundedFormula.toPrenexImpRight` `FirstOrder.Language.BoundedFormula.imp`	—	—
`top` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsQF` `Top.top` `FirstOrder.Language.BoundedFormula` `FirstOrder.Language.BoundedFormula.instTop`	—	`not` `FirstOrder.Language.BoundedFormula.isQF_bot`

FirstOrder.Language.BoundedFormula.IsUniversal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_embedding` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsUniversal` `FirstOrder.Language.BoundedFormula.Realize` `DFunLike.coe`	`FirstOrder.Language.BoundedFormula.Realize`	—	`FirstOrder.Language.BoundedFormula.IsQF.realize_embedding` `Fin.comp_snoc`

FirstOrder.Language.Formula

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAtomic_graph` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsAtomic` `graph`	—	—

FirstOrder.Language.Relations

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAtomic` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsAtomic` `boundedFormula`	—	—
`isQF` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsQF` `boundedFormula`	—	`FirstOrder.Language.BoundedFormula.IsAtomic.isQF` `isAtomic`
`isUniversal_antisymmetric` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsUniversal` `antisymmetric`	—	`FirstOrder.Language.BoundedFormula.IsQF.isUniversal` `isQF` `FirstOrder.Language.BoundedFormula.IsAtomic.isQF`
`isUniversal_irreflexive` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsUniversal` `irreflexive`	—	`FirstOrder.Language.BoundedFormula.IsQF.isUniversal` `FirstOrder.Language.BoundedFormula.IsQF.not` `FirstOrder.Language.BoundedFormula.IsAtomic.isQF` `isAtomic`
`isUniversal_reflexive` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsUniversal` `reflexive`	—	`FirstOrder.Language.BoundedFormula.IsQF.isUniversal` `isQF`
`isUniversal_symmetric` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsUniversal` `symmetric`	—	`FirstOrder.Language.BoundedFormula.IsQF.isUniversal` `isQF`
`isUniversal_total` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsUniversal` `total`	—	`FirstOrder.Language.BoundedFormula.IsQF.isUniversal` `FirstOrder.Language.BoundedFormula.IsQF.sup` `isQF`
`isUniversal_transitive` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.IsUniversal` `transitive`	—	`FirstOrder.Language.BoundedFormula.IsQF.isUniversal` `isQF`

FirstOrder.Language.Substructure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`models_of_isUniversal` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.Substructure` `SetLike.instMembership` `instSetLike` `inducedStructure`	—	`FirstOrder.Language.Theory.IsUniversal.models_of_embedding`

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
`IsUniversal` 📖	CompData	4 math math: `FirstOrder.Language.instIsUniversalLinearOrderTheory`, `IsUniversal.insert`, `FirstOrder.Language.instIsUniversalPreorderTheory`, `FirstOrder.Language.instIsUniversalPartialOrderTheory`

FirstOrder.Language.Theory.IsUniversal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`insert` 📖	mathematical	`FirstOrder.Language.BoundedFormula.IsUniversal`	`FirstOrder.Language.Theory.IsUniversal` `FirstOrder.Language.Sentence` `FirstOrder.Language.Theory` `Set.instInsert`	—	`isUniversal_of_mem`
`isUniversal_of_mem` 📖	mathematical	`FirstOrder.Language.Sentence` `FirstOrder.Language.Theory` `Set.instMembership`	`FirstOrder.Language.BoundedFormula.IsUniversal`	—	—
`models_of_embedding` 📖	mathematical	—	`FirstOrder.Language.Theory.Model`	—	`FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding` `FirstOrder.Language.Embedding.embeddingLike` `FirstOrder.Language.Embedding.strongHomClass` `isUniversal_of_mem` `Empty.instIsEmpty` `Fin.isEmpty'` `Unique.instSubsingleton` `FirstOrder.Language.Theory.realize_sentence_of_mem`

---

← Back to Index