Meagre images over Lindelöf sets #
Meagreness of an image can be checked locally on a Lindelöf set: if every point of a Lindelöf
set U has a neighbourhood N such that f '' (N ∩ S) is meagre, then so is f '' (U ∩ S),
because countably many of these neighbourhoods cover U and a countable union of meagre sets is
meagre. This is the local-to-global step of the Sard and Sard--Smale theorems, in which S is a
set of critical points.
theorem
IsLindelof.isMeagre_image_inter_of_forall_exists_mem_nhds
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{U S : Set X}
{f : X → Y}
(hU : IsLindelof U)
(h : ∀ x ∈ U, ∃ N ∈ nhds x, IsMeagre (f '' (N ∩ S)))
:
If every point of a Lindelöf set U has a neighbourhood N such that f '' (N ∩ S) is
meagre, then f '' (U ∩ S) is meagre, since countably many of these neighbourhoods cover U.