Documentation Verification Report

ElementarySubstructures

📁 Source: Mathlib/ModelTheory/ElementarySubstructures.lean

Statistics

Metric	Count
Definitions `ElementarySubstructure`, `inducedStructure`, `instCoe`, `instInhabited`, `instPartialOrder`, `instSetLike`, `instTop`, `subtype`, `toSubstructure`, `IsElementary`, `toElementarySubstructure`	11
Theorems `coe_subtype`, `coe_top`, `elementarilyEquivalent`, `instNonempty`, `isElementary`, `isElementary'`, `mem_top`, `realize_sentence`, `subtype_apply`, `subtype_injective`, `theory_model`, `theory_model_iff`, `isElementary_of_exists`, `toElementarySubstructure_toSubstructure`	14
Total	25

FirstOrder.Language

Definitions

Name	Category	Theorems
`ElementarySubstructure` 📖	CompData	14 math math: `ElementarySubstructure.subtype_apply`, `ElementarySubstructure.theory_model`, `ElementarySubstructure.instNonempty`, `ElementarySubstructure.theory_model_iff`, `ElementarySubstructure.coe_top`, `exists_small_elementarySubstructure`, `ElementarySubstructure.subtype_injective`, `ElementarySubstructure.realize_sentence`, `Substructure.coeSort_elementarySkolem₁Reduct`, `Substructure.elementarySkolem₁Reduct.instSmall`, `ElementarySubstructure.elementarilyEquivalent`, `ElementarySubstructure.coe_subtype`, `exists_elementarySubstructure_card_eq`, `ElementarySubstructure.mem_top`

FirstOrder.Language.ElementarySubstructure

Definitions

Name	Category	Theorems
`inducedStructure` 📖	CompOp	7 math math: `subtype_apply`, `theory_model`, `theory_model_iff`, `subtype_injective`, `realize_sentence`, `elementarilyEquivalent`, `coe_subtype`
`instCoe` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instSetLike` 📖	CompOp	14 math math: `subtype_apply`, `theory_model`, `instNonempty`, `theory_model_iff`, `coe_top`, `FirstOrder.Language.exists_small_elementarySubstructure`, `subtype_injective`, `realize_sentence`, `FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct`, `FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall`, `elementarilyEquivalent`, `coe_subtype`, `FirstOrder.Language.exists_elementarySubstructure_card_eq`, `mem_top`
`instTop` 📖	CompOp	2 math math: `coe_top`, `mem_top`
`subtype` 📖	CompOp	3 math math: `subtype_apply`, `subtype_injective`, `coe_subtype`
`toSubstructure` 📖	CompOp	3 math math: `isElementary'`, `FirstOrder.Language.Substructure.toElementarySubstructure_toSubstructure`, `isElementary`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `FirstOrder.Language.ElementaryEmbedding` `FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `inducedStructure` `FirstOrder.Language.ElementaryEmbedding.instFunLike` `subtype`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.ElementarySubstructure` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`elementarilyEquivalent` 📖	mathematical	—	`FirstOrder.Language.ElementarilyEquivalent` `FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `inducedStructure`	—	`FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent`
`instNonempty` 📖	mathematical	—	`FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike`	—	`FirstOrder.Language.model_nonemptyTheory_iff` `theory_model` `FirstOrder.Language.model_nonempty`
`isElementary` 📖	mathematical	—	`FirstOrder.Language.Substructure.IsElementary` `toSubstructure`	—	`isElementary'`
`isElementary'` 📖	mathematical	—	`FirstOrder.Language.Substructure.IsElementary` `toSubstructure`	—	—
`mem_top` 📖	mathematical	—	`FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`realize_sentence` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `inducedStructure`	—	`FirstOrder.Language.ElementaryEmbedding.map_sentence`
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `FirstOrder.Language.ElementaryEmbedding` `FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `inducedStructure` `FirstOrder.Language.ElementaryEmbedding.instFunLike` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `FirstOrder.Language.ElementaryEmbedding` `inducedStructure` `FirstOrder.Language.ElementaryEmbedding.instFunLike` `subtype`	—	`Subtype.coe_injective`
`theory_model` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `inducedStructure`	—	`theory_model_iff`
`theory_model_iff` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `instSetLike` `inducedStructure`	—	—

FirstOrder.Language.Substructure

Definitions

Name	Category	Theorems
`IsElementary` 📖	MathDef	4 math math: `FirstOrder.Language.ElementarySubstructure.isElementary'`, `skolem₁_reduct_isElementary`, `isElementary_of_exists`, `FirstOrder.Language.ElementarySubstructure.isElementary`
`toElementarySubstructure` 📖	CompOp	1 math math: `toElementarySubstructure_toSubstructure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isElementary_of_exists` 📖	mathematical	`FirstOrder.Language.BoundedFormula.Realize` `Unique.instInhabited` `Pi.uniqueOfIsEmpty` `Empty.instIsEmpty` `Fin.snoc` `FirstOrder.Language.Substructure` `SetLike.instMembership` `instSetLike`	`IsElementary`	—	`Empty.instIsEmpty` `FirstOrder.Language.Embedding.isElementary_of_exists`
`toElementarySubstructure_toSubstructure` 📖	mathematical	`FirstOrder.Language.BoundedFormula.Realize` `Unique.instInhabited` `Pi.uniqueOfIsEmpty` `Empty.instIsEmpty` `Fin.snoc` `FirstOrder.Language.Substructure` `SetLike.instMembership` `instSetLike`	`FirstOrder.Language.ElementarySubstructure.toSubstructure` `toElementarySubstructure`	—	`Empty.instIsEmpty`

---

← Back to Index