Documentation Verification Report

Syntax

📁 Source: Mathlib/ModelTheory/Syntax.lean

Statistics

MetricCount
DefinitionsBoundedFormula, alls, castLE, constantsVarsEquiv, ex, exs, freeVarFinset, iInf, iSup, iff, instBot, instInhabited, instMax, instMin, instTop, liftAt, mapTermRel, mapTermRelEquiv, not, relabel, relabelAux, relabelEquiv, restrictFreeVar, subst, toFormula, term, equivSentence, graph, iAlls, iExs, iExsUnique, iInf, iSup, iff, imp, not, relabel, apply₁, apply₂, term, onBoundedFormula, onFormula, onSentence, onTerm, onBoundedFormula, onFormula, onSentence, onTerm, onTheory, antisymmetric, boundedFormula, boundedFormula₁, boundedFormula₂, formula, formula₁, formula₂, irreflexive, reflexive, symmetric, total, transitive, Sentence, cardGe, bdEqual, constantsToVars, constantsVarsEquiv, constantsVarsEquivLeft, equal, inhabitedOfConstant, inhabitedOfVar, instDecidableEq, liftAt, relabel, relabelEquiv, restrictVar, restrictVarLeft, subst, substFunc, varFinset, varFinsetLeft, varsToConstants, Theory, distinctConstantsTheory, infiniteTheory, nonemptyTheory, «term&_», «term_='_», «term_⇔_», «term_⟹_», «term∀'_», «term∃'_», «term∼_»
92
TheoremscastLE_castLE, castLE_comp_castLE, castLE_rfl, mapTermRelEquiv_apply, mapTermRelEquiv_symm_apply, mapTermRel_id_id_id, mapTermRel_mapTermRel, relabelAux_sumInl, relabel_all, relabel_bot, relabel_ex, relabel_falsum, relabel_imp, relabel_not, relabel_sumInl, sumElim_comp_relabelAux, equivSentence_inf, equivSentence_not, onBoundedFormula_apply, onBoundedFormula_symm, onBoundedFormula_symm_apply, onFormula_apply, onFormula_symm, onSentence_apply, onSentence_symm_apply, onTerm_apply, onTerm_symm_apply, comp_onBoundedFormula, comp_onTerm, id_onBoundedFormula, id_onTerm, mem_onTheory, constantsVarsEquivLeft_apply, constantsVarsEquivLeft_symm_apply, constantsVarsEquiv_apply, constantsVarsEquiv_symm_apply, relabelEquiv_apply, relabelEquiv_symm_apply, relabel_comp_relabel, relabel_id, relabel_id_eq_id, relabel_relabel, substFunc_term, directed_distinctConstantsTheory, distinctConstantsTheory_eq_iUnion, distinctConstantsTheory_mono, monotone_distinctConstantsTheory
47
Total139

FirstOrder

Definitions

NameCategoryTheorems
«term&_» 📖CompOp
«term_='_» 📖CompOp
«term_⇔_» 📖CompOp
«term_⟹_» 📖CompOp
«term∀'_» 📖CompOp
«term∃'_» 📖CompOp
«term∼_» 📖CompOp

FirstOrder.Language

Definitions

NameCategoryTheorems
BoundedFormula 📖CompData
60 mathmath: Theory.imp_inf, Theory.imp_sup_right, BoundedFormula.IsQF.inf, BoundedFormula.realize_foldr_imp, Theory.imp_inf_iff, BoundedFormula.IsQF.sup, BoundedFormula.realize_inf, skolem₁_Functions, Theory.Iff.instSymmBoundedFormula, Theory.imp_sup_left, BoundedFormula.IsQF.top, BoundedFormula.isQF_bot, Theory.bot_imp, BoundedFormula.instCountableSigmaNat, Theory.Iff.instIsTransBoundedFormula, BoundedFormula.sigmaImp_apply, BoundedFormula.realize_foldr_sup, BoundedFormula.relabel_bot, Formula.inf_iff_not_sup_not, Theory.inf_imp_left, Theory.inf_imp_right, BoundedFormula.realize_relabelEquiv, LHom.comp_onBoundedFormula, BoundedFormula.realize_bot, Theory.Imp.instIsTransBoundedFormula, card_functions_sum_skolem₁, BoundedFormula.realize_foldr_inf, Theory.Imp.instReflBoundedFormula, BoundedFormula.castLE_comp_castLE, LEquiv.onBoundedFormula_symm_apply, BoundedFormula.realize_top, LEquiv.onBoundedFormula_symm, BoundedFormula.mapTermRelEquiv_apply, BoundedFormula.inf_not_iff_bot, BoundedFormula.listEncode_sigma_injective, BoundedFormula.encoding_decode, BoundedFormula.encoding_encode, BoundedFormula.sup_not_iff_top, BoundedFormula.listDecode_encode_list, LHom.id_onBoundedFormula, BoundedFormula.imp_iff_not_sup, BoundedFormula.realize_constantsVarsEquiv, BoundedFormula.inf_iff_not_sup_not, BoundedFormula.mapTermRelEquiv_symm_apply, BoundedFormula.sigmaAll_apply, LEquiv.onBoundedFormula_apply, Formula.imp_iff_not_sup, BoundedFormula.sup_iff_not_inf_not, BoundedFormula.realize_mapTermRel_id, BoundedFormula.realize_sup, Theory.IsComplete.eq_complete_theory, Formula.sup_iff_not_inf_not, BoundedFormula.encoding_Γ, BoundedFormula.mapTermRel_mapTermRel, BoundedFormula.mapTermRel_id_id_id, Theory.Iff.instReflBoundedFormula, Theory.imp_top, BoundedFormula.card_le, Theory.sup_imp_iff, Theory.sup_imp
Sentence 📖CompOp
52 mathmath: Theory.CompleteType.compl_setOf_mem, Theory.CompleteType.mem_or_not_mem, directed_distinctConstantsTheory, Theory.models_iff_finset_models, CompleteType.isTopologicalBasis_range_typesWith, Theory.model_union_iff, Formula.equivSentence_not, LHom.mem_onTheory, Theory.IsMaximal.mem_or_not_mem, LEquiv.onSentence_apply, Theory.IsMaximal.mem_of_models, BoundedFormula.iff_toPrenex, Theory.CompleteType.mem_of_models, Theory.CompleteType.subset', Theory.model_singleton_iff, Theory.IsUniversal.insert, Formula.equivSentence_inf, distinctConstantsTheory_mono, Theory.models_formula_iff_onTheory_models_equivSentence, Formula.realize_equivSentence_symm_con, monotone_distinctConstantsTheory, Theory.isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset, Theory.model_insert_iff, Theory.model_iff_subset_completeTheory, Theory.CompleteType.formula_mem_typeOf, Theory.CompleteType.setOf_mem_eq_univ_iff, distinctConstantsTheory_eq_iUnion, Theory.IsMaximal.mem_iff_models, mem_completeTheory, Theory.isSatisfiable_empty, completeTheory.mem_or_not_mem, Theory.CompleteType.not_mem_iff, Theory.CompleteType.iInter_setOf_subset, Theory.CompleteType.setOf_subset_eq_empty_iff, Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite, Theory.CompleteType.mem_typeOf, Theory.CompleteType.setOf_subset_eq_univ_iff, Theory.CompleteType.toList_foldr_inf_mem, LEquiv.onSentence_symm_apply, Theory.CompleteType.instNonempty, model_empty, Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le, Theory.CompleteType.isMaximal, Theory.CompleteType.typesWith_inf, Theory.CompleteType.typesWith_top, Theory.completeTheory.subset, Theory.Model.union, Formula.realize_equivSentence_symm, Formula.realize_equivSentence, Theory.CompleteType.subset, Theory.models_iff_not_satisfiable, Theory.CompleteType.mem_typesWith_iff
Theory 📖CompOp
28 mathmath: directed_distinctConstantsTheory, Theory.model_union_iff, LHom.mem_onTheory, Theory.IsMaximal.mem_or_not_mem, Theory.IsMaximal.mem_of_models, BoundedFormula.iff_toPrenex, Theory.CompleteType.subset', Theory.model_singleton_iff, Theory.IsUniversal.insert, distinctConstantsTheory_mono, monotone_distinctConstantsTheory, Theory.model_insert_iff, Theory.model_iff_subset_completeTheory, Theory.IsMaximal.mem_iff_models, mem_completeTheory, Theory.isSatisfiable_empty, completeTheory.mem_or_not_mem, Theory.CompleteType.iInter_setOf_subset, Theory.CompleteType.setOf_subset_eq_empty_iff, Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite, Theory.CompleteType.setOf_subset_eq_univ_iff, Theory.CompleteType.instNonempty, model_empty, Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le, Theory.completeTheory.subset, Theory.Model.union, Theory.CompleteType.subset, Theory.models_iff_not_satisfiable
distinctConstantsTheory 📖CompOp
7 mathmath: directed_distinctConstantsTheory, distinctConstantsTheory_mono, monotone_distinctConstantsTheory, model_distinctConstantsTheory, distinctConstantsTheory_eq_iUnion, Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite, Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le
infiniteTheory 📖CompOp
3 mathmath: model_infiniteTheory, model_infiniteTheory_iff, Cardinal.empty_infinite_Theory_isComplete
nonemptyTheory 📖CompOp
2 mathmath: model_nonempty, model_nonemptyTheory_iff

Theorems

NameKindAssumesProvesValidatesDepends On
directed_distinctConstantsTheory 📖mathematicalDirected
Theory
withConstants
Set
Set.instHasSubset
Sentence
distinctConstantsTheory
Monotone.directed_le
OrderTop.instIsDirectedOrder
monotone_distinctConstantsTheory
distinctConstantsTheory_eq_iUnion 📖mathematicaldistinctConstantsTheory
Set.iUnion
Sentence
withConstants
Finset
Set.Elem
SetLike.coe
Finset.instSetLike
Finset.map
Set
Set.instMembership
Function.Embedding.subtype
Set.image_iUnion
Set.iUnion_inter
Set.ext
Finset.coe_map
Set.image_congr
distinctConstantsTheory_mono 📖mathematicalSet
Set.instHasSubset
Theory
withConstants
Sentence
distinctConstantsTheory
Set.image_mono
Set.inter_subset_inter
Set.prod_mono
subset_refl
Set.instReflSubset
monotone_distinctConstantsTheory 📖mathematicalMonotone
Set
Theory
withConstants
PartialOrder.toPreorder
OmegaCompletePartialOrder.toPartialOrder
CompleteLattice.instOmegaCompletePartialOrder
CompleteBooleanAlgebra.toCompleteLattice
CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra
Set.instCompleteAtomicBooleanAlgebra
Sentence
distinctConstantsTheory
distinctConstantsTheory_mono

FirstOrder.Language.BoundedFormula

Definitions

NameCategoryTheorems
alls 📖CompOp
1 mathmath: realize_alls
castLE 📖CompOp
9 mathmath: castLE_castLE, castLE_rfl, castLE_comp_castLE, IsPrenex.castLE, IsAtomic.castLE, realize_mapTermRel_add_castLe, relabel_sumInl, IsQF.castLE, realize_castLE_of_eq
constantsVarsEquiv 📖CompOp
1 mathmath: realize_constantsVarsEquiv
ex 📖CompOp
7 mathmath: not_ex_isAtomic, ex_iff_not_all_not, relabel_ex, realize_ex, not_ex_isQF, FirstOrder.Language.Theory.Iff.ex, all_iff_not_ex_not
exs 📖CompOp
1 mathmath: realize_exs
freeVarFinset 📖CompOp
iInf 📖CompOp
1 mathmath: realize_iInf
iSup 📖CompOp
1 mathmath: realize_iSup
iff 📖CompOp
1 mathmath: realize_iff
instBot 📖CompOp
7 mathmath: FirstOrder.Language.Formula.realize_bot, isQF_bot, FirstOrder.Language.Theory.bot_imp, realize_foldr_sup, relabel_bot, realize_bot, inf_not_iff_bot
instInhabited 📖CompOp
instMax 📖CompOp
15 mathmath: FirstOrder.Language.Theory.imp_sup_right, IsQF.sup, FirstOrder.Language.Theory.imp_sup_left, realize_foldr_sup, FirstOrder.Language.Formula.inf_iff_not_sup_not, sup_not_iff_top, imp_iff_not_sup, FirstOrder.Language.Formula.realize_sup, inf_iff_not_sup_not, FirstOrder.Language.Formula.imp_iff_not_sup, sup_iff_not_inf_not, realize_sup, FirstOrder.Language.Formula.sup_iff_not_inf_not, FirstOrder.Language.Theory.sup_imp_iff, FirstOrder.Language.Theory.sup_imp
instMin 📖CompOp
16 mathmath: FirstOrder.Language.Theory.imp_inf, IsQF.inf, FirstOrder.Language.Theory.imp_inf_iff, realize_inf, FirstOrder.Language.Formula.inf_iff_not_sup_not, FirstOrder.Language.Formula.equivSentence_inf, FirstOrder.Language.Theory.inf_imp_left, FirstOrder.Language.Theory.inf_imp_right, realize_foldr_inf, inf_not_iff_bot, FirstOrder.Language.Formula.realize_inf, inf_iff_not_sup_not, FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem, sup_iff_not_inf_not, FirstOrder.Language.Formula.sup_iff_not_inf_not, FirstOrder.Language.Theory.CompleteType.typesWith_inf
instTop 📖CompOp
8 mathmath: IsQF.top, realize_foldr_inf, realize_top, sup_not_iff_top, FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem, FirstOrder.Language.Formula.realize_top, FirstOrder.Language.Theory.CompleteType.typesWith_top, FirstOrder.Language.Theory.imp_top
liftAt 📖CompOp
8 mathmath: iff_all_liftAt, realize_liftAt_one, IsQF.liftAt, realize_liftAt_one_self, realize_all_liftAt_one_self, IsAtomic.liftAt, realize_liftAt, IsPrenex.liftAt
mapTermRel 📖CompOp
6 mathmath: mapTermRelEquiv_apply, mapTermRelEquiv_symm_apply, realize_mapTermRel_add_castLe, realize_mapTermRel_id, mapTermRel_mapTermRel, mapTermRel_id_id_id
mapTermRelEquiv 📖CompOp
2 mathmath: mapTermRelEquiv_apply, mapTermRelEquiv_symm_apply
not 📖CompOp
13 mathmath: ex_iff_not_all_not, relabel_not, realize_not, IsQF.not, inf_not_iff_bot, iff_not_not, sup_not_iff_top, imp_iff_not_sup, all_iff_not_ex_not, inf_iff_not_sup_not, sup_iff_not_inf_not, FirstOrder.Language.Theory.Iff.not, FirstOrder.Language.Theory.CompleteType.typesWith_not
relabel 📖CompOp
12 mathmath: relabel_ex, relabel_not, IsQF.relabel, relabel_imp, relabel_all, FirstOrder.Language.Formula.realize_relabel_sumInr, relabel_bot, realize_relabel, relabel_falsum, IsPrenex.relabel, IsAtomic.relabel, relabel_sumInl
relabelAux 📖CompOp
2 mathmath: relabelAux_sumInl, sumElim_comp_relabelAux
relabelEquiv 📖CompOp
1 mathmath: realize_relabelEquiv
restrictFreeVar 📖CompOp
2 mathmath: realize_restrictFreeVar', realize_restrictFreeVar
subst 📖CompOp
1 mathmath: realize_subst
toFormula 📖CompOp
2 mathmath: FirstOrder.Language.Theory.models_toFormula_iff, realize_toFormula

Theorems

NameKindAssumesProvesValidatesDepends On
castLE_castLE 📖mathematicalcastLE
LE.le.trans
Nat.instPreorder
LE.le.trans
FirstOrder.Language.Term.relabel_relabel
Function.comp_assoc
FirstOrder.Language.Term.relabel_comp_relabel
castLE_comp_castLE 📖mathematicalFirstOrder.Language.BoundedFormula
castLE
LE.le.trans
Nat.instPreorder
LE.le.trans
castLE_castLE
castLE_rfl 📖mathematicalcastLEFirstOrder.Language.Term.relabel_id_eq_id
mapTermRelEquiv_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.BoundedFormula
EquivLike.toFunLike
Equiv.instEquivLike
mapTermRelEquiv
mapTermRel
FirstOrder.Language.Term
FirstOrder.Language.Relations
mapTermRelEquiv_symm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.BoundedFormula
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
mapTermRelEquiv
mapTermRel
FirstOrder.Language.Term
FirstOrder.Language.Relations
mapTermRel_id_id_id 📖mathematicalmapTermRel
FirstOrder.Language.Term
FirstOrder.Language.Relations
FirstOrder.Language.BoundedFormula
mapTermRel_mapTermRel 📖mathematicalmapTermRel
FirstOrder.Language.BoundedFormula
FirstOrder.Language.Term
FirstOrder.Language.Relations
relabelAux_sumInl 📖mathematicalrelabelAux
relabel_all 📖mathematicalrelabel
all
relabel.eq_1
mapTermRel.eq_5
castLE_rfl
relabel_bot 📖mathematicalrelabel
Bot.bot
FirstOrder.Language.BoundedFormula
instBot
relabel_ex 📖mathematicalrelabel
ex
relabel_not
relabel_all
relabel_falsum 📖mathematicalrelabel
falsum
relabel_imp 📖mathematicalrelabel
imp
relabel_not 📖mathematicalrelabel
not
relabel_sumInl 📖mathematicalrelabel
castLE
AddZero.toAdd
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
Nat.instAddMonoid
AddZero.toZero
ge_of_eq
Nat.instPreorder
zero_add
ge_of_eq
zero_add
relabelAux_sumInl
castLE.congr_simp
castLE_rfl
sumElim_comp_relabelAux 📖mathematicalrelabelAux

FirstOrder.Language.Constants

Definitions

NameCategoryTheorems
term 📖CompOp
4 mathmath: FirstOrder.Language.Term.realize_constants, FirstOrder.Language.Term.realize_con, FirstOrder.Ring.one_def, FirstOrder.Ring.zero_def

FirstOrder.Language.Formula

Definitions

NameCategoryTheorems
equivSentence 📖CompOp
8 mathmath: equivSentence_not, equivSentence_inf, FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence, realize_equivSentence_symm_con, FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf, FirstOrder.Language.Theory.CompleteType.mem_typeOf, realize_equivSentence_symm, realize_equivSentence
graph 📖CompOp
2 mathmath: realize_graph, isAtomic_graph
iAlls 📖CompOp
2 mathmath: realize_iAlls, FirstOrder.Language.BoundedFormula.realize_iAlls
iExs 📖CompOp
2 mathmath: FirstOrder.Language.BoundedFormula.realize_iExs, realize_iExs
iExsUnique 📖CompOp
2 mathmath: FirstOrder.Language.BoundedFormula.realize_iExsUnique, realize_iExsUnique
iInf 📖CompOp
1 mathmath: realize_iInf
iSup 📖CompOp
1 mathmath: realize_iSup
iff 📖CompOp
1 mathmath: realize_iff
imp 📖CompOp
2 mathmath: imp_iff_not_sup, realize_imp
not 📖CompOp
14 mathmath: FirstOrder.Language.Theory.CompleteType.compl_setOf_mem, FirstOrder.Language.Theory.CompleteType.mem_or_not_mem, iff_not_not, equivSentence_not, FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem, FirstOrder.Language.Sentence.realize_not, inf_iff_not_sup_not, FirstOrder.Language.Theory.IsComplete.models_not_iff, FirstOrder.Language.completeTheory.mem_or_not_mem, realize_not, FirstOrder.Language.Theory.CompleteType.not_mem_iff, imp_iff_not_sup, sup_iff_not_inf_not, FirstOrder.Language.Theory.models_iff_not_satisfiable
relabel 📖CompOp
1 mathmath: realize_relabel

Theorems

NameKindAssumesProvesValidatesDepends On
equivSentence_inf 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Formula
FirstOrder.Language.Sentence
FirstOrder.Language.withConstants
EquivLike.toFunLike
Equiv.instEquivLike
equivSentence
FirstOrder.Language.BoundedFormula.instMin
equivSentence_not 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Formula
FirstOrder.Language.Sentence
FirstOrder.Language.withConstants
EquivLike.toFunLike
Equiv.instEquivLike
equivSentence
not

FirstOrder.Language.Functions

Definitions

NameCategoryTheorems
apply₁ 📖CompOp
2 mathmath: FirstOrder.Ring.neg_def, FirstOrder.Language.Term.realize_functions_apply₁
apply₂ 📖CompOp
3 mathmath: FirstOrder.Ring.mul_def, FirstOrder.Ring.add_def, FirstOrder.Language.Term.realize_functions_apply₂
term 📖CompOp
2 mathmath: FirstOrder.Language.Term.realize_function_term, FirstOrder.Language.Term.substFunc_term

FirstOrder.Language.LEquiv

Definitions

NameCategoryTheorems
onBoundedFormula 📖CompOp
3 mathmath: onBoundedFormula_symm_apply, onBoundedFormula_symm, onBoundedFormula_apply
onFormula 📖CompOp
2 mathmath: onFormula_apply, onFormula_symm
onSentence 📖CompOp
2 mathmath: onSentence_apply, onSentence_symm_apply
onTerm 📖CompOp
2 mathmath: onTerm_symm_apply, onTerm_apply

Theorems

NameKindAssumesProvesValidatesDepends On
onBoundedFormula_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.BoundedFormula
EquivLike.toFunLike
Equiv.instEquivLike
onBoundedFormula
FirstOrder.Language.LHom.onBoundedFormula
toLHom
onBoundedFormula_symm 📖mathematicalEquiv.symm
FirstOrder.Language.BoundedFormula
onBoundedFormula
symm
onBoundedFormula_symm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.BoundedFormula
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
onBoundedFormula
FirstOrder.Language.LHom.onBoundedFormula
invLHom
onFormula_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Formula
EquivLike.toFunLike
Equiv.instEquivLike
onFormula
FirstOrder.Language.LHom.onFormula
toLHom
onFormula_symm 📖mathematicalEquiv.symm
FirstOrder.Language.Formula
onFormula
symm
onSentence_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Sentence
EquivLike.toFunLike
Equiv.instEquivLike
onSentence
FirstOrder.Language.LHom.onBoundedFormula
toLHom
onSentence_symm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Sentence
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
onSentence
FirstOrder.Language.LHom.onBoundedFormula
invLHom
onTerm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
EquivLike.toFunLike
Equiv.instEquivLike
onTerm
FirstOrder.Language.LHom.onTerm
toLHom
onTerm_symm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
onTerm
FirstOrder.Language.LHom.onTerm
invLHom

FirstOrder.Language.LHom

Definitions

NameCategoryTheorems
onBoundedFormula 📖CompOp
7 mathmath: realize_onBoundedFormula, FirstOrder.Language.LEquiv.onSentence_apply, comp_onBoundedFormula, FirstOrder.Language.LEquiv.onBoundedFormula_symm_apply, id_onBoundedFormula, FirstOrder.Language.LEquiv.onBoundedFormula_apply, FirstOrder.Language.LEquiv.onSentence_symm_apply
onFormula 📖CompOp
3 mathmath: setOf_realize_onFormula, FirstOrder.Language.LEquiv.onFormula_apply, realize_onFormula
onSentence 📖CompOp
2 mathmath: mem_onTheory, realize_onSentence
onTerm 📖CompOp
5 mathmath: FirstOrder.Language.LEquiv.onTerm_symm_apply, comp_onTerm, realize_onTerm, FirstOrder.Language.LEquiv.onTerm_apply, id_onTerm
onTheory 📖CompOp
15 mathmath: FirstOrder.Language.Theory.ModelType.defaultExpansion_Carrier, FirstOrder.Language.Theory.ModelType.defaultExpansion_struc, mem_onTheory, FirstOrder.Language.Theory.CompleteType.subset', FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence, FirstOrder.Language.Theory.isSatisfiable_onTheory_iff, FirstOrder.Language.Theory.CompleteType.setOf_mem_eq_univ_iff, FirstOrder.Language.Theory.ModelType.reduct_struc, FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff, FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite, FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_univ_iff, onTheory_model, FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le, FirstOrder.Language.Theory.ModelType.reduct_Carrier, FirstOrder.Language.Theory.CompleteType.subset

Theorems

NameKindAssumesProvesValidatesDepends On
comp_onBoundedFormula 📖mathematicalonBoundedFormula
comp
FirstOrder.Language.BoundedFormula
comp_onTerm
comp_onTerm 📖mathematicalonTerm
comp
FirstOrder.Language.Term
id_onBoundedFormula 📖mathematicalonBoundedFormula
id
FirstOrder.Language.BoundedFormula
onBoundedFormula.eq_2
id_onTerm
FirstOrder.Language.Term.bdEqual.eq_1
onBoundedFormula.eq_3
onBoundedFormula.eq_4
onBoundedFormula.eq_5
id_onTerm 📖mathematicalonTerm
id
FirstOrder.Language.Term
mem_onTheory 📖mathematicalFirstOrder.Language.Sentence
FirstOrder.Language.Theory
Set.instMembership
onTheory
onSentence
Set.mem_image

FirstOrder.Language.Relations

Definitions

NameCategoryTheorems
antisymmetric 📖CompOp
2 mathmath: isUniversal_antisymmetric, realize_antisymmetric
boundedFormula 📖CompOp
3 mathmath: isAtomic, FirstOrder.Language.BoundedFormula.realize_rel, isQF
boundedFormula₁ 📖CompOp
1 mathmath: FirstOrder.Language.BoundedFormula.realize_rel₁
boundedFormula₂ 📖CompOp
1 mathmath: FirstOrder.Language.BoundedFormula.realize_rel₂
formula 📖CompOp
1 mathmath: FirstOrder.Language.Formula.realize_rel
formula₁ 📖CompOp
1 mathmath: FirstOrder.Language.Formula.realize_rel₁
formula₂ 📖CompOp
1 mathmath: FirstOrder.Language.Formula.realize_rel₂
irreflexive 📖CompOp
2 mathmath: isUniversal_irreflexive, realize_irreflexive
reflexive 📖CompOp
2 mathmath: isUniversal_reflexive, realize_reflexive
symmetric 📖CompOp
2 mathmath: isUniversal_symmetric, realize_symmetric
total 📖CompOp
2 mathmath: isUniversal_total, realize_total
transitive 📖CompOp
2 mathmath: realize_transitive, isUniversal_transitive

FirstOrder.Language.Sentence

Definitions

NameCategoryTheorems
cardGe 📖CompOp
1 mathmath: realize_cardGe

FirstOrder.Language.Term

Definitions

NameCategoryTheorems
bdEqual 📖CompOp
1 mathmath: FirstOrder.Language.BoundedFormula.realize_bdEqual
constantsToVars 📖CompOp
3 mathmath: constantsVarsEquivLeft_apply, realize_constantsToVars, constantsVarsEquiv_apply
constantsVarsEquiv 📖CompOp
2 mathmath: constantsVarsEquiv_symm_apply, constantsVarsEquiv_apply
constantsVarsEquivLeft 📖CompOp
3 mathmath: constantsVarsEquivLeft_apply, constantsVarsEquivLeft_symm_apply, realize_constantsVarsEquivLeft
equal 📖CompOp
1 mathmath: FirstOrder.Language.Formula.realize_equal
inhabitedOfConstant 📖CompOp
inhabitedOfVar 📖CompOp
instDecidableEq 📖CompOp
liftAt 📖CompOp
1 mathmath: realize_liftAt
relabel 📖CompOp
9 mathmath: constantsVarsEquivLeft_apply, realize_relabel, constantsVarsEquivLeft_symm_apply, relabelEquiv_symm_apply, relabel_id_eq_id, relabel_comp_relabel, relabel_id, relabelEquiv_apply, relabel_relabel
relabelEquiv 📖CompOp
2 mathmath: relabelEquiv_symm_apply, relabelEquiv_apply
restrictVar 📖CompOp
2 mathmath: realize_restrictVar, realize_restrictVar'
restrictVarLeft 📖CompOp
2 mathmath: realize_restrictVarLeft', realize_restrictVarLeft
subst 📖CompOp
1 mathmath: realize_subst
substFunc 📖CompOp
2 mathmath: realize_substFunc, substFunc_term
varFinset 📖CompOp
varFinsetLeft 📖CompOp
varsToConstants 📖CompOp
3 mathmath: constantsVarsEquiv_symm_apply, constantsVarsEquivLeft_symm_apply, realize_varsToConstants

Theorems

NameKindAssumesProvesValidatesDepends On
constantsVarsEquivLeft_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
FirstOrder.Language.withConstants
EquivLike.toFunLike
Equiv.instEquivLike
constantsVarsEquivLeft
relabel
Equiv.symm
Equiv.sumAssoc
constantsToVars
constantsVarsEquivLeft_symm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
FirstOrder.Language.withConstants
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
constantsVarsEquivLeft
varsToConstants
relabel
Equiv.sumAssoc
constantsVarsEquiv_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
FirstOrder.Language.withConstants
EquivLike.toFunLike
Equiv.instEquivLike
constantsVarsEquiv
constantsToVars
constantsVarsEquiv_symm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
FirstOrder.Language.withConstants
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
constantsVarsEquiv
varsToConstants
relabelEquiv_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
EquivLike.toFunLike
Equiv.instEquivLike
relabelEquiv
relabel
relabelEquiv_symm_apply 📖mathematicalDFunLike.coe
Equiv
FirstOrder.Language.Term
EquivLike.toFunLike
Equiv.instEquivLike
Equiv.symm
relabelEquiv
relabel
relabel_comp_relabel 📖mathematicalFirstOrder.Language.Term
relabel
relabel_relabel
relabel_id 📖mathematicalrelabel
relabel_id_eq_id 📖mathematicalrelabel
FirstOrder.Language.Term
relabel_id
relabel_relabel 📖mathematicalrelabel
substFunc_term 📖mathematicalsubstFunc
FirstOrder.Language.Functions.term

---

← Back to Index