Commit 2023-02-27 11:35 86d79e14

View on Github →

feat: Port Dynamics.OmegaLimit (#2490)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/OmegaLimit.lean

added theorem Flow.isInvariant_omegaLimit

added theorem Flow.omegaLimit_image_eq

added theorem Flow.omegaLimit_image_subset

added theorem Flow.omegaLimit_omegaLimit

added theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset'

added theorem eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset

added theorem eventually_closure_subset_of_isOpen_of_omegaLimit_subset

added theorem eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset

added theorem eventually_mapsTo_of_isOpen_of_omegaLimit_subset

added theorem isClosed_omegaLimit

added theorem mapsTo_omegaLimit

added theorem mapsTo_omega_limit'

added theorem mem_omegaLimit_iff_frequently

added theorem mem_omegaLimit_iff_frequently₂

added theorem mem_omegaLimit_singleton_iff_map_cluster_point

added theorem nonempty_omegaLimit

added theorem nonempty_omegaLimit_of_isCompact_absorbing

added def omegaLimit

added theorem omegaLimit_def

added theorem omegaLimit_eq_bInter_inter

added theorem omegaLimit_eq_interᵢ

added theorem omegaLimit_eq_interᵢ_inter

added theorem omegaLimit_image_eq

added theorem omegaLimit_inter

added theorem omegaLimit_interᵢ

added theorem omegaLimit_mono_left

added theorem omegaLimit_mono_right

added theorem omegaLimit_preimage_subset

added theorem omegaLimit_subset_closure_fw_image

added theorem omegaLimit_subset_of_tendsto

added theorem omegaLimit_union

added theorem omegaLimit_unionᵢ