Transport bounded/frontier statements along a homeomorphism of proper spaces

When moving a planar theorem from ℂ to another 2-dimensional normed space E (via ContinuousLinearEquiv.ofFinrankEq) or along an affine homeomorphism, the fiddly part is IsBounded. Rewriting L '' (L ⁻¹' s) failed: the coercions ⇑↑L and ⇑L.toAddEquiv.toEquiv do not match syntactically, and ContinuousLinearEquiv.lipschitz is deprecated in recent Mathlib. A coercion-free route for any homeomorphism between proper spaces: IsBounded s → (s.isCompact_closure.image h.continuous).isBounded.subset (image_mono subset_closure), or .subset with an explicit witness ⟨L.symm y, subset_closure _, by simp⟩. For the other conditions, use preimages: Homeomorph.preimage_frontier, Homeomorph.isConnected_preimage, Disjoint.preimage, preimage_union/preimage_compl, and Equiv.preimage_image for the curve itself.