Let X, Tx and W be given.
Assume Hnorm: normal_space X Tx.
Assume HWcov: open_cover X Tx W.
Assume HWlf: locally_finite_family X Tx W.
We will prove partition_of_unity_dominated X Tx W.
We will prove topology_on X Tx ∧ open_cover X Tx W ∧ ∃P : set, partition_of_unity_family X Tx W 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 HWcov.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (normal_space_implies_regular X Tx Hnorm).
We prove the intermediate claim HWopen: ∀w : set, w ∈ W → w ∈ Tx.
An exact proof term for the current goal is (andEL (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcov).
We prove the intermediate claim HWcovers: covers X W.
An exact proof term for the current goal is (andER (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcov).
We prove the intermediate claim HWsubPow: W ⊆ 𝒫 X.
An exact proof term for the current goal is (open_cover_family_sub X Tx W HTx HWcov).
An exact proof term for the current goal is (normal_locally_finite_partition_of_unity_family X Tx W Hnorm HWcov HWlf).
∎