Types

📁 Source: Mathlib/ModelTheory/Types.lean

Statistics

Metric	Count
Definitions CompleteType, instSetLike, instPartialOrder, toTheory, typesWith, realizedTypes, typeOf	7
Theorems compl_setOf_mem, false_of_mem_of_not_mem, formula_mem_typeOf, iInter_setOf_subset, instNonempty, isMaximal, isMaximal', mem_of_models, mem_or_not_mem, mem_typeOf, mem_typesWith_iff, nonempty_iff, not_mem_iff, setOf_mem_eq_univ_iff, setOf_subset_eq_empty_iff, setOf_subset_eq_univ_iff, subset, subset', toList_foldr_inf_mem, typesWith_eq_univ_of_mem_onTheory_lhomWithConstants, typesWith_inf, typesWith_not, typesWith_top, exists_modelType_is_realized_in	24
Total	31

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
CompleteType 📖	CompData	26 math math: CompleteType.compl_setOf_mem, CompleteType.mem_or_not_mem, CompleteType.nonempty_iff, CompleteType.isTopologicalBasis_range_typesWith, CompleteType.isOpen_typesWith, CompleteType.isClosed_typesWith, CompleteType.mem_of_models, CompleteType.instTotallySeparatedSpaceCompleteType, CompleteType.typesWith_eq_univ_of_mem_onTheory_lhomWithConstants, CompleteType.formula_mem_typeOf, CompleteType.setOf_mem_eq_univ_iff, CompleteType.not_mem_iff, CompleteType.iInter_setOf_subset, CompleteType.setOf_subset_eq_empty_iff, CompleteType.mem_typeOf, CompleteType.setOf_subset_eq_univ_iff, CompleteType.toList_foldr_inf_mem, CompleteType.instNonempty, CompleteType.typesWith_not, CompleteType.isMaximal, CompleteType.isClopen_typesWith, CompleteType.typesWith_inf, CompleteType.typesWith_top, exists_modelType_is_realized_in, CompleteType.subset, CompleteType.mem_typesWith_iff
realizedTypes 📖	CompOp	1 math math: exists_modelType_is_realized_in
typeOf 📖	CompOp	2 math math: CompleteType.formula_mem_typeOf, CompleteType.mem_typeOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_modelType_is_realized_in 📖	mathematical	—	CompleteType Set Set.instMembership realizedTypes ModelType.Carrier ModelType.struc ModelType.nonempty' ModelType.is_model	—	ModelType.nonempty' ModelType.is_model CompleteType.isMaximal CompleteType.subset SetLike.ext FirstOrder.Language.Formula.realize_equivSentence_symm_con FirstOrder.Language.LHom.isExpansionOn_reduct trans IsPreorder.toIsTrans IsEquiv.toIsPreorder iff_isEquiv IsComplete.realize_sentence_iff IsMaximal.isComplete IsMaximal.mem_iff_models

FirstOrder.Language.Theory.CompleteType

Definitions

Name	Category	Theorems
instPartialOrder 📖	CompOp	—
toTheory 📖	CompOp	2 math math: subset', isMaximal'
typesWith 📖	CompOp	9 math math: CompleteType.isTopologicalBasis_range_typesWith, CompleteType.isOpen_typesWith, CompleteType.isClosed_typesWith, typesWith_eq_univ_of_mem_onTheory_lhomWithConstants, typesWith_not, CompleteType.isClopen_typesWith, typesWith_inf, typesWith_top, mem_typesWith_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_setOf_mem 📖	mathematical	—	Compl.compl Set FirstOrder.Language.Theory.CompleteType Set.instCompl setOf FirstOrder.Language.Sentence FirstOrder.Language.withConstants SetLike.instMembership Sentence.instSetLike FirstOrder.Language.Formula FirstOrder.Language.Formula.not	—	Set.ext not_mem_iff
false_of_mem_of_not_mem 📖	—	FirstOrder.Language.Sentence FirstOrder.Language.Theory Set.instMembership FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.not	—	—	FirstOrder.Language.Theory.Model.realize_of_mem FirstOrder.Language.Theory.ModelType.is_model
formula_mem_typeOf 📖	mathematical	—	FirstOrder.Language.Sentence FirstOrder.Language.withConstants FirstOrder.Language.Theory.CompleteType SetLike.instMembership Sentence.instSetLike FirstOrder.Language.Theory.typeOf DFunLike.coe Equiv FirstOrder.Language.Formula EquivLike.toFunLike Equiv.instEquivLike FirstOrder.Language.Formula.equivSentence FirstOrder.Language.Formula.Realize	—	Equiv.symm_apply_apply
iInter_setOf_subset 📖	mathematical	—	Set.iInter FirstOrder.Language.Theory.CompleteType setOf FirstOrder.Language.Theory FirstOrder.Language.withConstants Set.instHasSubset FirstOrder.Language.Sentence SetLike.coe Sentence.instSetLike Set Set.iUnion	—	Set.ext
instNonempty 📖	mathematical	—	FirstOrder.Language.Theory.CompleteType FirstOrder.Language.Theory Set.instEmptyCollection FirstOrder.Language.Sentence	—	nonempty_iff FirstOrder.Language.Theory.isSatisfiable_empty
isMaximal 📖	mathematical	—	FirstOrder.Language.Theory.IsMaximal FirstOrder.Language.withConstants SetLike.coe FirstOrder.Language.Theory.CompleteType FirstOrder.Language.Sentence Sentence.instSetLike	—	isMaximal'
isMaximal' 📖	mathematical	—	FirstOrder.Language.Theory.IsMaximal FirstOrder.Language.withConstants toTheory	—	—
mem_of_models 📖	mathematical	FirstOrder.Language.Theory.ModelsBoundedFormula FirstOrder.Language.withConstants FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants	FirstOrder.Language.Sentence FirstOrder.Language.Theory.CompleteType SetLike.instMembership Sentence.instSetLike	—	mem_or_not_mem FirstOrder.Language.Theory.models_iff_not_satisfiable FirstOrder.Language.Theory.IsSatisfiable.mono isMaximal Set.union_subset subset Set.singleton_subset_iff
mem_or_not_mem 📖	mathematical	—	FirstOrder.Language.Sentence FirstOrder.Language.withConstants FirstOrder.Language.Theory.CompleteType SetLike.instMembership Sentence.instSetLike FirstOrder.Language.Formula FirstOrder.Language.Formula.not	—	FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem isMaximal
mem_typeOf 📖	mathematical	—	FirstOrder.Language.Sentence FirstOrder.Language.withConstants FirstOrder.Language.Theory.CompleteType SetLike.instMembership Sentence.instSetLike FirstOrder.Language.Theory.typeOf FirstOrder.Language.Formula.Realize DFunLike.coe Equiv FirstOrder.Language.Formula EquivLike.toFunLike Equiv.instEquivLike Equiv.symm FirstOrder.Language.Formula.equivSentence	—	FirstOrder.Language.mem_completeTheory FirstOrder.Language.Formula.realize_equivSentence_symm
mem_typesWith_iff 📖	mathematical	—	FirstOrder.Language.Theory.CompleteType Set Set.instMembership typesWith FirstOrder.Language.Sentence FirstOrder.Language.withConstants SetLike.instMembership Sentence.instSetLike	—	—
nonempty_iff 📖	mathematical	—	FirstOrder.Language.Theory.CompleteType FirstOrder.Language.Theory.IsSatisfiable	—	FirstOrder.Language.Theory.isSatisfiable_onTheory_iff FirstOrder.Language.lhomWithConstants_injective Set.nonempty_iff_univ_nonempty Set.nonempty_iff_ne_empty not_iff_comm Set.union_empty setOf_subset_eq_empty_iff
not_mem_iff 📖	mathematical	—	FirstOrder.Language.Formula FirstOrder.Language.withConstants FirstOrder.Language.Theory.CompleteType SetLike.instMembership FirstOrder.Language.Sentence Sentence.instSetLike FirstOrder.Language.Formula.not	—	FirstOrder.Language.Theory.IsSatisfiable.mono isMaximal Set.insert_subset_iff Set.singleton_subset_iff mem_or_not_mem
setOf_mem_eq_univ_iff 📖	mathematical	—	setOf FirstOrder.Language.Theory.CompleteType FirstOrder.Language.Sentence FirstOrder.Language.withConstants SetLike.instMembership Sentence.instSetLike Set.univ FirstOrder.Language.Theory.ModelsBoundedFormula FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants	—	FirstOrder.Language.Theory.models_iff_not_satisfiable Set.compl_empty_iff compl_setOf_mem setOf_subset_eq_empty_iff
setOf_subset_eq_empty_iff 📖	mathematical	—	setOf FirstOrder.Language.Theory.CompleteType FirstOrder.Language.Theory FirstOrder.Language.withConstants Set.instHasSubset FirstOrder.Language.Sentence SetLike.coe Sentence.instSetLike Set Set.instEmptyCollection FirstOrder.Language.Theory.IsSatisfiable Set.instUnion FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants	—	iff_not_comm Set.not_nonempty_iff_eq_empty Set.Nonempty.eq_1 HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left FirstOrder.Language.Theory.completeTheory.subset FirstOrder.Language.Theory.ModelType.is_model FirstOrder.Language.completeTheory.isMaximal FirstOrder.Language.Theory.ModelType.nonempty' Set.subset_union_right FirstOrder.Language.Theory.IsSatisfiable.mono isMaximal Set.union_subset subset
setOf_subset_eq_univ_iff 📖	mathematical	—	setOf FirstOrder.Language.Theory.CompleteType FirstOrder.Language.Theory FirstOrder.Language.withConstants Set.instHasSubset FirstOrder.Language.Sentence SetLike.coe Sentence.instSetLike Set.univ FirstOrder.Language.Theory.ModelsBoundedFormula FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants	—	Set.ext Set.sInter_image
subset 📖	mathematical	—	FirstOrder.Language.Theory FirstOrder.Language.withConstants Set.instHasSubset FirstOrder.Language.Sentence FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants SetLike.coe FirstOrder.Language.Theory.CompleteType Sentence.instSetLike	—	subset'
subset' 📖	mathematical	—	FirstOrder.Language.Theory FirstOrder.Language.withConstants Set.instHasSubset FirstOrder.Language.Sentence FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants toTheory	—	—
toList_foldr_inf_mem 📖	mathematical	—	FirstOrder.Language.Sentence FirstOrder.Language.withConstants FirstOrder.Language.Theory.CompleteType SetLike.instMembership Sentence.instSetLike FirstOrder.Language.BoundedFormula.instMin Top.top FirstOrder.Language.BoundedFormula.instTop Finset.toList Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike	—	FirstOrder.Language.Theory.IsMaximal.mem_iff_models isMaximal Empty.instIsEmpty Fin.isEmpty'
typesWith_eq_univ_of_mem_onTheory_lhomWithConstants 📖	mathematical	FirstOrder.Language.Sentence FirstOrder.Language.withConstants FirstOrder.Language.Theory Set.instMembership FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants	typesWith Set.univ FirstOrder.Language.Theory.CompleteType	—	Set.univ_subset_iff subset
typesWith_inf 📖	mathematical	—	typesWith FirstOrder.Language.Sentence FirstOrder.Language.withConstants FirstOrder.Language.BoundedFormula.instMin Set FirstOrder.Language.Theory.CompleteType Set.instInter	—	Set.ext FirstOrder.Language.Theory.IsMaximal.mem_iff_models isMaximal FirstOrder.Language.BoundedFormula.realize_inf
typesWith_not 📖	mathematical	—	typesWith FirstOrder.Language.BoundedFormula.not FirstOrder.Language.withConstants Compl.compl Set FirstOrder.Language.Theory.CompleteType Set.instCompl	—	compl_setOf_mem
typesWith_top 📖	mathematical	—	typesWith Top.top FirstOrder.Language.Sentence FirstOrder.Language.withConstants FirstOrder.Language.BoundedFormula.instTop Set.univ FirstOrder.Language.Theory.CompleteType	—	Set.univ_subset_iff FirstOrder.Language.Theory.IsMaximal.mem_of_models isMaximal

FirstOrder.Language.Theory.CompleteType.Sentence

Definitions

Name	Category	Theorems
instSetLike 📖	CompOp	14 math math: FirstOrder.Language.Theory.CompleteType.compl_setOf_mem, FirstOrder.Language.Theory.CompleteType.mem_or_not_mem, FirstOrder.Language.Theory.CompleteType.mem_of_models, FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf, FirstOrder.Language.Theory.CompleteType.setOf_mem_eq_univ_iff, FirstOrder.Language.Theory.CompleteType.not_mem_iff, FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset, FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff, FirstOrder.Language.Theory.CompleteType.mem_typeOf, FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_univ_iff, FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem, FirstOrder.Language.Theory.CompleteType.isMaximal, FirstOrder.Language.Theory.CompleteType.subset, FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff

---

← Back to Index