Documentation Verification Report

Take

📁 Source: Mathlib/Data/Fin/Tuple/Take.lean

Statistics

Metric	Count
Definitions `take`	1
Theorems `get_take_eq_take_get_comp_cast`, `get_take_ofFn_eq_take_comp_cast`, `ofFn_take_eq_take_ofFn`, `ofFn_take_get`, `take_addCases_left`, `take_addCases_right`, `take_append_left`, `take_append_right`, `take_apply`, `take_eq_init`, `take_eq_self`, `take_init`, `take_one`, `take_repeat`, `take_succ_eq_snoc`, `take_take`, `take_update_of_ge`, `take_update_of_lt`, `take_zero`	19
Total	20

Fin

Definitions

Name	Category	Theorems
`take` 📖	CompOp	19 math math: `get_take_eq_take_get_comp_cast`, `take_init`, `take_one`, `take_take`, `take_apply`, `take_zero`, `take_addCases_right`, `get_take_ofFn_eq_take_comp_cast`, `take_eq_init`, `take_update_of_ge`, `take_append_left`, `take_succ_eq_snoc`, `take_addCases_left`, `ofFn_take_get`, `take_append_right`, `take_update_of_lt`, `take_repeat`, `ofFn_take_eq_take_ofFn`, `take_eq_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`get_take_eq_take_get_comp_cast` 📖	mathematical	—	`take`	—	—
`get_take_ofFn_eq_take_comp_cast` 📖	mathematical	—	`take`	—	—
`ofFn_take_eq_take_ofFn` 📖	mathematical	—	`take`	—	`inf_of_le_left`
`ofFn_take_get` 📖	mathematical	—	`take`	—	`inf_of_le_left`
`take_addCases_left` 📖	mathematical	—	`take`	—	—
`take_addCases_right` 📖	mathematical	—	`take`	—	—
`take_append_left` 📖	mathematical	—	`take` `append`	—	`take_addCases_left`
`take_append_right` 📖	mathematical	—	`take` `append`	—	`take_addCases_right`
`take_apply` 📖	mathematical	—	`take`	—	—
`take_eq_init` 📖	mathematical	—	`take` `init`	—	—
`take_eq_self` 📖	mathematical	—	`take` `le_refl` `Nat.instPreorder`	—	`le_refl`
`take_init` 📖	mathematical	—	`take` `init`	—	—
`take_one` 📖	mathematical	—	`take`	—	—
`take_repeat` 📖	mathematical	—	`take` `repeat`	—	—
`take_succ_eq_snoc` 📖	mathematical	—	`take` `snoc` `LT.lt.le` `Nat.instPreorder`	—	`LT.lt.le` `snoc_castSucc`
`take_take` 📖	mathematical	—	`take`	—	—
`take_update_of_ge` 📖	mathematical	—	`take` `Function.update`	—	`lt_of_lt_of_le` `Function.update_of_ne`
`take_update_of_lt` 📖	mathematical	—	`take` `Function.update`	—	`Function.update_self` `Function.update_of_ne`
`take_zero` 📖	mathematical	—	`take`	—	—

---

← Back to Index