Let X, Tx and U be given.
Assume Hpara: paracompact_space X Tx.
Assume HH: Hausdorff_space X Tx.
Assume HUcov: open_cover X Tx U.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀U0 : set, open_cover X Tx U0 → ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 U0) Hpara).
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 HexVW: ∃V W : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U ∧ (∀v : set, v ∈ V → ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u) ∧ open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W V ∧ (∀w : set, w ∈ W → ∃v : set, v ∈ V ∧ closure_of X Tx w ⊆ v).
An exact proof term for the current goal is (shrinking_lemma_41_6_twice X Tx U Hpara HH HUcov).
Apply HexVW to the current goal.
Let V be given.
Assume HexW.
Apply HexW to the current goal.
Let W be given.
Assume HVW: (open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U ∧ (∀v : set, v ∈ V → ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u) ∧ open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W V) ∧ (∀w : set, w ∈ W → ∃v : set, v ∈ V ∧ closure_of X Tx w ⊆ v).
Apply HVW to the current goal.
Assume HVWleft HWcl.
Apply HVWleft to the current goal.
Assume HVW6 HWref.
Apply HVW6 to the current goal.
Assume HVW5 HWlf.
Apply HVW5 to the current goal.
Assume HVW4 HWcov.
Apply HVW4 to the current goal.
Assume HVW3 HVcl.
Apply HVW3 to the current goal.
Assume HVW2 HVref.
Apply HVW2 to the current goal.
Assume HVcov HVlf.
We prove the intermediate claim HVTx: ∀v : set, v ∈ V → v ∈ Tx.
An exact proof term for the current goal is (andEL (∀v : set, v ∈ V → v ∈ Tx) (covers X V) HVcov).
We prove the intermediate claim HVcovers: covers X V.
An exact proof term for the current goal is (andER (∀v : set, v ∈ V → v ∈ Tx) (covers X V) HVcov).
We prove the intermediate claim HWTx: ∀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 HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HVsubX: ∀v : set, v ∈ V → v ⊆ X.
Let v be given.
Assume HvV: v ∈ V.
An exact proof term for the current goal is (PowerE X v (HTsub v (HVTx v HvV))).
We prove the intermediate claim HWsubX: ∀w : set, w ∈ W → w ⊆ X.
Let w be given.
Assume HwW: w ∈ W.
An exact proof term for the current goal is (PowerE X w (HTsub w (HWTx w HwW))).
Set pickV to be the term λw : set ⇒ Eps_i (λv0 : set ⇒ v0 ∈ V ∧ closure_of X Tx w ⊆ v0).
We prove the intermediate claim HpickV: ∀w : set, w ∈ W → pickV w ∈ V ∧ closure_of X Tx w ⊆ pickV w.
Let w be given.
Assume HwW: w ∈ W.
We prove the intermediate claim Hexv: ∃v0 : set, v0 ∈ V ∧ closure_of X Tx w ⊆ v0.
An exact proof term for the current goal is (HWcl w HwW).
An exact proof term for the current goal is (Eps_i_ex (λv0 : set ⇒ v0 ∈ V ∧ closure_of X Tx w ⊆ v0) Hexv).
Set W_of to be the term λv : set ⇒ {w ∈ W|pickV w = v}.
Set Cl_of to be the term λv : set ⇒ {closure_of X Tx w|w ∈ (W_of v)}.
Set A_of to be the term λv : set ⇒ ⋃ (Cl_of v).
We prove the intermediate claim HA_of_closed_sub: ∀v : set, v ∈ V → closed_in X Tx (A_of v) ∧ A_of v ⊆ v.
Let v be given.
Assume HvV: v ∈ V.
Set Fam to be the term Cl_of v.
We prove the intermediate claim HclFam: ∀C : set, C ∈ Fam → closed_in X Tx C.
Let C be given.
Assume HC: C ∈ Fam.
Apply (ReplE_impred (W_of v) (λw0 : set ⇒ closure_of X Tx w0) C HC (closed_in X Tx C)) to the current goal.
Let w be given.
Assume Hw: w ∈ W_of v.
Assume Heq: C = closure_of X Tx w.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (SepE1 W (λw0 : set ⇒ pickV w0 = v) w Hw).
An exact proof term for the current goal is (closure_is_closed X Tx w HTx (HWsubX w HwW)).
We prove the intermediate claim HClWlf: locally_finite_family X Tx {closure_of X Tx w|w ∈ W}.
An exact proof term for the current goal is (locally_finite_family_closures X Tx W HWlf).
We prove the intermediate claim HFamSub: Fam ⊆ {closure_of X Tx w|w ∈ W}.
Let C be given.
Assume HC: C ∈ Fam.
Apply (ReplE_impred (W_of v) (λw0 : set ⇒ closure_of X Tx w0) C HC (C ∈ {closure_of X Tx w|w ∈ W})) to the current goal.
Let w be given.
Assume Hw: w ∈ W_of v.
Assume Heq: C = closure_of X Tx w.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (SepE1 W (λw0 : set ⇒ pickV w0 = v) w Hw).
An exact proof term for the current goal is (ReplI W (λw0 : set ⇒ closure_of X Tx w0) w HwW).
We prove the intermediate claim HLFam: locally_finite_family X Tx Fam.
An exact proof term for the current goal is (locally_finite_subfamily X Tx {closure_of X Tx w|w ∈ W} Fam HClWlf HFamSub).
We prove the intermediate claim HAcl: closed_in X Tx (A_of v).
We prove the intermediate claim HeqA: A_of v = ⋃ Fam.
Use reflexivity.
rewrite the current goal using HeqA (from left to right).
An exact proof term for the current goal is (Union_locally_finite_closed_is_closed X Tx Fam HLFam HclFam).
We prove the intermediate claim HAsub: A_of v ⊆ v.
Let x be given.
Assume Hx: x ∈ A_of v.
Apply (UnionE_impred Fam x Hx (x ∈ v)) to the current goal.
Let C be given.
Assume HxC: x ∈ C.
Assume HC: C ∈ Fam.
Apply (ReplE_impred (W_of v) (λw0 : set ⇒ closure_of X Tx w0) C HC (x ∈ v)) to the current goal.
Let w be given.
Assume Hw: w ∈ W_of v.
Assume Heq: C = closure_of X Tx w.
We prove the intermediate claim Hxcl: x ∈ closure_of X Tx w.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HxC.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (SepE1 W (λw0 : set ⇒ pickV w0 = v) w Hw).
We prove the intermediate claim Heqv: pickV w = v.
An exact proof term for the current goal is (SepE2 W (λw0 : set ⇒ pickV w0 = v) w Hw).
We prove the intermediate claim Hvpack: pickV w ∈ V ∧ closure_of X Tx w ⊆ pickV w.
An exact proof term for the current goal is (HpickV w HwW).
We prove the intermediate claim Hclsub: closure_of X Tx w ⊆ pickV w.
An exact proof term for the current goal is (andER (pickV w ∈ V) (closure_of X Tx w ⊆ pickV w) Hvpack).
We prove the intermediate claim Hclsubv: closure_of X Tx w ⊆ v.
rewrite the current goal using Heqv (from right to left).
An exact proof term for the current goal is Hclsub.
An exact proof term for the current goal is (Hclsubv x Hxcl).
An exact proof term for the current goal is (andI (closed_in X Tx (A_of v)) (A_of v ⊆ v) HAcl HAsub).
Set bumpV to be the term λv : set ⇒ Eps_i (λf : set ⇒ continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ (A_of v) → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval)).
We prove the intermediate claim HbumpV: ∀v : set, v ∈ V → continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x : set, x ∈ (A_of v) → apply_fun (bumpV v) x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV v) x = 0) ∧ (∀x : set, x ∈ X → apply_fun (bumpV v) x ∈ unit_interval).
Let v be given.
Assume HvV: v ∈ V.
We prove the intermediate claim HvTx: v ∈ Tx.
An exact proof term for the current goal is (HVTx v HvV).
We prove the intermediate claim HApack: closed_in X Tx (A_of v) ∧ A_of v ⊆ v.
An exact proof term for the current goal is (HA_of_closed_sub v HvV).
We prove the intermediate claim HAcl: closed_in X Tx (A_of v).
An exact proof term for the current goal is (andEL (closed_in X Tx (A_of v)) (A_of v ⊆ v) HApack).
We prove the intermediate claim HAsubv: A_of v ⊆ v.
An exact proof term for the current goal is (andER (closed_in X Tx (A_of v)) (A_of v ⊆ v) HApack).
We prove the intermediate claim Hexf: ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ (A_of v) → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval).
An exact proof term for the current goal is (Urysohn_bump_closed_in_open X Tx (A_of v) v Hnorm HAcl HvTx HAsubv).
An exact proof term for the current goal is (Eps_i_ex (λf0 : set ⇒ continuous_map X Tx R R_standard_topology f0 ∧ (∀x : set, x ∈ (A_of v) → apply_fun f0 x = 1) ∧ (∀x : set, x ∈ (X ∖ v) → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ X → apply_fun f0 x ∈ unit_interval)) Hexf).
Set bumpV0 to be the term λv : set ⇒ graph X (λx : set ⇒ apply_fun (bumpV v) x).
Set P to be the term {bumpV0 v|v ∈ V}.
We prove the intermediate claim HPsubFS: P ⊆ function_space X R.
Let f be given.
Assume HfP: f ∈ P.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f HfP (f ∈ function_space X R)) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Heq: f = bumpV0 v.
rewrite the current goal using Heq (from left to right).
Set g to be the term (λx : set ⇒ apply_fun (bumpV v) x).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
Apply (graph_in_function_space X R g) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hpack: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ (A_of v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) ∧ (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v HvV).
Apply Hpack to the current goal.
Assume Hleft Hui.
An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (apply_fun (bumpV v) x) (Hui x HxX)).
We prove the intermediate claim HPcont: ∀f : set, f ∈ P → continuous_map X Tx R R_standard_topology f.
Let f be given.
Assume HfP: f ∈ P.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f HfP (continuous_map X Tx R R_standard_topology f)) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Heq: f = bumpV0 v.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hpack: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ (A_of v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) ∧ (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v HvV).
Apply Hpack to the current goal.
Assume Hleft Hui.
Apply Hleft to the current goal.
Assume Hleft2 Hz.
Apply Hleft2 to the current goal.
Assume Hc Hval1.
We prove the intermediate claim HbV0FS: bumpV0 v ∈ function_space X R.
An exact proof term for the current goal is (HPsubFS (bumpV0 v) (ReplI V (λv0 : set ⇒ bumpV0 v0) v HvV)).
We prove the intermediate claim Hfun: function_on (bumpV0 v) X R.
An exact proof term for the current goal is (function_on_of_function_space (bumpV0 v) X R HbV0FS).
We prove the intermediate claim Heqpt: ∀x : set, x ∈ X → apply_fun (bumpV v) x = apply_fun (bumpV0 v) x.
Let x be given.
Assume HxX: x ∈ X.
Set g to be the term (λx0 : set ⇒ apply_fun (bumpV v) x0).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_congr_on X Tx R R_standard_topology (bumpV v) (bumpV0 v) Hc Hfun Heqpt).
We prove the intermediate claim HPui: ∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval.
Let f and x be given.
Assume HfP: f ∈ P.
Assume HxX: x ∈ X.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f HfP (apply_fun f x ∈ unit_interval)) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Heq: f = bumpV0 v.
rewrite the current goal using Heq (from left to right).
Set g to be the term (λx0 : set ⇒ apply_fun (bumpV v) x0).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
We prove the intermediate claim Hpack: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ (A_of v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) ∧ (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v HvV).
Apply Hpack to the current goal.
Assume Hleft Hui.
An exact proof term for the current goal is (Hui x HxX).
We prove the intermediate claim HPdom: ∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u.
Let f be given.
Assume HfP: f ∈ P.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f HfP (∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u)) to the current goal.
Let v be given.
Assume HvV: v ∈ V.
Assume Heq: f = bumpV0 v.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u.
An exact proof term for the current goal is (HVcl v HvV).
Apply Hexu to the current goal.
Let u be given.
Assume Hu: u ∈ U ∧ closure_of X Tx 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) (closure_of X Tx v ⊆ u) Hu).
We prove the intermediate claim HvTx: v ∈ Tx.
An exact proof term for the current goal is (HVTx v HvV).
We prove the intermediate claim Hz: ∀x : set, x ∈ (X ∖ v) → apply_fun (bumpV0 v) x = 0.
Let x be given.
Assume Hxout: x ∈ (X ∖ v).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X v x Hxout).
Set g to be the term (λx0 : set ⇒ apply_fun (bumpV v) x0).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
We prove the intermediate claim Hpack: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ (A_of v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) ∧ (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v HvV).
Apply Hpack to the current goal.
Assume Hleft Hui.
Apply Hleft to the current goal.
Assume Hleft2 Hz0.
An exact proof term for the current goal is (Hz0 x Hxout).
We prove the intermediate claim Hsuppsub: support_of X Tx (bumpV0 v) ⊆ closure_of X Tx v.
An exact proof term for the current goal is (support_of_zero_outside_open_sub_closure X Tx (bumpV0 v) v HTx HvTx Hz).
An exact proof term for the current goal is (Subq_tra (support_of X Tx (bumpV0 v)) (closure_of X Tx v) u Hsuppsub (andER (u ∈ U) (closure_of X Tx v ⊆ u) Hu)).
We prove the intermediate claim HPone: ∀x : set, x ∈ X → ∃f : set, f ∈ P ∧ apply_fun f x = 1.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ x ∈ w.
An exact proof term for the current goal is (HWcovers x HxX).
Apply Hexw to the current goal.
Let w be given.
Assume Hwx: w ∈ W ∧ x ∈ w.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (x ∈ w) Hwx).
We prove the intermediate claim Hxw: x ∈ w.
An exact proof term for the current goal is (andER (w ∈ W) (x ∈ w) Hwx).
Set v to be the term pickV w.
We use (bumpV0 v) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (pickV w ∈ V) (closure_of X Tx w ⊆ pickV w) (HpickV w HwW)).
An exact proof term for the current goal is (ReplI V (λv0 : set ⇒ bumpV0 v0) v HvV).
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (pickV w ∈ V) (closure_of X Tx w ⊆ pickV w) (HpickV w HwW)).
We prove the intermediate claim Hxclw: x ∈ closure_of X Tx w.
An exact proof term for the current goal is ((subset_of_closure X Tx w HTx (HWsubX w HwW)) x Hxw).
We prove the intermediate claim Heqv: pickV w = v.
Use reflexivity.
We prove the intermediate claim HwWv: w ∈ W_of v.
An exact proof term for the current goal is (SepI W (λw0 : set ⇒ pickV w0 = v) w HwW Heqv).
We prove the intermediate claim HclwIn: closure_of X Tx w ∈ Cl_of v.
An exact proof term for the current goal is (ReplI (W_of v) (λw0 : set ⇒ closure_of X Tx w0) w HwWv).
We prove the intermediate claim HxA: x ∈ A_of v.
An exact proof term for the current goal is (UnionI (Cl_of v) x (closure_of X Tx w) Hxclw HclwIn).
We prove the intermediate claim Hpack: continuous_map X Tx R R_standard_topology (bumpV v) ∧ (∀x0 : set, x0 ∈ (A_of v) → apply_fun (bumpV v) x0 = 1) ∧ (∀x0 : set, x0 ∈ (X ∖ v) → apply_fun (bumpV v) x0 = 0) ∧ (∀x0 : set, x0 ∈ X → apply_fun (bumpV v) x0 ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v HvV).
Apply Hpack to the current goal.
Assume Hleft Hui.
Apply Hleft to the current goal.
Assume Hleft2 Hz0.
Apply Hleft2 to the current goal.
Assume Hc Hval1.
Set g to be the term (λx0 : set ⇒ apply_fun (bumpV v) x0).
We prove the intermediate claim Hb0eq: bumpV0 v = graph X g.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
An exact proof term for the current goal is (Hval1 x HxA).
We prove the intermediate claim HPlf: ∀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.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (locally_finite_family_property X Tx V HVlf x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HN: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HNcore: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HN).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HNcore).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNcore).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HN).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ V ∧ ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HSfinSub: finite S ∧ S ⊆ V.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ V) (∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ V) HSfinSub).
We prove the intermediate claim HSsubV: S ⊆ V.
An exact proof term for the current goal is (andER (finite S) (S ⊆ V) HSfinSub).
We prove the intermediate claim HSprop: ∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ V) (∀A : set, A ∈ V → A ∩ N ≠ Empty → A ∈ S) HS).
Set F0 to be the term {bumpV0 v0|v0 ∈ S}.
We use N 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 HNTx.
An exact proof term for the current goal is HxN.
We use F0 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 (Repl_finite (λv0 : set ⇒ bumpV0 v0) S HSfin).
We will prove F0 ⊆ P.
Let f be given.
Assume HfF0: f ∈ F0.
Apply (ReplE_impred S (λv0 : set ⇒ bumpV0 v0) f HfF0 (f ∈ P)) to the current goal.
Let v0 be given.
Assume Hv0S: v0 ∈ S.
Assume Heq: f = bumpV0 v0.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hv0V: v0 ∈ V.
An exact proof term for the current goal is (HSsubV v0 Hv0S).
An exact proof term for the current goal is (ReplI V (λv1 : set ⇒ bumpV0 v1) v0 Hv0V).
Let f be given.
Assume HfP: f ∈ P.
Assume Hsupp: support_of X Tx f ∩ N ≠ Empty.
Apply (ReplE_impred V (λv0 : set ⇒ bumpV0 v0) f HfP (f ∈ F0)) to the current goal.
Let v0 be given.
Assume Hv0V: v0 ∈ V.
Assume Heq: f = bumpV0 v0.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hv0Tx: v0 ∈ Tx.
An exact proof term for the current goal is (HVTx v0 Hv0V).
We prove the intermediate claim Hz: ∀z : set, z ∈ (X ∖ v0) → apply_fun (bumpV0 v0) z = 0.
Let z be given.
Assume Hzout: z ∈ (X ∖ v0).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (setminusE1 X v0 z Hzout).
Set g0 to be the term (λz0 : set ⇒ apply_fun (bumpV v0) z0).
We prove the intermediate claim Hb0eq: bumpV0 v0 = graph X g0.
Use reflexivity.
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (apply_fun_graph X g0 z HzX) (from left to right).
We prove the intermediate claim Hpack: continuous_map X Tx R R_standard_topology (bumpV v0) ∧ (∀z0 : set, z0 ∈ (A_of v0) → apply_fun (bumpV v0) z0 = 1) ∧ (∀z0 : set, z0 ∈ (X ∖ v0) → apply_fun (bumpV v0) z0 = 0) ∧ (∀z0 : set, z0 ∈ X → apply_fun (bumpV v0) z0 ∈ unit_interval).
An exact proof term for the current goal is (HbumpV v0 Hv0V).
Apply Hpack to the current goal.
Assume Hleft Hui.
Apply Hleft to the current goal.
Assume Hleft2 Hz0.
An exact proof term for the current goal is (Hz0 z Hzout).
We prove the intermediate claim Hsuppsubcl: support_of X Tx (bumpV0 v0) ⊆ closure_of X Tx v0.
An exact proof term for the current goal is (support_of_zero_outside_open_sub_closure X Tx (bumpV0 v0) v0 HTx Hv0Tx Hz).
We prove the intermediate claim Hsupp0: support_of X Tx (bumpV0 v0) ∩ N ≠ Empty.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hsupp.
We prove the intermediate claim Hexy: ∃y : set, y ∈ support_of X Tx (bumpV0 v0) ∩ N.
An exact proof term for the current goal is (nonempty_has_element (support_of X Tx (bumpV0 v0) ∩ N) Hsupp0).
Apply Hexy to the current goal.
Let y be given.
Assume Hy: y ∈ support_of X Tx (bumpV0 v0) ∩ N.
We prove the intermediate claim Hysupp: y ∈ support_of X Tx (bumpV0 v0).
An exact proof term for the current goal is (binintersectE1 (support_of X Tx (bumpV0 v0)) N y Hy).
We prove the intermediate claim HyN: y ∈ N.
An exact proof term for the current goal is (binintersectE2 (support_of X Tx (bumpV0 v0)) N y Hy).
We prove the intermediate claim Hycl: y ∈ closure_of X Tx v0.
An exact proof term for the current goal is (Hsuppsubcl y Hysupp).
We prove the intermediate claim HyProp: ∀U0 : set, U0 ∈ Tx → y ∈ U0 → U0 ∩ v0 ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∀U0 : set, U0 ∈ Tx → y0 ∈ U0 → U0 ∩ v0 ≠ Empty) y Hycl).
We prove the intermediate claim HNv0: N ∩ v0 ≠ Empty.
An exact proof term for the current goal is (HyProp N HNTx HyN).
We prove the intermediate claim Hv0N: v0 ∩ N ≠ Empty.
rewrite the current goal using (binintersect_com v0 N) (from left to right).
An exact proof term for the current goal is HNv0.
We prove the intermediate claim Hv0S: v0 ∈ S.
An exact proof term for the current goal is (HSprop v0 Hv0V Hv0N).
An exact proof term for the current goal is (ReplI S (λv1 : set ⇒ bumpV0 v1) v0 Hv0S).
We use V to witness the existential quantifier.
We use P to witness the existential quantifier.
Apply andI to the current goal.
We will prove 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).
Apply andI to the current goal.
We will prove 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).
Apply and7I to the current goal.
An exact proof term for the current goal is HVcov.
An exact proof term for the current goal is HVlf.
An exact proof term for the current goal is HVref.
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.
∎