Documentation Verification Report

Embedding

📁 Source: Mathlib/Data/Fin/Embedding.lean

Statistics

Metric	Count
Definitions `addNatEmb`, `castAddEmb`, `castLEEmb`, `castSuccEmb`, `natAddEmb`, `natAdd_castLEEmb`, `succAboveEmb`, `succEmb`, `valEmbedding`	9
Theorems `addNatEmb_apply`, `castAddEmb_apply`, `castLEEmb_apply`, `castSuccEmb_apply`, `coe_castAddEmb`, `coe_castLEEmb`, `coe_castSuccEmb`, `coe_succAboveEmb`, `coe_succEmb`, `equivSubtype_symm_trans_valEmbedding`, `equiv_iff_eq`, `natAddEmb_apply`, `natAdd_castLEEmb_apply_val`, `nonempty_embedding_iff`, `range_natAdd_castLEEmb`, `succAboveEmb_apply`, `valEmbedding_apply`	17
Total	26

Fin

Definitions

Name	Category	Theorems
`addNatEmb` 📖	CompOp	8 math math: `map_addNatEmb_Ici`, `map_addNatEmb_Ioi`, `map_addNatEmb_Ico`, `map_addNatEmb_uIcc`, `map_addNatEmb_Ioc`, `map_addNatEmb_Icc`, `map_addNatEmb_Ioo`, `addNatEmb_apply`
`castAddEmb` 📖	CompOp	13 math math: `map_castAddEmb_Ico`, `map_castAddEmb_Ici`, `Embedding.restrictSurjective_of_add_le_ENatCard`, `castAddEmb_apply`, `map_castAddEmb_Ioc`, `Embedding.restrictSurjective_of_add_le_natCard`, `map_castAddEmb_Iio`, `map_castAddEmb_uIcc`, `map_castAddEmb_Iic`, `coe_castAddEmb`, `map_castAddEmb_Icc`, `map_castAddEmb_Ioo`, `map_castAddEmb_Ioi`
`castLEEmb` 📖	CompOp	11 math math: `map_castLEEmb_Ioc`, `map_castLEEmb_Iic`, `map_castLEEmb_uIcc`, `Embedding.restrictSurjective_of_le_natCard`, `Embedding.restrictSurjective_of_le_ENatCard`, `map_castLEEmb_Ico`, `map_castLEEmb_Ioo`, `map_castLEEmb_Icc`, `map_castLEEmb_Iio`, `coe_castLEEmb`, `castLEEmb_apply`
`castSuccEmb` 📖	CompOp	14 math math: `Iio_last_eq_map`, `coe_castSuccEmb`, `map_castSuccEmb_Ici`, `map_castSuccEmb_Icc`, `Iio_castSucc`, `map_castSuccEmb_Iio`, `map_castSuccEmb_uIcc`, `map_castSuccEmb_Iic`, `univ_castSuccEmb`, `map_castSuccEmb_Ioi`, `castSuccEmb_apply`, `map_castSuccEmb_Ico`, `map_castSuccEmb_Ioo`, `map_castSuccEmb_Ioc`
`natAddEmb` 📖	CompOp	8 math math: `natAddEmb_apply`, `map_natAddEmb_Ici`, `map_natAddEmb_uIcc`, `map_natAddEmb_Icc`, `map_natAddEmb_Ico`, `map_natAddEmb_Ioi`, `map_natAddEmb_Ioo`, `map_natAddEmb_Ioc`
`natAdd_castLEEmb` 📖	CompOp	3 math math: `natAdd_castLEEmb_apply_val`, `cycleIcc_def_le`, `range_natAdd_castLEEmb`
`succAboveEmb` 📖	CompOp	3 math math: `univ_succAbove`, `succAboveEmb_apply`, `coe_succAboveEmb`
`succEmb` 📖	CompOp	14 math math: `map_succEmb_Iio`, `coe_succEmb`, `Ioi_succ`, `map_succEmb_uIcc`, `map_succEmb_Ioi`, `map_succEmb_Ici`, `map_succEmb_Ioo`, `map_succEmb_Ico`, `map_succEmb_Ioc`, `Finsupp.cons_support`, `map_succEmb_Icc`, `Ioi_zero_eq_map`, `succOrderEmb_toEmbedding`, `map_succEmb_Iic`
`valEmbedding` 📖	CompOp	13 math math: `map_valEmbedding_uIcc`, `valEmbedding_apply`, `map_valEmbedding_Ici`, `map_valEmbedding_Icc`, `equivSubtype_symm_trans_valEmbedding`, `map_valEmbedding_Ioi`, `map_valEmbedding_Ioo`, `map_valEmbedding_Ico`, `Finset.map_valEmbedding_attachFin`, `map_valEmbedding_univ`, `map_valEmbedding_Iio`, `map_valEmbedding_Iic`, `map_valEmbedding_Ioc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addNatEmb_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `addNatEmb`	—	—
`castAddEmb_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `castAddEmb`	—	—
`castLEEmb_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `castLEEmb`	—	—
`castSuccEmb_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `castSuccEmb`	—	—
`coe_castAddEmb` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `castAddEmb`	—	—
`coe_castLEEmb` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `castLEEmb`	—	—
`coe_castSuccEmb` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `castSuccEmb`	—	—
`coe_succAboveEmb` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `succAboveEmb` `succAbove`	—	—
`coe_succEmb` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `succEmb`	—	—
`equivSubtype_symm_trans_valEmbedding` 📖	mathematical	—	`Function.Embedding.trans` `Equiv.toEmbedding` `Equiv.symm` `equivSubtype` `valEmbedding` `Function.Embedding.subtype`	—	—
`equiv_iff_eq` 📖	mathematical	—	`Equiv`	—	`le_antisymm` `nonempty_embedding_iff`
`natAddEmb_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `natAddEmb`	—	—
`natAdd_castLEEmb_apply_val` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `natAdd_castLEEmb`	—	—
`nonempty_embedding_iff` 📖	mathematical	—	`Function.Embedding`	—	`LT.lt.ne'` `Nonempty.map` `Function.Embedding.setValue_eq_iff` `Function.instEmbeddingLikeEmbedding`
`range_natAdd_castLEEmb` 📖	mathematical	—	`Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `natAdd_castLEEmb` `setOf`	—	`Set.ext`
`succAboveEmb_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `succAboveEmb` `succAbove`	—	—
`valEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `valEmbedding`	—	—

---

← Back to Index