Commit 2021-03-09 21:43 78af5b16

View on Github →

feat(topology): closure in a pi space (#6575) Also add can_lift instances that lift f : subtype p → β to f : α → β and a version of filter.mem_infi_iff that uses a globally defined function.

Estimated changes

Modified src/data/set/basic.lean

Modified src/data/set/function.lean

added theorem set.pi_piecewise

added theorem set.univ_pi_piecewise

Modified src/order/filter/basic.lean

modified theorem filter.inf_principal_eq_bot

added theorem filter.infi_principal_finite

added theorem filter.mem_infi_iff'

Modified src/order/lattice.lean

added theorem inf_right_comm

added theorem sup_right_comm

Modified src/tactic/lift.lean

Modified src/topology/algebra/group.lean

Modified src/topology/algebra/ordered.lean

Modified src/topology/constructions.lean

added theorem is_closed_set_pi

Modified src/topology/continuous_on.lean

added theorem closure_pi_set

added theorem dense_pi

added theorem mem_closure_pi

added theorem nhds_within_pi_eq'

added theorem nhds_within_pi_eq

added theorem nhds_within_pi_eq_bot

added theorem nhds_within_pi_ne_bot

added theorem nhds_within_pi_univ_eq

added theorem nhds_within_pi_univ_eq_bot