Let X, Tx, U, V and P be given.
Assume HP: partition_of_unity_family X Tx V P.
Assume Href: refine_of V U.
We will prove partition_of_unity_family X Tx U P.
We prove the intermediate claim HA: P ⊆ function_space X R.
An exact proof term for the current goal is (partition_of_unity_family_sub_function_space X Tx V P HP).
We prove the intermediate claim HB: ∀f : set, f ∈ P → continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (partition_of_unity_family_continuous X Tx V P HP).
We prove the intermediate claim HC: ∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval.
An exact proof term for the current goal is (partition_of_unity_family_unit_interval X Tx V P HP).
We prove the intermediate claim HDV: ∀f : set, f ∈ P → ∃v : set, v ∈ V ∧ support_of X Tx f ⊆ v.
An exact proof term for the current goal is (partition_of_unity_family_support_dominated X Tx V P HP).
We prove the intermediate claim HE: ∀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 (partition_of_unity_family_supports_locally_finite X Tx V P HP).
We prove the intermediate claim HF: ∀x : set, x ∈ X → ∃F : set, finite F ∧ F ⊆ P ∧ (∀f : set, f ∈ P → apply_fun f x ≠ 0 → f ∈ F) ∧ ∃n : set, n ∈ ω ∧ ∃e : set, bijection n F e ∧ ∃p : set, function_on p (ordsucc n) R ∧ apply_fun p Empty = 0 ∧ (∀k : set, k ∈ n → apply_fun p (ordsucc k) = add_SNo (apply_fun p k) (apply_fun (apply_fun e k) x)) ∧ apply_fun p n = 1.
An exact proof term for the current goal is (partition_of_unity_family_pointwise_finite_sum X Tx V P HP).
We prove the intermediate claim HdomU: ∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u.
Let f be given.
Assume HfP: f ∈ P.
Apply (HDV f HfP) to the current goal.
Let v be given.
Assume Hv: v ∈ V ∧ support_of X Tx f ⊆ v.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (v ∈ V) (support_of X Tx f ⊆ v) Hv).
We prove the intermediate claim Hsuppsubv: support_of X Tx f ⊆ v.
An exact proof term for the current goal is (andER (v ∈ V) (support_of X Tx f ⊆ v) Hv).
Apply (Href v HvV) to the current goal.
Let u be given.
Assume Hu: u ∈ U ∧ v ⊆ u.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (u ∈ U) (v ⊆ u) Hu).
An exact proof term for the current goal is (Subq_tra (support_of X Tx f) v u Hsuppsubv (andER (u ∈ U) (v ⊆ u) Hu)).
We will prove 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 → ∃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) ∧ (∀x : set, x ∈ X → ∃F : set, finite F ∧ F ⊆ P ∧ (∀f : set, f ∈ P → apply_fun f x ≠ 0 → f ∈ F) ∧ ∃n : set, n ∈ ω ∧ ∃e : set, bijection n F e ∧ ∃p : set, function_on p (ordsucc n) R ∧ apply_fun p Empty = 0 ∧ (∀k : set, k ∈ n → apply_fun p (ordsucc k) = add_SNo (apply_fun p k) (apply_fun (apply_fun e k) x)) ∧ apply_fun p n = 1).
Apply and6I to the current goal.
An exact proof term for the current goal is HA.
An exact proof term for the current goal is HB.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HdomU.
An exact proof term for the current goal is HE.
An exact proof term for the current goal is HF.
∎