Let X, Tx and U be given.
Assume Hnorm: normal_space X Tx.
Assume Hfin: finite U.
Assume Hcover: open_cover X Tx U.
We will prove partition_of_unity_dominated X Tx U.
We will prove topology_on X Tx ∧ open_cover X Tx U ∧ ∃P : set, partition_of_unity_family X Tx U P.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
An exact proof term for the current goal is Hcover.
An exact proof term for the current goal is (finite_open_cover_has_partition_of_unity_family X Tx U Hnorm Hfin Hcover).
∎