Commit 2023-05-23 21:45 d4f691b9

View on Github →

feat(order/filter/basic): generalize some lemmas from nhds_within (#19070)

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.set_eventually_eq_iff_inf_principal

added theorem filter.set_eventually_le_iff_inf_principal_le

added theorem filter.set_eventually_le_iff_mem_inf_principal

Modified src/topology/continuous_on.lean