Documentation Verification Report

Skolem

📁 Source: Mathlib/ModelTheory/Skolem.lean

Statistics

Metric	Count
Definitions `elementarySkolem₁Reduct`, `skolem₁`, `skolem₁Structure`	3
Theorems `coeSort_elementarySkolem₁Reduct`, `instSmall`, `skolem₁_reduct_isElementary`, `card_functions_sum_skolem₁`, `card_functions_sum_skolem₁_le`, `exists_elementarySubstructure_card_eq`, `exists_small_elementarySubstructure`, `skolem₁_Functions`, `skolem₁_Relations`	9
Total	12

FirstOrder.Language

Definitions

Name	Category	Theorems
`skolem₁` 📖	CompOp	7 math math: `skolem₁_Functions`, `card_functions_sum_skolem₁_le`, `Substructure.skolem₁_reduct_isElementary`, `card_functions_sum_skolem₁`, `Substructure.coeSort_elementarySkolem₁Reduct`, `Substructure.elementarySkolem₁Reduct.instSmall`, `skolem₁_Relations`
`skolem₁Structure` 📖	CompOp	3 math math: `Substructure.skolem₁_reduct_isElementary`, `Substructure.coeSort_elementarySkolem₁Reduct`, `Substructure.elementarySkolem₁Reduct.instSmall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_functions_sum_skolem₁` 📖	mathematical	—	`Functions` `sum` `skolem₁` `BoundedFormula`	—	`Cardinal.mk_sigma` `card_functions_sum` `Cardinal.sum_add_distrib'` `Cardinal.lift_id'` `add_comm` `Cardinal.add_eq_max` `Cardinal.infinite_iff` `Infinite.of_injective` `instInfiniteNat` `max_eq_left` `Cardinal.sum_le_sum` `Cardinal.lift_le` `Cardinal.lift_lift` `Cardinal.lift_mk_le`
`card_functions_sum_skolem₁_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Functions` `sum` `skolem₁` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0` `card`	—	`card_functions_sum_skolem₁` `Function.Injective.sigma_map` `Nat.succ_injective` `trans` `instIsTransLe` `BoundedFormula.card_le` `Cardinal.lift_le` `Cardinal.mk_empty` `Cardinal.lift_zero` `Cardinal.lift_uzero` `zero_add` `le_refl`
`exists_elementarySubstructure_card_eq` 📖	mathematical	`Cardinal` `Cardinal.instLE` `Cardinal.aleph0` `Cardinal.lift` `Set.Elem` `card`	`Set` `Set.instHasSubset` `SetLike.coe` `ElementarySubstructure` `ElementarySubstructure.instSetLike` `SetLike.instMembership`	—	`Cardinal.le_mk_iff_exists_set` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_union_left` `Substructure.subset_closure` `Cardinal.mk_image_eq_lift` `Equiv.injective` `Substructure.coeSort_elementarySkolem₁Reduct` `Cardinal.lift_id'` `Cardinal.lift_umax` `le_antisymm` `Cardinal.lift_le` `LE.le.trans` `Substructure.lift_card_closure_le` `max_le_iff` `Cardinal.aleph0_le_lift` `Cardinal.add_eq_max` `trans` `instIsTransLe` `Cardinal.mk_le_mk_of_subset` `Set.subset_union_right` `Cardinal.mk_union_le` `Cardinal.lift_add` `add_comm` `max_le` `le_rfl` `card_functions_sum_skolem₁_le` `Cardinal.lift_max` `Cardinal.lift_aleph0` `Cardinal.lift_lift` `le_refl`
`exists_small_elementarySubstructure` 📖	mathematical	—	`Small` `ElementarySubstructure` `SetLike.instMembership` `ElementarySubstructure.instSetLike`	—	`Substructure.elementarySkolem₁Reduct.instSmall`
`skolem₁_Functions` 📖	mathematical	—	`Functions` `skolem₁` `BoundedFormula`	—	—
`skolem₁_Relations` 📖	mathematical	—	`Relations` `skolem₁`	—	—

FirstOrder.Language.Substructure

Definitions

Name	Category	Theorems
`elementarySkolem₁Reduct` 📖	CompOp	2 math math: `coeSort_elementarySkolem₁Reduct`, `elementarySkolem₁Reduct.instSmall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeSort_elementarySkolem₁Reduct` 📖	mathematical	—	`FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `FirstOrder.Language.ElementarySubstructure.instSetLike` `elementarySkolem₁Reduct` `FirstOrder.Language.Substructure` `FirstOrder.Language.sum` `FirstOrder.Language.skolem₁` `FirstOrder.Language.sumStructure` `FirstOrder.Language.skolem₁Structure` `instSetLike`	—	—
`skolem₁_reduct_isElementary` 📖	mathematical	—	`IsElementary` `DFunLike.coe` `OrderEmbedding` `FirstOrder.Language.Substructure` `FirstOrder.Language.sum` `FirstOrder.Language.skolem₁` `FirstOrder.Language.sumStructure` `FirstOrder.Language.skolem₁Structure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instFunLikeOrderEmbedding` `FirstOrder.Language.LHom.substructureReduct` `FirstOrder.Language.LHom.sumInl` `FirstOrder.Language.LHom.sumInl_isExpansionOn`	—	`isElementary_of_exists` `FirstOrder.Language.LHom.sumInl_isExpansionOn` `Empty.instIsEmpty` `fun_mem`

FirstOrder.Language.Substructure.elementarySkolem₁Reduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSmall` 📖	mathematical	—	`Small` `FirstOrder.Language.ElementarySubstructure` `SetLike.instMembership` `FirstOrder.Language.ElementarySubstructure.instSetLike` `FirstOrder.Language.Substructure.elementarySkolem₁Reduct` `Bot.bot` `FirstOrder.Language.Substructure` `FirstOrder.Language.sum` `FirstOrder.Language.skolem₁` `FirstOrder.Language.sumStructure` `FirstOrder.Language.skolem₁Structure` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `FirstOrder.Language.Substructure.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct` `FirstOrder.Language.Substructure.small_bot`

---

← Back to Index