Meagre sets in local coordinates

An open partial homeomorphism preserves meagreness on its source. In particular, a meagre set in an open coordinate domain remains meagre in the ambient space after applying a chart inverse. The source restriction is essential: the function outside the source is unconstrained.

theorem OpenPartialHomeomorph.isMeagre_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsMeagre s) (hse : s ⊆ e.source) : IsMeagre (↑e '' s)

An open partial homeomorphism sends a meagre subset of its source to a meagre set in the ambient target space.