Lemmas

📁 Source: Batteries/Data/Fin/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `bind_find?_isSome`, `bind_findRev?_isSome`, `bind_findSome?_guard_isSome`, `bind_findSomeRev?_guard_isSome`, `coe_clamp`, `coe_divNat`, `coe_mkDivMod`, `coe_modNat`, `countP_eq_countP_map_finRange`, `countP_le`, `countP_one`, `countP_succ`, `countP_zero`, `divNat_mkDivMod`, `divNat_mkDivMod_modNat`, `eq_false_of_find?_eq_none`, `eq_false_of_find?_eq_some_of_lt`, `eq_false_of_findRev?_eq_none`, `eq_false_of_findRev?_eq_some_of_lt`, `eq_false_of_isNone_find?`, `eq_false_of_isNone_findRev?`, `eq_none_of_findSome?_eq_none`, `eq_none_of_findSomeRev?_eq_none`, `eq_true_of_find?_eq_some`, `eq_true_of_findRev?_eq_some`, `exists_eq_some_of_findSome?_eq_some`, `exists_eq_some_of_findSomeRev?_eq_some`, `exists_eq_true_iff_exists_maximal_eq_true`, `exists_eq_true_iff_exists_minimal_eq_true`, `exists_eq_true_of_isSome_find?`, `exists_eq_true_of_isSome_findRev?`, `exists_iff_exists_maximal`, `exists_iff_exists_minimal`, `exists_isSome_of_isSome_findSome?`, `exists_isSome_of_isSome_findSomeRev?`, `exists_minimal_of_findSome?_eq_some`, `exists_minimal_of_findSomeRev?_eq_some`, `exists_of_findSome?_eq_some`, `find?_eq_find?_finRange`, `find?_eq_findRev?_iff`, `find?_eq_none_iff`, `find?_eq_some_iff`, `find?_isNone_iff`, `find?_isSome_iff`, `find?_le_findRev?`, `find?_one`, `find?_rev`, `find?_succ`, `find?_zero`, `findRev?_eq_none_iff`, `findRev?_eq_some_iff`, `findRev?_one`, `findRev?_rev`, `findRev?_succ`, `findRev?_zero`, `findSome?_eq_findSome?_finRange`, `findSome?_eq_none_iff`, `findSome?_eq_some_iff`, `findSome?_guard`, `findSome?_isNone_iff`, `findSome?_isSome_iff`, `findSome?_one`, `findSome?_rev`, `findSome?_succ`, `findSome?_succ_of_isNone`, `findSome?_succ_of_isSome`, `findSome?_succ_of_none`, `findSome?_succ_of_some`, `findSome?_zero`, `findSomeRev?_eq_none_iff`, `findSomeRev?_eq_some_iff`, `findSomeRev?_guard`, `findSomeRev?_one`, `findSomeRev?_rev`, `findSomeRev?_succ`, `findSomeRev?_zero`, `foldl_assoc`, `foldr_assoc`, `get_find?_eq_true`, `get_find?_minimal`, `get_findRev?_eq_true`, `get_findRev?_maximal`, `isNone_find?_iff`, `isNone_findRev?_iff`, `isNone_findSome?_iff`, `isNone_findSomeRev?_iff`, `isNone_of_isNone_findSome?`, `isNone_of_isNone_findSomeRev?`, `isSome_find?_iff`, `isSome_find?_of_eq_true`, `isSome_findRev?_iff`, `isSome_findRev?_of_eq_true`, `isSome_findSome?_iff`, `isSome_findSome?_of_isSome`, `isSome_findSomeRev?_iff`, `isSome_findSomeRev?_of_isSome`, `map_findSome?`, `map_findSomeRev?`, `map_rev_find?`, `map_rev_findRev?`, `modNat_mkDivMod`, `prod_eq_prod_map_finRange`, `prod_succ`, `prod_zero`, `sum_eq_sum_map_finRange`, `sum_succ`, `sum_zero`	107
Total	107

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_find?_isSome` 📖	mathematical	—	`find?` `findSome?`	—	`bind_findSome?_guard_isSome`
`bind_findRev?_isSome` 📖	mathematical	—	`findRev?` `findSomeRev?`	—	`bind_findSomeRev?_guard_isSome`
`bind_findSome?_guard_isSome` 📖	mathematical	—	`findSome?`	—	—
`bind_findSomeRev?_guard_isSome` 📖	mathematical	—	`findSomeRev?`	—	—
`coe_clamp` 📖	mathematical	—	`clamp`	—	—
`coe_divNat` 📖	mathematical	—	`divNat`	—	—
`coe_mkDivMod` 📖	mathematical	—	`mkDivMod`	—	—
`coe_modNat` 📖	mathematical	—	`modNat`	—	—
`countP_eq_countP_map_finRange` 📖	mathematical	—	`countP`	—	`countP_succ`
`countP_le` 📖	mathematical	—	`countP`	—	`countP_zero` `countP_succ`
`countP_one` 📖	mathematical	—	`countP`	—	`sum_eq_sum_map_finRange`
`countP_succ` 📖	mathematical	—	`countP`	—	`sum_eq_sum_map_finRange`
`countP_zero` 📖	mathematical	—	`countP`	—	`sum_zero`
`divNat_mkDivMod` 📖	mathematical	—	`divNat` `mkDivMod`	—	—
`divNat_mkDivMod_modNat` 📖	mathematical	—	`mkDivMod` `divNat` `modNat`	—	—
`eq_false_of_find?_eq_none` 📖	—	`find?`	—	—	`find?_eq_none_iff`
`eq_false_of_find?_eq_some_of_lt` 📖	—	`find?`	—	—	`find?_eq_some_iff`
`eq_false_of_findRev?_eq_none` 📖	—	`findRev?`	—	—	`findRev?_eq_none_iff`
`eq_false_of_findRev?_eq_some_of_lt` 📖	—	`findRev?`	—	—	`findRev?_eq_some_iff`
`eq_false_of_isNone_find?` 📖	—	`find?`	—	—	`isNone_find?_iff`
`eq_false_of_isNone_findRev?` 📖	—	`findRev?`	—	—	`isNone_findRev?_iff`
`eq_none_of_findSome?_eq_none` 📖	—	`findSome?`	—	—	`findSome?_eq_none_iff`
`eq_none_of_findSomeRev?_eq_none` 📖	—	`findSomeRev?`	—	—	`findSomeRev?_eq_none_iff`
`eq_true_of_find?_eq_some` 📖	—	`find?`	—	—	`find?_eq_some_iff`
`eq_true_of_findRev?_eq_some` 📖	—	`findRev?`	—	—	`findRev?_eq_some_iff`
`exists_eq_some_of_findSome?_eq_some` 📖	—	`findSome?`	—	—	—
`exists_eq_some_of_findSomeRev?_eq_some` 📖	—	`findSomeRev?`	—	—	—
`exists_eq_true_iff_exists_maximal_eq_true` 📖	—	—	—	—	—
`exists_eq_true_iff_exists_minimal_eq_true` 📖	—	—	—	—	—
`exists_eq_true_of_isSome_find?` 📖	—	`find?`	—	—	`isSome_find?_iff`
`exists_eq_true_of_isSome_findRev?` 📖	—	`findRev?`	—	—	`isSome_findRev?_iff`
`exists_iff_exists_maximal` 📖	—	—	—	—	—
`exists_iff_exists_minimal` 📖	—	—	—	—	—
`exists_isSome_of_isSome_findSome?` 📖	—	`findSome?`	—	—	`isSome_findSome?_iff`
`exists_isSome_of_isSome_findSomeRev?` 📖	—	`findSomeRev?`	—	—	`isSome_findSomeRev?_iff`
`exists_minimal_of_findSome?_eq_some` 📖	—	`findSome?`	—	—	`findSome?_eq_some_iff`
`exists_minimal_of_findSomeRev?_eq_some` 📖	—	`findSomeRev?`	—	—	`findSomeRev?_eq_some_iff`
`exists_of_findSome?_eq_some` 📖	—	`findSome?`	—	—	`exists_eq_some_of_findSome?_eq_some`
`find?_eq_find?_finRange` 📖	mathematical	—	`find?`	—	`findSome?_eq_findSome?_finRange`
`find?_eq_findRev?_iff` 📖	mathematical	—	`find?` `findRev?`	—	—
`find?_eq_none_iff` 📖	mathematical	—	`find?`	—	—
`find?_eq_some_iff` 📖	mathematical	—	`find?`	—	—
`find?_isNone_iff` 📖	mathematical	—	`find?`	—	`isNone_find?_iff`
`find?_isSome_iff` 📖	mathematical	—	`find?`	—	`isSome_find?_iff`
`find?_le_findRev?` 📖	mathematical	—	`find?` `findRev?`	—	—
`find?_one` 📖	mathematical	—	`find?`	—	`findSome?_one`
`find?_rev` 📖	mathematical	—	`find?` `findRev?`	—	`map_findSomeRev?`
`find?_succ` 📖	mathematical	—	`find?`	—	`findSome?_succ` `map_findSome?`
`find?_zero` 📖	mathematical	—	`find?`	—	`findSome?_zero`
`findRev?_eq_none_iff` 📖	mathematical	—	`findRev?`	—	—
`findRev?_eq_some_iff` 📖	mathematical	—	`findRev?`	—	—
`findRev?_one` 📖	mathematical	—	`findRev?`	—	—
`findRev?_rev` 📖	mathematical	—	`findRev?` `find?`	—	`map_findSome?`
`findRev?_succ` 📖	mathematical	—	`findRev?`	—	`findSomeRev?_succ` `map_findSomeRev?`
`findRev?_zero` 📖	mathematical	—	`findRev?`	—	—
`findSome?_eq_findSome?_finRange` 📖	mathematical	—	`findSome?`	—	`findSome?_zero` `findSome?_succ`
`findSome?_eq_none_iff` 📖	mathematical	—	`findSome?`	—	`findSome?_zero` `findSome?_succ`
`findSome?_eq_some_iff` 📖	mathematical	—	`findSome?`	—	`findSome?_zero` `findSome?_succ`
`findSome?_guard` 📖	mathematical	—	`findSome?` `find?`	—	—
`findSome?_isNone_iff` 📖	mathematical	—	`findSome?`	—	`isNone_findSome?_iff`
`findSome?_isSome_iff` 📖	mathematical	—	`findSome?`	—	`isSome_findSome?_iff`
`findSome?_one` 📖	mathematical	—	`findSome?`	—	—
`findSome?_rev` 📖	mathematical	—	`findSome?` `findSomeRev?`	—	—
`findSome?_succ` 📖	mathematical	—	`findSome?`	—	`foldl_assoc`
`findSome?_succ_of_isNone` 📖	mathematical	—	`findSome?`	—	`findSome?_succ`
`findSome?_succ_of_isSome` 📖	mathematical	—	`findSome?`	—	`findSome?_succ`
`findSome?_succ_of_none` 📖	mathematical	—	`findSome?`	—	`findSome?_succ`
`findSome?_succ_of_some` 📖	mathematical	—	`findSome?`	—	`findSome?_succ`
`findSome?_zero` 📖	mathematical	—	`findSome?`	—	—
`findSomeRev?_eq_none_iff` 📖	mathematical	—	`findSomeRev?`	—	`findSome?_eq_none_iff`
`findSomeRev?_eq_some_iff` 📖	mathematical	—	`findSomeRev?`	—	`findSome?_eq_some_iff`
`findSomeRev?_guard` 📖	mathematical	—	`findSomeRev?` `findRev?`	—	—
`findSomeRev?_one` 📖	mathematical	—	`findSomeRev?`	—	`findSome?_one`
`findSomeRev?_rev` 📖	mathematical	—	`findSomeRev?` `findSome?`	—	—
`findSomeRev?_succ` 📖	mathematical	—	`findSomeRev?`	—	`findSome?_succ`
`findSomeRev?_zero` 📖	mathematical	—	`findSomeRev?`	—	`findSome?_zero`
`foldl_assoc` 📖	—	—	—	—	—
`foldr_assoc` 📖	—	—	—	—	`foldl_assoc`
`get_find?_eq_true` 📖	—	`find?`	—	—	`eq_true_of_find?_eq_some`
`get_find?_minimal` 📖	—	`find?`	—	—	`eq_false_of_find?_eq_some_of_lt`
`get_findRev?_eq_true` 📖	—	`findRev?`	—	—	`eq_true_of_findRev?_eq_some`
`get_findRev?_maximal` 📖	—	`findRev?`	—	—	`eq_false_of_findRev?_eq_some_of_lt`
`isNone_find?_iff` 📖	mathematical	—	`find?`	—	—
`isNone_findRev?_iff` 📖	mathematical	—	`findRev?`	—	—
`isNone_findSome?_iff` 📖	mathematical	—	`findSome?`	—	—
`isNone_findSomeRev?_iff` 📖	mathematical	—	`findSomeRev?`	—	—
`isNone_of_isNone_findSome?` 📖	—	`findSome?`	—	—	`isNone_findSome?_iff`
`isNone_of_isNone_findSomeRev?` 📖	—	`findSomeRev?`	—	—	`isNone_findSomeRev?_iff`
`isSome_find?_iff` 📖	mathematical	—	`find?`	—	—
`isSome_find?_of_eq_true` 📖	mathematical	—	`find?`	—	`isSome_find?_iff`
`isSome_findRev?_iff` 📖	mathematical	—	`findRev?`	—	—
`isSome_findRev?_of_eq_true` 📖	mathematical	—	`findRev?`	—	`isSome_findRev?_iff`
`isSome_findSome?_iff` 📖	mathematical	—	`findSome?`	—	—
`isSome_findSome?_of_isSome` 📖	mathematical	—	`findSome?`	—	`isSome_findSome?_iff`
`isSome_findSomeRev?_iff` 📖	mathematical	—	`findSomeRev?`	—	—
`isSome_findSomeRev?_of_isSome` 📖	mathematical	—	`findSomeRev?`	—	`isSome_findSomeRev?_iff`
`map_findSome?` 📖	mathematical	—	`findSome?`	—	`findSome?_zero` `findSome?_succ`
`map_findSomeRev?` 📖	mathematical	—	`findSomeRev?`	—	—
`map_rev_find?` 📖	mathematical	—	`find?` `findRev?`	—	—
`map_rev_findRev?` 📖	mathematical	—	`findRev?` `find?`	—	—
`modNat_mkDivMod` 📖	mathematical	—	`modNat` `mkDivMod`	—	—
`prod_eq_prod_map_finRange` 📖	mathematical	—	`prod` `List.prod`	—	—
`prod_succ` 📖	mathematical	—	`prod`	—	—
`prod_zero` 📖	mathematical	—	`prod`	—	—
`sum_eq_sum_map_finRange` 📖	mathematical	—	`sum`	—	—
`sum_succ` 📖	mathematical	—	`sum`	—	—
`sum_zero` 📖	mathematical	—	`sum`	—	—

---

← Back to Index