Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eventually_maps_to_of_is_open_of_omega_limit_subset

Modification history