Let X, Tx, C and eps be given.
Assume Hpara: paracompact_space X Tx.
Assume HH: Hausdorff_space X Tx.
Assume Hloc: locally_finite_family X Tx C.
Assume HCsubPow: C ⊆ 𝒫 X.
Assume Heps: ∀c : set, c ∈ C → apply_fun eps c ∈ R ∧ Rlt 0 (apply_fun eps c).
We will prove ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ X → Rlt 0 (apply_fun f x)) ∧ (∀c x : set, c ∈ C → x ∈ c → Rle (apply_fun f x) (apply_fun eps c)).
We prove the intermediate claim Hnorm: normal_space X Tx.
An exact proof term for the current goal is (paracompact_Hausdorff_normal X Tx Hpara HH).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S) Hloc).
An exact proof term for the current goal is (paracompact_Hausdorff_locally_finite_bounded_function_aux X Tx C eps Hpara HH Hloc HCsubPow Heps Hnorm HTx).
∎