Documentation Verification Report

KatonaCircle

📁 Source: Mathlib/Combinatorics/KatonaCircle.lean

Statistics

Metric	Count
Definitions `Numbering`, `IsPrefix`, `instDecidableIsPrefix`, `prefixed`, `prefixedEquiv`	5
Theorems `card_numbering`, `subset_of_card_le_card`, `card_prefixed`, `dens_prefixed`, `disjoint_prefixed_prefixed`, `mem_prefixed`	6
Total	11

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_numbering` 📖	mathematical	—	`card` `Numbering` `Equiv.instFintype` `Fin.fintype` `Nat.factorial`	—	`card_equiv`

Numbering

Definitions

Name	Category	Theorems
`IsPrefix` 📖	MathDef	1 math math: `mem_prefixed`
`instDecidableIsPrefix` 📖	CompOp	—
`prefixed` 📖	CompOp	4 math math: `disjoint_prefixed_prefixed`, `mem_prefixed`, `card_prefixed`, `dens_prefixed`
`prefixedEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_prefixed` 📖	mathematical	—	`Finset.card` `Numbering` `prefixed` `Nat.factorial` `Fintype.card`	—	`Fintype.card_coe` `Fintype.card_prod` `Fintype.card_numbering` `Fintype.card_congr'` `Fintype.card_subtype_compl` `Fintype.card_congr`
`dens_prefixed` 📖	mathematical	—	`Finset.dens` `Numbering` `Equiv.instFintype` `Fintype.card` `Fin.fintype` `prefixed` `NNRat` `NNRat.instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NNRat.instSemifield` `Nat.choose` `Finset.card`	—	`card_prefixed` `Nat.cast_mul` `Fintype.card_numbering` `Nat.cast_choose` `Finset.card_le_univ` `NNRat.instCharZero` `inv_div`
`disjoint_prefixed_prefixed` 📖	mathematical	`Finset` `Finset.instHasSubset`	`Disjoint` `Numbering` `Finset.partialOrder` `Finset.instOrderBot` `prefixed`	—	`IsPrefix.subset_of_card_le_card`
`mem_prefixed` 📖	mathematical	—	`Numbering` `Finset` `Finset.instMembership` `prefixed` `IsPrefix`	—	—

Numbering.IsPrefix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subset_of_card_le_card` 📖	mathematical	`Numbering.IsPrefix` `Finset.card`	`Finset` `Finset.instHasSubset`	—	`LT.lt.trans_le`

(root)

Definitions

Name	Category	Theorems
`Numbering` 📖	CompOp	5 math math: `Numbering.disjoint_prefixed_prefixed`, `Numbering.mem_prefixed`, `Numbering.card_prefixed`, `Numbering.dens_prefixed`, `Fintype.card_numbering`

---

← Back to Index