Commit 2024-10-21 09:29 5195b1b9

View on Github →

chore(Filter/Tendsto): split from Basic (#17959)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/Derangements/Exponential.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.EventuallyEq.comp_tendsto

deleted theorem Filter.Tendsto.comp

deleted theorem Filter.Tendsto.congr'

deleted theorem Filter.Tendsto.congr

deleted theorem Filter.Tendsto.eventually

deleted theorem Filter.Tendsto.eventually_mem

deleted theorem Filter.Tendsto.frequently

deleted theorem Filter.Tendsto.frequently_map

deleted theorem Filter.Tendsto.inf

deleted theorem Filter.Tendsto.mono_left

deleted theorem Filter.Tendsto.mono_right

deleted theorem Filter.Tendsto.neBot

deleted theorem Filter.Tendsto.not_tendsto

deleted theorem Filter.Tendsto.of_neBot_imp

deleted theorem Filter.Tendsto.of_tendsto_comp

deleted theorem Filter.Tendsto.sup

deleted theorem Filter.Tendsto.sup_sup

deleted theorem Filter.comap_eq_of_inverse

deleted theorem Filter.eventuallyEq_of_left_inv_of_right_inv

deleted theorem Filter.le_map_of_right_inverse

deleted theorem Filter.map_eq_of_inverse

deleted theorem Filter.map_inf_principal_preimage

deleted theorem Filter.map_mapsTo_Iic_iff_mapsTo

deleted theorem Filter.map_mapsTo_Iic_iff_tendsto

deleted theorem Filter.not_tendsto_iff_exists_frequently_nmem

deleted theorem Filter.pure_le_iff

deleted theorem Filter.tendsto_bot

deleted theorem Filter.tendsto_comap'_iff

deleted theorem Filter.tendsto_comap

deleted theorem Filter.tendsto_comap_iff

deleted theorem Filter.tendsto_congr'

deleted theorem Filter.tendsto_congr

deleted theorem Filter.tendsto_const_pure

deleted theorem Filter.tendsto_def

deleted theorem Filter.tendsto_iInf'

deleted theorem Filter.tendsto_iInf

deleted theorem Filter.tendsto_iInf_iInf

deleted theorem Filter.tendsto_iSup

deleted theorem Filter.tendsto_iSup_iSup

deleted theorem Filter.tendsto_id'

deleted theorem Filter.tendsto_id

deleted theorem Filter.tendsto_iff_comap

deleted theorem Filter.tendsto_iff_eventually

deleted theorem Filter.tendsto_iff_forall_eventually_mem

deleted theorem Filter.tendsto_inf

deleted theorem Filter.tendsto_inf_left

deleted theorem Filter.tendsto_inf_right

deleted theorem Filter.tendsto_map'_iff

deleted theorem Filter.tendsto_map

deleted theorem Filter.tendsto_of_isEmpty

deleted theorem Filter.tendsto_principal

deleted theorem Filter.tendsto_principal_principal

deleted theorem Filter.tendsto_pure

deleted theorem Filter.tendsto_pure_left

deleted theorem Filter.tendsto_pure_pure

deleted theorem Filter.tendsto_sup

deleted theorem Filter.tendsto_top

deleted theorem Set.MapsTo.tendsto

Modified Mathlib/Order/Filter/CardinalInter.lean

Modified Mathlib/Order/Filter/Extr.lean

Modified Mathlib/Order/Filter/Germ/Basic.lean

Modified Mathlib/Order/Filter/Partial.lean

Modified Mathlib/Order/Filter/Pi.lean

Modified Mathlib/Order/Filter/Prod.lean

Created Mathlib/Order/Filter/Tendsto.lean

added theorem Filter.EventuallyEq.comp_tendsto

added theorem Filter.Tendsto.comp

added theorem Filter.Tendsto.congr'

added theorem Filter.Tendsto.congr

added theorem Filter.Tendsto.eventually

added theorem Filter.Tendsto.eventually_mem

added theorem Filter.Tendsto.frequently

added theorem Filter.Tendsto.frequently_map

added theorem Filter.Tendsto.inf

added theorem Filter.Tendsto.mono_left

added theorem Filter.Tendsto.mono_right

added theorem Filter.Tendsto.neBot

added theorem Filter.Tendsto.not_tendsto

added theorem Filter.Tendsto.of_neBot_imp

added theorem Filter.Tendsto.of_tendsto_comp

added theorem Filter.Tendsto.sup

added theorem Filter.Tendsto.sup_sup

added theorem Filter.comap_eq_of_inverse

added theorem Filter.eventuallyEq_of_left_inv_of_right_inv

added theorem Filter.le_map_of_right_inverse

added theorem Filter.map_eq_of_inverse

added theorem Filter.map_inf_principal_preimage

added theorem Filter.map_mapsTo_Iic_iff_mapsTo

added theorem Filter.map_mapsTo_Iic_iff_tendsto

added theorem Filter.not_tendsto_iff_exists_frequently_nmem

added theorem Filter.pure_le_iff

added theorem Filter.tendsto_bot

added theorem Filter.tendsto_comap'_iff

added theorem Filter.tendsto_comap

added theorem Filter.tendsto_comap_iff

added theorem Filter.tendsto_congr'

added theorem Filter.tendsto_congr

added theorem Filter.tendsto_const_pure

added theorem Filter.tendsto_def

added theorem Filter.tendsto_iInf'

added theorem Filter.tendsto_iInf

added theorem Filter.tendsto_iInf_iInf

added theorem Filter.tendsto_iSup

added theorem Filter.tendsto_iSup_iSup

added theorem Filter.tendsto_id'

added theorem Filter.tendsto_id

added theorem Filter.tendsto_iff_comap

added theorem Filter.tendsto_iff_eventually

added theorem Filter.tendsto_iff_forall_eventually_mem

added theorem Filter.tendsto_inf

added theorem Filter.tendsto_inf_left

added theorem Filter.tendsto_inf_right

added theorem Filter.tendsto_map'_iff

added theorem Filter.tendsto_map

added theorem Filter.tendsto_of_isEmpty

added theorem Filter.tendsto_principal

added theorem Filter.tendsto_principal_principal

added theorem Filter.tendsto_pure

added theorem Filter.tendsto_pure_left

added theorem Filter.tendsto_pure_pure

added theorem Filter.tendsto_sup

added theorem Filter.tendsto_top

added theorem Set.MapsTo.tendsto

Modified Mathlib/Topology/Compactness/Compact.lean