Commit 2024-11-12 16:48 7fd10963

feat(Topology/ShrinkingLemma): add a predicate on refined open sets (#18827) add a predicate p : Set X → Prop for PartialRefinent. All the existing theorems remain valid by taking fun _ => True as p. motivation: with this we can require that the refined open set has a compact closure, by taking fun w => IsCompact (closure w) as p. This can be applied when X is locally compact and T2, and we can obtain a PartitionOfUnity for an open cover of a compact set. (This will be done in #12266) This splits from #12266