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	4 math math: not_ex_isAtomic, FirstOrder.Language.Relations.isAtomic, FirstOrder.Language.Formula.isAtomic_graph, not_all_isAtomic
IsExistential 📖	CompData	2 math math: IsAtomic.isExistential, IsQF.isExistential
IsPrenex 📖	CompData	3 math math: IsAtomic.isPrenex, IsQF.isPrenex, toPrenex_isPrenex
IsQF 📖	CompData	6 math math: not_all_isQF, IsQF.top, isQF_bot, not_ex_isQF, FirstOrder.Language.Relations.isQF, 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	toPrenexImp	—	IsQF.toPrenexImp isPrenex_toPrenexImpRight IsPrenex.liftAt
isPrenex_toPrenexImpRight 📖	mathematical	IsQF 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.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.liftAt	—	—
realize_comp 📖	mathematical	FirstOrder.Language.BoundedFormula.IsAtomic FirstOrder.Language.BoundedFormula.Realize	DFunLike.coe	—	realize_comp_of_injective EmbeddingLike.injective
realize_comp_of_injective 📖	—	FirstOrder.Language.BoundedFormula.IsAtomic DFunLike.coe FirstOrder.Language.BoundedFormula.Realize	—	—	FirstOrder.Language.HomClass.realize_term FirstOrder.Language.HomClass.map_rel
relabel 📖	mathematical	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	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.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.liftAt	—	FirstOrder.Language.BoundedFormula.IsQF.isPrenex FirstOrder.Language.BoundedFormula.IsQF.liftAt castLE
relabel 📖	mathematical	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.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 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.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.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.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 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 📖	—	FirstOrder.Language.BoundedFormula.IsUniversal FirstOrder.Language.BoundedFormula.Realize DFunLike.coe	—	—	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