Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-02 20:45 838dc66e

View on Github →

feat(topology/basic): add eventually_eventually_nhds (#3266)

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.bind_inf_principal

added theorem filter.bind_le

deleted theorem filter.bind_mono2

modified theorem filter.bind_mono

deleted theorem filter.bind_sup

added theorem filter.eventually_bind

added theorem filter.eventually_eq.le

added theorem filter.eventually_eq.trans_le

added theorem filter.eventually_eq_bind

added theorem filter.eventually_le.antisymm

added theorem filter.eventually_le.congr

added theorem filter.eventually_le.refl

added theorem filter.eventually_le.trans

added theorem filter.eventually_le.trans_eq

added def filter.eventually_le

added theorem filter.eventually_le_bind

added theorem filter.eventually_le_congr

modified theorem filter.inf_principal_ne_bot_iff

added theorem filter.join_le

added theorem filter.join_mono

added theorem filter.mem_bind_sets'

added theorem filter.sup_bind

Modified src/order/filter/germ.lean

deleted theorem filter.eventually_eq.le

deleted theorem filter.eventually_eq.trans_le

deleted theorem filter.eventually_le.antisymm

deleted theorem filter.eventually_le.congr

deleted theorem filter.eventually_le.refl

deleted theorem filter.eventually_le.trans

deleted theorem filter.eventually_le.trans_eq

deleted def filter.eventually_le

deleted theorem filter.eventually_le_congr

Modified src/topology/basic.lean

added theorem cluster_pt_principal_iff

added theorem eventually_eventually_eq_nhds

added theorem eventually_eventually_le_nhds

added theorem eventually_eventually_nhds

added theorem eventually_nhds_iff

added theorem filter.eventually.eventually_nhds

added theorem filter.eventually_eq.eventually_eq_nhds

added theorem filter.eventually_le.eventually_le_nhds

added theorem nhds_bind_nhds

Modified src/topology/continuous_on.lean

added theorem eventually_nhds_nhds_within

added theorem eventually_nhds_within_iff

added theorem eventually_nhds_within_nhds_within

added theorem nhds_bind_nhds_within