Documentation Verification Report

Bundled

📁 Source: Mathlib/ModelTheory/Bundled.lean

Statistics

Metric	Count
Definitions `structure`, `bundledInduced`, `bundledInducedEquiv`, `toModel`, `toModel`, `bundled`, `ModelType`, `Carrier`, `defaultExpansion`, `equivInduced`, `instCoeSort`, `instInhabited`, `leftStructure`, `of`, `reduct`, `rightStructure`, `shrink`, `struc`, `subtheoryModel`, `ulift`, `equivSetoid`	21
Theorems `bundledInduced_str`, `bundledInduced_α`, `instSmall`, `coe_of`, `defaultExpansion_Carrier`, `defaultExpansion_struc`, `instNonempty`, `is_model`, `nonempty'`, `of_small`, `reduct_Carrier`, `reduct_struc`, `subtheoryModel_Carrier`, `subtheoryModel_models`, `subtheoryModel_struc`, `coe_of`	16
Total	37

CategoryTheory.Bundled

Definitions

Name	Category	Theorems
`structure` 📖	CompOp	10 math math: `FirstOrder.Language.exists_elementarilyEquivalent_card_eq`, `FirstOrder.Language.dlo_age`, `FirstOrder.Language.isFraisse_finite_linear_order`, `FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo`, `FirstOrder.Language.exists_countable_is_age_of_iff`, `FirstOrder.Language.IsFraisse.FG`, `FirstOrder.Language.exists_elementaryEmbedding_card_eq`, `FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le`, `FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge`, `FirstOrder.Language.Structure.FG.mem_age_of_equiv`

Equiv

Definitions

Name	Category	Theorems
`bundledInduced` 📖	CompOp	2 math math: `bundledInduced_α`, `bundledInduced_str`
`bundledInducedEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bundledInduced_str` 📖	mathematical	—	`CategoryTheory.Bundled.str` `FirstOrder.Language.Structure` `bundledInduced` `inducedStructure`	—	—
`bundledInduced_α` 📖	mathematical	—	`CategoryTheory.Bundled.α` `FirstOrder.Language.Structure` `bundledInduced`	—	—

FirstOrder.Language

Definitions

Name	Category	Theorems
`equivSetoid` 📖	CompOp	3 math math: `IsFraisse.is_essentially_countable`, `exists_countable_is_age_of_iff`, `age.countable_quotient`

FirstOrder.Language.ElementarilyEquivalent

Definitions

Name	Category	Theorems
`toModel` 📖	CompOp	—

FirstOrder.Language.ElementarySubstructure

Definitions

Name	Category	Theorems
`toModel` 📖	CompOp	1 math math: `toModel.instSmall`

FirstOrder.Language.ElementarySubstructure.toModel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSmall` 📖	mathematical	—	`Small` `FirstOrder.Language.Theory.ModelType.Carrier` `FirstOrder.Language.ElementarySubstructure.toModel`	—	—

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
`ModelType` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`ModelType.Carrier` `Model.bundled`	—	—

FirstOrder.Language.Theory.Model

Definitions

Name	Category	Theorems
`bundled` 📖	CompOp	1 math math: `FirstOrder.Language.Theory.coe_of`

FirstOrder.Language.Theory.ModelType

Definitions

Name	Category	Theorems
`Carrier` 📖	CompOp	18 math math: `defaultExpansion_Carrier`, `subtheoryModel_Carrier`, `defaultExpansion_struc`, `subtheoryModel_models`, `FirstOrder.Language.Theory.models_formula_iff`, `is_model`, `instNonempty`, `FirstOrder.Language.Theory.models_sentence_iff`, `FirstOrder.Language.Theory.coe_of`, `of_small`, `FirstOrder.Language.Theory.exists_large_model_of_infinite_model`, `coe_of`, `nonempty'`, `reduct_struc`, `FirstOrder.Language.Theory.IsComplete.isComplete_iff_models_elementarily_equivalent`, `FirstOrder.Language.ElementarySubstructure.toModel.instSmall`, `reduct_Carrier`, `FirstOrder.Language.Theory.exists_modelType_is_realized_in`
`defaultExpansion` 📖	CompOp	2 math math: `defaultExpansion_Carrier`, `defaultExpansion_struc`
`equivInduced` 📖	CompOp	—
`instCoeSort` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`leftStructure` 📖	CompOp	—
`of` 📖	CompOp	2 math math: `of_small`, `coe_of`
`reduct` 📖	CompOp	2 math math: `reduct_struc`, `reduct_Carrier`
`rightStructure` 📖	CompOp	—
`shrink` 📖	CompOp	—
`struc` 📖	CompOp	9 math math: `defaultExpansion_struc`, `subtheoryModel_models`, `FirstOrder.Language.Theory.models_formula_iff`, `is_model`, `subtheoryModel_struc`, `FirstOrder.Language.Theory.models_sentence_iff`, `reduct_struc`, `FirstOrder.Language.Theory.IsComplete.isComplete_iff_models_elementarily_equivalent`, `FirstOrder.Language.Theory.exists_modelType_is_realized_in`
`subtheoryModel` 📖	CompOp	3 math math: `subtheoryModel_Carrier`, `subtheoryModel_models`, `subtheoryModel_struc`
`ulift` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`Carrier` `of`	—	—
`defaultExpansion_Carrier` 📖	mathematical	`FirstOrder.Language.LHom.Injective`	`Carrier` `FirstOrder.Language.LHom.onTheory` `defaultExpansion`	—	—
`defaultExpansion_struc` 📖	mathematical	`FirstOrder.Language.LHom.Injective`	`struc` `FirstOrder.Language.LHom.onTheory` `defaultExpansion` `FirstOrder.Language.LHom.defaultExpansion` `Carrier`	—	—
`instNonempty` 📖	mathematical	—	`Carrier`	—	`nonempty'`
`is_model` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `Carrier` `struc`	—	—
`nonempty'` 📖	mathematical	—	`Carrier`	—	—
`of_small` 📖	mathematical	—	`Small` `Carrier` `of`	—	—
`reduct_Carrier` 📖	mathematical	—	`Carrier` `reduct` `FirstOrder.Language.LHom.onTheory`	—	—
`reduct_struc` 📖	mathematical	—	`struc` `reduct` `FirstOrder.Language.LHom.reduct` `Carrier` `FirstOrder.Language.LHom.onTheory`	—	—
`subtheoryModel_Carrier` 📖	mathematical	`FirstOrder.Language.Theory` `Set.instHasSubset` `FirstOrder.Language.Sentence`	`Carrier` `subtheoryModel`	—	—
`subtheoryModel_models` 📖	mathematical	`FirstOrder.Language.Theory` `Set.instHasSubset` `FirstOrder.Language.Sentence`	`FirstOrder.Language.Theory.Model` `Carrier` `subtheoryModel` `struc`	—	`is_model`
`subtheoryModel_struc` 📖	mathematical	`FirstOrder.Language.Theory` `Set.instHasSubset` `FirstOrder.Language.Sentence`	`struc` `subtheoryModel`	—	—

---

← Back to Index