Commit 2023-12-17 15:16 92d4b01a

feat: add topological lemmas for ULift (#8958) This also adds a handful of easy instances Arguably the topological space instance should be defined via coinduced to make these true by Iff.rfl, but that creates a headache with constructors for normed spaces, so is not in this PR.