Let X, Tx, U and W be given.
Assume Hnorm: normal_space X Tx.
Assume HUcov: open_cover X Tx U.
Assume HWcov: open_cover X Tx W.
Assume HWlf: locally_finite_family X Tx W.
Assume Href: refine_of W U.
We will prove partition_of_unity_dominated X Tx U.
We prove the intermediate claim HPW: partition_of_unity_dominated X Tx W.
An exact proof term for the current goal is (normal_locally_finite_partition_of_unity_dominated X Tx W Hnorm HWcov HWlf).
An exact proof term for the current goal is (partition_of_unity_dominated_refine X Tx U W HUcov HPW Href).
∎