BubbleSortInduction

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

Statistics

Metric	Count
Definitions	0
Theorems bubble_sort_induction, bubble_sort_induction'	2
Total	2

Tuple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bubble_sort_induction 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.swap	sort	—	bubble_sort_induction'
bubble_sort_induction' 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.swap	sort	—	WellFounded.induction_bot' IsWellFounded.wf Finite.to_wellFoundedLT Equiv.finite_left Finite.of_fintype antitone_pair_of_not_sorted' Pi.lex_desc LT.lt.le

---

← Back to Index