UniquelyDecodable
📁 Source: Mathlib/InformationTheory/Coding/UniquelyDecodable.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsUniquelyDecodable | 1 |
| 2 | |
| Total | 3 |
InformationTheory
Definitions
| Name | Category | Theorems |
|---|---|---|
UniquelyDecodable 📖 | MathDef | — |
InformationTheory.UniquelyDecodable
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
epsilon_not_mem 📖 | mathematical | InformationTheory.UniquelyDecodable | SetSet.instMembership | — | — |
flatten_injective 📖 | — | InformationTheory.UniquelyDecodable | — | — | Subtype.prop |
---