Let X, Tx and U be given.
Assume Hpara: paracompact_space X Tx.
Assume HH: Hausdorff_space X Tx.
Assume Hcover: open_cover X Tx U.
We will prove partition_of_unity_dominated X Tx U.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HH).
We prove the intermediate claim Hbump: ∃V P : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U ∧ P ⊆ function_space X R ∧ (∀f : set, f ∈ P → continuous_map X Tx R R_standard_topology f) ∧ (∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval) ∧ (∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u) ∧ (∀x : set, x ∈ X → ∃f : set, f ∈ P ∧ apply_fun f x = 1) ∧ (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0).
An exact proof term for the current goal is (paracompact_Hausdorff_bump_cover_dominated X Tx U Hpara HH Hcover).
Apply Hbump to the current goal.
Let V be given.
Assume HexP.
Apply HexP to the current goal.
Let P be given.
Assume HVP: open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U ∧ P ⊆ function_space X R ∧ (∀f : set, f ∈ P → continuous_map X Tx R R_standard_topology f) ∧ (∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval) ∧ (∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u) ∧ (∀x : set, x ∈ X → ∃f : set, f ∈ P ∧ apply_fun f x = 1) ∧ (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0).
Apply HVP to the current goal.
Assume HVP0 HPlf.
Apply HVP0 to the current goal.
Assume HVP1 HPone.
Apply HVP1 to the current goal.
Assume HVP2 HPdom.
Apply HVP2 to the current goal.
Assume HVP3 HPui.
Apply HVP3 to the current goal.
Assume HVP4 HPcont.
Apply HVP4 to the current goal.
Assume HVP5 HPsubFS.
Apply HVP5 to the current goal.
Assume HVcovlf HVref.
Apply HVcovlf to the current goal.
Assume HVcov HVlf.
We prove the intermediate claim HPpack: P ⊆ function_space X R ∧ (∀f : set, f ∈ P → continuous_map X Tx R R_standard_topology f) ∧ (∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval) ∧ (∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u) ∧ (∀x : set, x ∈ X → ∃f : set, f ∈ P ∧ apply_fun f x = 1) ∧ (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0).
Apply and6I to the current goal.
An exact proof term for the current goal is HPsubFS.
An exact proof term for the current goal is HPcont.
An exact proof term for the current goal is HPui.
An exact proof term for the current goal is HPdom.
An exact proof term for the current goal is HPone.
An exact proof term for the current goal is HPlf.
An exact proof term for the current goal is (locally_finite_bump_cover_normalizes_to_partition_of_unity_dominated X Tx U V P HTx Hcover HVcov HVlf HVref HPpack).
∎