ElementaryMaps

📁 Source: Mathlib/ModelTheory/ElementaryMaps.lean

Statistics

Metric	Count
Definitions ElementaryEmbedding, comp, instFunLike, instInhabited, ofModelsElementaryDiagram, refl, toEmbedding, toFun, toHom, toElementaryEmbedding, toElementaryEmbedding, elementaryDiagram, «term_↪ₑ[_]_»	13
Theorems coe_injective, coe_toEmbedding, coe_toHom, comp_apply, comp_assoc, elementarilyEquivalent, embeddingLike, ext, ext_iff, injective, map_boundedFormula, map_constants, map_formula, map_formula', map_fun, map_rel, map_sentence, ofModelsElementaryDiagram_toFun, refl_apply, strongHomClass, theory_model_iff, toEmbedding_toHom, isElementary_of_exists, toElementaryEmbedding_toFun, coe_toElementaryEmbedding, toElementaryEmbedding_toEmbedding, realize_term_substructure	27
Total	40

FirstOrder

Definitions

Name	Category	Theorems
«term_↪ₑ[_]_» 📖	CompOp	—

FirstOrder.Language

Definitions

Name	Category	Theorems
ElementaryEmbedding 📖	CompData	23 math math: ElementaryEmbedding.map_rel, ElementarySubstructure.subtype_apply, ElementaryEmbedding.ext_iff, Equiv.coe_toElementaryEmbedding, Embedding.toElementaryEmbedding_toFun, ElementaryEmbedding.map_constants, ElementaryEmbedding.map_fun, ElementaryEmbedding.injective, ElementaryEmbedding.map_boundedFormula, ElementaryEmbedding.embeddingLike, ElementaryEmbedding.coe_injective, ElementaryEmbedding.refl_apply, exists_elementaryEmbedding_card_eq, exists_elementaryEmbedding_card_eq_of_le, ElementaryEmbedding.ofModelsElementaryDiagram_toFun, exists_elementaryEmbedding_card_eq_of_ge, ElementarySubstructure.subtype_injective, ElementaryEmbedding.strongHomClass, ElementarySubstructure.coe_subtype, ElementaryEmbedding.coe_toHom, ElementaryEmbedding.coe_toEmbedding, ElementaryEmbedding.map_formula, ElementaryEmbedding.comp_apply
elementaryDiagram 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realize_term_substructure 📖	mathematical	—	Term.realize Substructure SetLike.instMembership Substructure.instSetLike Substructure.inducedStructure	—	HomClass.realize_term StrongHomClass.homClass Embedding.strongHomClass

FirstOrder.Language.ElementaryEmbedding

Definitions

Name	Category	Theorems
comp 📖	CompOp	2 math math: comp_assoc, comp_apply
instFunLike 📖	CompOp	20 math math: map_rel, FirstOrder.Language.ElementarySubstructure.subtype_apply, ext_iff, FirstOrder.Language.Equiv.coe_toElementaryEmbedding, FirstOrder.Language.Embedding.toElementaryEmbedding_toFun, map_constants, map_fun, injective, map_boundedFormula, embeddingLike, coe_injective, refl_apply, ofModelsElementaryDiagram_toFun, FirstOrder.Language.ElementarySubstructure.subtype_injective, strongHomClass, FirstOrder.Language.ElementarySubstructure.coe_subtype, coe_toHom, coe_toEmbedding, map_formula, comp_apply
instInhabited 📖	CompOp	—
ofModelsElementaryDiagram 📖	CompOp	1 math math: ofModelsElementaryDiagram_toFun
refl 📖	CompOp	1 math math: refl_apply
toEmbedding 📖	CompOp	3 math math: FirstOrder.Language.Equiv.toElementaryEmbedding_toEmbedding, toEmbedding_toHom, coe_toEmbedding
toFun 📖	CompOp	1 math math: map_formula'
toHom 📖	CompOp	2 math math: toEmbedding_toHom, coe_toHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_injective 📖	mathematical	—	FirstOrder.Language.ElementaryEmbedding DFunLike.coe instFunLike	—	DFunLike.coe_injective
coe_toEmbedding 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike toEmbedding FirstOrder.Language.ElementaryEmbedding instFunLike	—	—
coe_toHom 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike toHom FirstOrder.Language.ElementaryEmbedding instFunLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
elementarilyEquivalent 📖	mathematical	—	FirstOrder.Language.ElementarilyEquivalent	—	FirstOrder.Language.elementarilyEquivalent_iff map_sentence
embeddingLike 📖	mathematical	—	EmbeddingLike FirstOrder.Language.ElementaryEmbedding instFunLike	—	injective
ext 📖	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike	—	ext
injective 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike	—	map_formula
map_boundedFormula 📖	mathematical	—	FirstOrder.Language.BoundedFormula.Realize DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike	—	Set.Subset.rfl FirstOrder.Language.BoundedFormula.realize_restrictFreeVar' Set.inclusion_eq_id iff_eq_eq map_formula' Function.comp_assoc Equiv.symm_comp_self
map_constants 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike FirstOrder.Language.constantMap	—	FirstOrder.Language.HomClass.map_constants FirstOrder.Language.StrongHomClass.homClass strongHomClass
map_formula 📖	mathematical	—	FirstOrder.Language.Formula.Realize DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike	—	Fin.isEmpty' FirstOrder.Language.Formula.Realize.eq_1 map_boundedFormula Unique.eq_default
map_formula' 📖	mathematical	—	FirstOrder.Language.Formula.Realize toFun	—	—
map_fun 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike FirstOrder.Language.Structure.funMap	—	map_formula FirstOrder.Language.Formula.realize_graph Fin.comp_cons
map_rel 📖	mathematical	—	FirstOrder.Language.Structure.RelMap DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike	—	map_formula
map_sentence 📖	mathematical	—	FirstOrder.Language.Sentence.Realize	—	Empty.instIsEmpty FirstOrder.Language.Sentence.Realize.eq_1 map_formula Unique.eq_default
ofModelsElementaryDiagram_toFun 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike ofModelsElementaryDiagram FirstOrder.Language.Constants FirstOrder.Language.withConstants FirstOrder.Language.constantMap FirstOrder.Language.Functions	—	—
refl_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding instFunLike refl	—	—
strongHomClass 📖	mathematical	—	FirstOrder.Language.StrongHomClass FirstOrder.Language.ElementaryEmbedding instFunLike	—	map_fun map_rel
theory_model_iff 📖	mathematical	—	FirstOrder.Language.Theory.Model	—	map_sentence
toEmbedding_toHom 📖	mathematical	—	FirstOrder.Language.Embedding.toHom toEmbedding toHom	—	—

FirstOrder.Language.Embedding

Definitions

Name	Category	Theorems
toElementaryEmbedding 📖	CompOp	1 math math: toElementaryEmbedding_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isElementary_of_exists 📖	mathematical	FirstOrder.Language.BoundedFormula.Realize Unique.instInhabited Pi.uniqueOfIsEmpty Empty.instIsEmpty Fin.snoc DFunLike.coe FirstOrder.Language.Embedding funLike	FirstOrder.Language.Formula.Realize	—	Empty.instIsEmpty FirstOrder.Language.HomClass.realize_term FirstOrder.Language.StrongHomClass.homClass strongHomClass embeddingLike map_rel Fin.comp_snoc Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq FirstOrder.Language.BoundedFormula.realize_not Unique.eq_default FirstOrder.Language.Formula.realize_relabel_sumInr trans IsPreorder.toIsTrans IsEquiv.toIsPreorder iff_isEquiv
toElementaryEmbedding_toFun 📖	mathematical	FirstOrder.Language.BoundedFormula.Realize Unique.instInhabited Pi.uniqueOfIsEmpty Empty.instIsEmpty Fin.snoc DFunLike.coe FirstOrder.Language.Embedding funLike	FirstOrder.Language.ElementaryEmbedding FirstOrder.Language.ElementaryEmbedding.instFunLike toElementaryEmbedding	—	Empty.instIsEmpty

FirstOrder.Language.Equiv

Definitions

Name	Category	Theorems
toElementaryEmbedding 📖	CompOp	2 math math: coe_toElementaryEmbedding, toElementaryEmbedding_toEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toElementaryEmbedding 📖	mathematical	—	DFunLike.coe FirstOrder.Language.ElementaryEmbedding FirstOrder.Language.ElementaryEmbedding.instFunLike toElementaryEmbedding FirstOrder.Language.Equiv EquivLike.toFunLike instEquivLike	—	—
toElementaryEmbedding_toEmbedding 📖	mathematical	—	FirstOrder.Language.ElementaryEmbedding.toEmbedding toElementaryEmbedding toEmbedding	—	—

---

← Back to Index