mathlib

78af5b16 - feat(topology): closure in a `pi` space (#6575)

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.