Documentation Verification Report

Basic

📁 Source: Mathlib/Combinatorics/SimpleGraph/UnitDistance/Basic.lean

Statistics

Metric	Count
Definitions `UnitDistEmbedding`, `bot`, `copy`, `embed`, `iso`, `p`, `subsingleton`	7
Theorems `bot_p`, `copy_p_apply`, `embed_p_apply`, `iso_p_apply`, `subsingleton_p_apply`, `unit_dist`	6
Total	13

SimpleGraph

Definitions

Name	Category	Theorems
`UnitDistEmbedding` 📖	CompData	—

SimpleGraph.UnitDistEmbedding

Definitions

Name	Category	Theorems
`bot` 📖	CompOp	1 math math: `bot_p`
`copy` 📖	CompOp	1 math math: `copy_p_apply`
`embed` 📖	CompOp	1 math math: `embed_p_apply`
`iso` 📖	CompOp	1 math math: `iso_p_apply`
`p` 📖	CompOp	6 math math: `iso_p_apply`, `bot_p`, `unit_dist`, `embed_p_apply`, `subsingleton_p_apply`, `copy_p_apply`
`subsingleton` 📖	CompOp	1 math math: `subsingleton_p_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_p` 📖	mathematical	—	`p` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `bot`	—	—
`copy_p_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `p` `copy` `SimpleGraph.Copy.toEmbedding`	—	—
`embed_p_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `p` `embed` `SimpleGraph.Copy.toEmbedding` `SimpleGraph.Embedding.toCopy`	—	—
`iso_p_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `p` `iso` `SimpleGraph.Copy.toEmbedding` `SimpleGraph.Iso.toCopy` `SimpleGraph.Iso.symm`	—	—
`subsingleton_p_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `p` `subsingleton`	—	—
`unit_dist` 📖	mathematical	`SimpleGraph.Adj`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `p` `Real` `Real.instOne`	—	—

---

← Back to Index