Documentation Verification Report

Functions

📁 Source: Mathlib/Testing/Plausible/Functions.lean

Statistics

Metric	Count
Definitions `Functions`, `testable`, `testable`, `InjectiveFunction`, `applyId`, `slice`, `sampleableExt`, `apply`, `instArbitraryInt`, `instRepr`, `mk`, `repr`, `shrink`, `shrinkPerm`, `sliceSizes`, `testable`, `sampleableExt`, `sampleableExt`, `applyFinsupp`, `zeroDefault`, `zeroDefaultSupp`, `instInhabitedInjectiveFunction`	22
Theorems `applyId_cons`, `applyId_eq_self`, `applyId_zip_eq`, `applyId_injective`, `applyId_mem_iff`, `injective`	6
Total	28

FirstOrder.Language

Definitions

Name	Category	Theorems
`Functions` 📖	CompOp	31 math math: `LHom.Injective.onFunction`, `Term.listDecode_encode_list`, `LHom.sumElim_onFunction`, `LHom.sumMap_onFunction`, `LHom.funMap_sumInl`, `skolem₁_Functions`, `card_eq_card_functions_add_card_relations`, `empty.isFraisseLimit_of_countable_infinite`, `LHom.funMap_sumInr`, `constantsOn_Functions`, `card_functions_sum_skolem₁_le`, `Countable.countable_functions`, `Term.listEncode_injective`, `LHom.sumInr_onFunction`, `card_functions_sum_skolem₁`, `LHom.sumInl_onFunction`, `withConstants_funMap_sumInl`, `lhomWithConstants_onFunction`, `funMap_sumInr`, `Term.card_sigma`, `ElementaryEmbedding.ofModelsElementaryDiagram_toFun`, `Term.card_le`, `withConstants_funMap_sumInr`, `orderLHom_onFunction`, `Term.encoding_Γ`, `LHom.id_onFunction`, `card_functions_sum`, `LHom.ofIsEmpty_onFunction`, `funMap_sumInl`, `Substructure.lift_card_closure_le`, `isEmpty_functions_constantsOn_succ`

Plausible

Definitions

Name	Category	Theorems
`InjectiveFunction` 📖	CompData	—
`instInhabitedInjectiveFunction` 📖	CompOp	—

Plausible.Antitone

Definitions

Name	Category	Theorems
`testable` 📖	CompOp	—

Plausible.Injective

Definitions

Name	Category	Theorems
`testable` 📖	CompOp	—

Plausible.InjectiveFunction

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	1 math math: `injective`
`instArbitraryInt` 📖	CompOp	—
`instRepr` 📖	CompOp	—
`mk` 📖	CompOp	—
`repr` 📖	CompOp	—
`shrink` 📖	CompOp	—
`shrinkPerm` 📖	CompOp	—
`sliceSizes` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`applyId_injective` 📖	mathematical	—	`List.applyId`	—	`List.applyId_zip_eq` `applyId_mem_iff` `List.applyId_eq_self`
`applyId_mem_iff` 📖	mathematical	—	`List.applyId`	—	`List.mem_dlookup_iff` `le_of_eq`
`injective` 📖	mathematical	—	`apply`	—	`Plausible.TotalFunction.List.toFinmap'.eq_1` `Sigma.eta` `applyId_injective`

Plausible.InjectiveFunction.List

Definitions

Name	Category	Theorems
`applyId` 📖	CompOp	5 math math: `Plausible.InjectiveFunction.applyId_mem_iff`, `applyId_cons`, `applyId_eq_self`, `applyId_zip_eq`, `Plausible.InjectiveFunction.applyId_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`applyId_cons` 📖	mathematical	—	`applyId`	—	—
`applyId_eq_self` 📖	mathematical	—	`applyId`	—	`List.dlookup_eq_none`
`applyId_zip_eq` 📖	mathematical	—	`applyId`	—	`applyId_cons` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass`

Plausible.InjectiveFunction.Perm

Definitions

Name	Category	Theorems
`slice` 📖	CompOp	—

Plausible.InjectiveFunction.PiInjective

Definitions

Name	Category	Theorems
`sampleableExt` 📖	CompOp	—

Plausible.Monotone

Definitions

Name	Category	Theorems
`testable` 📖	CompOp	—

Plausible.TotalFunction

Definitions

Name	Category	Theorems
`applyFinsupp` 📖	CompOp	—
`zeroDefault` 📖	CompOp	—
`zeroDefaultSupp` 📖	CompOp	—

Plausible.TotalFunction.DFinsupp

Definitions

Name	Category	Theorems
`sampleableExt` 📖	CompOp	—

Plausible.TotalFunction.Finsupp

Definitions

Name	Category	Theorems
`sampleableExt` 📖	CompOp	—

---

← Back to Index