I was looking for Set.union_subset in the Sets tab but it was in the Set which only contains that theorem. This caused some minor friction while playing level 7 in linear independence and span world.
My suggestion is to move Set.union_subset to the Sets tab and remove the Set tab.
Similarly for \R and real numbers tabs , \C and complex numbers tabs. The real numbers tabs can be merged together and the complex numbers tabs can be merged together.
I was looking for
Set.union_subsetin theSetstab but it was in theSetwhich only contains that theorem. This caused some minor friction while playing level 7 in linear independence and span world.My suggestion is to move
Set.union_subsetto theSetstab and remove theSettab.Similarly for
\Rand real numbers tabs ,\Cand complex numbers tabs. The real numbers tabs can be merged together and the complex numbers tabs can be merged together.