Documentation Verification Report

Encoding

📁 Source: Mathlib/ModelTheory/Encoding.lean

Statistics

Metric	Count
Definitions `encoding`, `listDecode`, `listEncode`, `sigmaAll`, `sigmaImp`, `encoding`, `instEncodableOfSigmaNatFunctions`, `listDecode`, `listEncode`	9
Theorems `card_le`, `encoding_decode`, `encoding_encode`, `encoding_Γ`, `instCountableFormula`, `instCountableSigmaNat`, `instCountableSymbolsConstantsOn`, `instCountableSymbolsWithConstants`, `listDecode_encode_list`, `listEncode_sigma_injective`, `sigmaAll_apply`, `sigmaImp_apply`, `card_le`, `card_sigma`, `encoding_decode`, `encoding_encode`, `encoding_Γ`, `instCountableOfSigmaNatFunctions`, `listDecode_encode_list`, `listEncode_injective`, `small`	21
Total	30

FirstOrder.Language.BoundedFormula

Definitions

Name	Category	Theorems
`encoding` 📖	CompOp	3 math math: `encoding_decode`, `encoding_encode`, `encoding_Γ`
`listDecode` 📖	CompOp	2 math math: `encoding_decode`, `listDecode_encode_list`
`listEncode` 📖	CompOp	3 math math: `listEncode_sigma_injective`, `encoding_encode`, `listDecode_encode_list`
`sigmaAll` 📖	CompOp	1 math math: `sigmaAll_apply`
`sigmaImp` 📖	CompOp	1 math math: `sigmaImp_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `FirstOrder.Language.BoundedFormula` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0` `Cardinal.instAdd` `Cardinal.lift` `FirstOrder.Language.card`	—	`Cardinal.lift_le` `LE.le.trans` `Computability.Encoding.card_le_card_list` `encoding_Γ` `Cardinal.mk_list_eq_max_mk_aleph0` `Cardinal.lift_max` `Cardinal.lift_aleph0` `max_le_iff` `Cardinal.mk_sum` `FirstOrder.Language.Term.card_sigma` `Cardinal.add_eq_max` `le_rfl` `Cardinal.mk_nat` `Cardinal.lift_add` `Cardinal.lift_lift` `add_assoc` `add_comm` `Cardinal.aleph0_add_aleph0` `FirstOrder.Language.card.eq_1` `FirstOrder.Language.Symbols.eq_1` `le_refl` `le_max_left`
`encoding_decode` 📖	mathematical	—	`Computability.Encoding.decode` `FirstOrder.Language.BoundedFormula` `encoding` `listDecode`	—	—
`encoding_encode` 📖	mathematical	—	`Computability.Encoding.encode` `FirstOrder.Language.BoundedFormula` `encoding` `listEncode`	—	—
`encoding_Γ` 📖	mathematical	—	`Computability.Encoding.Γ` `FirstOrder.Language.BoundedFormula` `encoding` `FirstOrder.Language.Term` `FirstOrder.Language.Relations`	—	—
`instCountableFormula` 📖	mathematical	—	`Countable` `FirstOrder.Language.Formula`	—	`Function.Injective.countable` `instCountableSigmaNat` `sigma_mk_injective`
`instCountableSigmaNat` 📖	mathematical	—	`Countable` `FirstOrder.Language.BoundedFormula`	—	`Cardinal.mk_le_aleph0_iff` `LE.le.trans` `card_le` `max_le` `le_refl`
`instCountableSymbolsConstantsOn` 📖	mathematical	—	`Countable` `FirstOrder.Language.Symbols` `FirstOrder.Language.constantsOn`	—	`Cardinal.mk_le_aleph0_iff` `FirstOrder.Language.card_constantsOn`
`instCountableSymbolsWithConstants` 📖	mathematical	—	`Countable` `FirstOrder.Language.Symbols` `FirstOrder.Language.withConstants`	—	`FirstOrder.Language.card_sum` `instCountableSymbolsConstantsOn`
`listDecode_encode_list` 📖	mathematical	—	`listDecode` `FirstOrder.Language.BoundedFormula` `FirstOrder.Language.Term` `FirstOrder.Language.Relations` `listEncode`	—	`listEncode.eq_1` `listDecode.eq_1` `listEncode.eq_2` `listDecode.eq_2` `listEncode.eq_3` `listDecode.eq_3` `Option.bind_congr'` `lt_of_lt_of_le` `le_self_add` `Nat.instCanonicallyOrderedAdd` `Sigma.eta` `le_refl` `listEncode.eq_4` `listDecode.eq_4` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `sigmaImp_apply` `listEncode.eq_5` `listDecode.eq_5` `listDecode.eq_6`
`listEncode_sigma_injective` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula` `FirstOrder.Language.Term` `FirstOrder.Language.Relations` `listEncode`	—	`Computability.Encoding.encode_injective`
`sigmaAll_apply` 📖	mathematical	—	`sigmaAll` `FirstOrder.Language.BoundedFormula` `all`	—	—
`sigmaImp_apply` 📖	mathematical	—	`sigmaImp` `FirstOrder.Language.BoundedFormula` `imp`	—	—

FirstOrder.Language.Term

Definitions

Name	Category	Theorems
`encoding` 📖	CompOp	3 math math: `encoding_Γ`, `encoding_decode`, `encoding_encode`
`instEncodableOfSigmaNatFunctions` 📖	CompOp	—
`listDecode` 📖	CompOp	2 math math: `listDecode_encode_list`, `encoding_decode`
`listEncode` 📖	CompOp	3 math math: `listDecode_encode_list`, `listEncode_injective`, `encoding_encode`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `FirstOrder.Language.Term` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0` `FirstOrder.Language.Functions`	—	`Cardinal.lift_le` `trans` `instIsTransLe` `Computability.Encoding.card_le_card_list` `Cardinal.mk_list_le_max`
`card_sigma` 📖	mathematical	—	`FirstOrder.Language.Term` `Cardinal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0` `FirstOrder.Language.Functions`	—	`le_antisymm` `Cardinal.mk_sigma` `LE.le.trans` `Cardinal.sum_le_lift_mk_mul_iSup` `Cardinal.mk_nat` `Cardinal.lift_aleph0` `Cardinal.mul_eq_max_of_aleph0_le_left` `le_rfl` `Cardinal.one_le_iff_ne_zero` `trans` `instIsTransLe` `Cardinal.mk_ne_zero_iff` `le_ciSup` `Cardinal.bddAbove_range` `UnivLE.small` `univLE_of_max` `UnivLE.self` `max_le_iff` `ciSup_le_iff'` `le_max_left` `card_le` `max_le` `Cardinal.add_eq_max` `Cardinal.mk_sum` `add_comm` `Cardinal.lift_add` `add_assoc` `Cardinal.lift_lift` `Cardinal.mk_fin` `Cardinal.lift_natCast` `le_imp_le_of_le_of_le` `add_le_add_left` `Cardinal.addRightMono` `le_of_lt` `Cardinal.natCast_lt_aleph0` `le_refl` `Cardinal.infinite_iff` `Infinite.of_injective` `instInfiniteNat` `Cardinal.le_def`
`encoding_decode` 📖	mathematical	—	`Computability.Encoding.decode` `FirstOrder.Language.Term` `encoding` `listDecode`	—	—
`encoding_encode` 📖	mathematical	—	`Computability.Encoding.encode` `FirstOrder.Language.Term` `encoding` `listEncode`	—	—
`encoding_Γ` 📖	mathematical	—	`Computability.Encoding.Γ` `FirstOrder.Language.Term` `encoding` `FirstOrder.Language.Functions`	—	—
`instCountableOfSigmaNatFunctions` 📖	mathematical	—	`Countable` `FirstOrder.Language.Term`	—	`Cardinal.mk_le_aleph0_iff` `LE.le.trans` `card_le` `max_le_iff` `Cardinal.mk_sum` `Cardinal.mk_le_aleph0`
`listDecode_encode_list` 📖	mathematical	—	`listDecode` `FirstOrder.Language.Term` `FirstOrder.Language.Functions` `listEncode`	—	`listEncode.eq_1` `listDecode.eq_2` `listEncode.eq_2` `listDecode.eq_3` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd`
`listEncode_injective` 📖	mathematical	—	`FirstOrder.Language.Term` `FirstOrder.Language.Functions` `listEncode`	—	`Computability.Encoding.encode_injective`
`small` 📖	mathematical	—	`Small` `FirstOrder.Language.Term`	—	`small_of_injective` `smallList` `small_sum` `small_sigma` `UnivLE.small` `univLE_of_max` `UnivLE.self` `listEncode_injective`

---

← Back to Index