Let X, Tx and U be given.
Assume Hnorm: normal_space X Tx.
Assume HUfin: finite U.
Assume HUcov: open_cover X Tx U.
We will prove ∃P : set, partition_of_unity_family X Tx U P.
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 Hlf: locally_finite_family X Tx U.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ U ∧ ∀A : set, A ∈ U → A ∩ N ≠ Empty → A ∈ S.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We use X to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
An exact proof term for the current goal is HxX.
We use U to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUfin.
An exact proof term for the current goal is (Subq_ref U).
Let A be given.
Assume HA: A ∈ U.
Assume _: A ∩ X ≠ Empty.
An exact proof term for the current goal is HA.
An exact proof term for the current goal is (normal_locally_finite_partition_of_unity_family X Tx U Hnorm HUcov Hlf).
∎